Size: a a a

2021 January 21

EG

Emmanuel Goldstein in rust_offtopic
Ну, у Idris функции в позиции типов обязаны быть доказуемо тотальными, ЕМНИП
источник

p

polunin.ai in rust_offtopic
Emmanuel Goldstein
Ну, у Idris функции в позиции типов обязаны быть доказуемо тотальными, ЕМНИП
нет
источник

p

polunin.ai in rust_offtopic
я могу писать
foo: (putStrLn "a") -> (putStrLn "no")
источник

p

polunin.ai in rust_offtopic
но как написать значение которое имеет тип putStrLn "a" я не знаю
источник

а

а это кто in rust_offtopic
polunin.ai
но как написать значение которое имеет тип putStrLn "a" я не знаю
IO () или чето
источник

а

а это кто in rust_offtopic
источник

а

а это кто in rust_offtopic
polunin.ai
я могу писать
foo: (putStrLn "a") -> (putStrLn "no")
Так нельзя сделать потому что (putStrLn "a") должно иметь тип Type
источник

а

а это кто in rust_offtopic
или нет
источник

p

polunin.ai in rust_offtopic
а это кто
IO () или чето
нет
источник

p

polunin.ai in rust_offtopic
там будет тип putStrLn "10" грубо говоря
источник

p

polunin.ai in rust_offtopic
а это кто
Так нельзя сделать потому что (putStrLn "a") должно иметь тип Type
а, это да
источник

p

polunin.ai in rust_offtopic
ну в завтип запихни
источник

EG

Emmanuel Goldstein in rust_offtopic
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

polunin.ai in rust_offtopic
Emmanuel Goldstein
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

Emmanuel Goldstein in rust_offtopic
nontotal 0 имеет тип Type
источник

EG

Emmanuel Goldstein in rust_offtopic
Как Idris доказал, что nontotal 0 не вернёт String никогда?
источник

p

polunin.ai in rust_offtopic
Emmanuel Goldstein
Как Idris доказал, что nontotal 0 не вернёт String никогда?
потому что он не тотальный этот nontotal 0
источник

EG

Emmanuel Goldstein in rust_offtopic
И? Именно поэтому это недоказуемо
источник

p

polunin.ai in rust_offtopic
Emmanuel Goldstein
И? Именно поэтому это недоказуемо
смари, если функция в типе тотальная - она редуцируется
источник

p

polunin.ai in rust_offtopic
если нетотальная - просто подставляется тело
источник