JC
Парс донт валидейт ин рашн https://habr.com/ru/post/498042/
а в Хаскеле head с ошибкой падает на пустом списке🌝
Size: a a a
2020 April 25
G
а в Хаскеле head с ошибкой падает на пустом списке🌝
В Idris это исправили вроде
SP
relude там тоже чтото хотят
G
prelude в Idris2 минимальный, кстати
AZ
а в Хаскеле head с ошибкой падает на пустом списке🌝
в хаскелле вообще прелюд плохой
AZ
но он 30 лет не менялся, можно простить языку из начала 90х такое
EG
В Idris это исправили вроде
В Idris head на пустом списке же не скомпилируется?
EG
Пока я не докажу, что список не пустой
SP
head().unwrap()
G
В Idris head на пустом списке же не скомпилируется?
Там вроде есть функция с
Maybe и та, которая не скомпилируется
G
Там вроде есть функция с
Maybe и та, которая не скомпилируется
G
C
Maybe нет, наврал) Само определение вектора там и так своего рода MaybeEG
Idris> :t head
Prelude.List.head : (l : List a) ->
{auto ok : NonEmpty l} -> a
EG
На списках тоже есть
head, но оно требует NonEmptyEG
А Maybe возвращает
head'G
А где тут
head?EG
А где тут
head?Я не знаю, но у меня в REPL он есть
