r
Я его не туда засунул, действительно надо в селект, а не в условие.
Size: a a a
2021 May 28
X
Хы, в haskell есть unsafe функции
X
Ну и зачем мне тогда энтот ваш раст?
ΑZ
ансейф в хачкеле это ио функции которые выглядят как пур функции. При этом память в сейфе попортить можно.
в расте ансейф это потенциально мемори ансейф фунцкии которые выглядят как мемори сейф. При этом ссайдэффектить в сейфе можно.
в расте ансейф это потенциально мемори ансейф фунцкии которые выглядят как мемори сейф. При этом ссайдэффектить в сейфе можно.
ΑZ
разные ансейфы
AN
а как в идрисе решается когда есть эфекты. например readInt
AN
вообще где про это почитать лучше. Как обходят IO
H
Переслано от Vyacheslav Goma
AN
получается где то захаркодили с этим IO, этим он отличается от монады которую я сделать могу сам, правильно? как он знает что нельзя зависеть от терма который содержить вызов с IO. ? Вообще же поидее не от любого выражения можно делать завтипы. хм не понятно.
AS
idris не тьюринг полный?
gо
Та часть Idris, которая может выполняться на тайплевеле, не Тьюринг-полная
gо
И в целом довольно ограниченная
AN
т.е. если я сделаю, грубо говоря someFuncThatRequiresEqArguments (f x) (f x) то он не сможет это проверить? Потому что не сможет вычислить f?
gо
Если f не тотальная, то думаю не сможет
gо
Idris не запускает ничего Тьюринг-полного на этапе компиляции
AN
аа там типа отдельно метку какую то ставишь для тотальных функций
KR
“мамойклянусь тотальная”?
gо
Нет
gо
Это проверяется
gо
«Но это же проблема останова!»
Да, поэтому это проверяется плохо.
Да, поэтому это проверяется плохо.