EG
Ну, у Idris функции в позиции типов обязаны быть доказуемо тотальными, ЕМНИП
Size: a a a
2021 January 21
p
Ну, у Idris функции в позиции типов обязаны быть доказуемо тотальными, ЕМНИП
нет
p
я могу писать
foo: (putStrLn "a") -> (putStrLn "no")
foo: (putStrLn "a") -> (putStrLn "no")
p
но как написать значение которое имеет тип putStrLn "a" я не знаю
а
но как написать значение которое имеет тип putStrLn "a" я не знаю
IO () или чето
а
я могу писать
foo: (putStrLn "a") -> (putStrLn "no")
foo: (putStrLn "a") -> (putStrLn "no")
Так нельзя сделать потому что (putStrLn "a") должно иметь тип Type
а
или нет
p
IO () или чето
нет
p
там будет тип putStrLn "10" грубо говоря
p
Так нельзя сделать потому что (putStrLn "a") должно иметь тип Type
а, это да
p
ну в завтип запихни
EG
nontotal : Int -> Type
nontotal x = nontotal x
foo : (nontotal 0) -> (nontotal 0)
foo x = foo x
main : IO ()
main = putStrLn (foo "x")
ЯННП
Идрис отказывается это компилировать, утверждая, что nontotal 0 это не String. Вопрос: как он узнал?
p
nontotal : Int -> Type
nontotal x = nontotal x
foo : (nontotal 0) -> (nontotal 0)
foo x = foo x
main : IO ()
main = putStrLn (foo "x")
ЯННП
Идрис отказывается это компилировать, утверждая, что nontotal 0 это не String. Вопрос: как он узнал?
nontotal 0 имеет тип nontotal 0
EG
nontotal 0 имеет тип TypeEG
Как Idris доказал, что
nontotal 0 не вернёт String никогда?p
Как Idris доказал, что
nontotal 0 не вернёт String никогда?потому что он не тотальный этот nontotal 0
EG
И? Именно поэтому это недоказуемо
p
И? Именно поэтому это недоказуемо
смари, если функция в типе тотальная - она редуцируется
p
если нетотальная - просто подставляется тело