EG
Он не может понять во втором случае что _ не включает 0
Ему не нужно было бы это понимать, если бы он вызвал функцию
Size: a a a
2021 February 01
ΑZ
Ему не нужно было бы это понимать, если бы он вызвал функцию
Перепиши на case
EG
*/tmp/test> my_type 0
Int : Type
Вызов этой функции возвращает
Intp
Ему не нужно было бы это понимать, если бы он вызвал функцию
Он вызывает my_type на рандомном _ и видит что там может быть 0 или _
EG
Он вызывает my_type на рандомном _ и видит что там может быть 0 или _
Он что-то «вызывает» максимум как в слове «symbolic execution». Он не вызывает функцию по-настоящему.
p
Я бы посмотрел что там но Идрис удалил
ΑZ
Я бы посмотрел что там но Идрис удалил
Почему?
EG
Перепиши на case
Без разницы, оно не тайпчекнется
Idris умеет в компайл-тайме паттерн-матчить только на сумтипах
Idris умеет в компайл-тайме паттерн-матчить только на сумтипах
DS
Без разницы, оно не тайпчекнется
Idris умеет в компайл-тайме паттерн-матчить только на сумтипах
Idris умеет в компайл-тайме паттерн-матчить только на сумтипах
Так пречём тут зав типы, если это проблемы конкретной реализации у идриса?
p
Почему?
Нахер он мне нужен. Все равно тайплевел не работает.
p
Нет нормального тайплевела нигде
p
И очень вряд ли что появится
EG
Так пречём тут зав типы, если это проблемы конкретной реализации у идриса?
В каком ещё языке есть не совсем притянутые за уши завтипы?
EG
Вот именно чтоб как "принимаешь тип на вход и делаешь с ним чо хочешь"
DS
В каком ещё языке есть не совсем притянутые за уши завтипы?
В лямбда исчислении
EG
В лямбда исчислении
Это не ЯП
p
В лямбда исчислении
))
DS
Это не ЯП
А что это?
DS
Вполне себе самый настоящий ЯП
EG
А что это?
Это теоретическая математическая фигня
Неумение отличать теорию от практики — одна из основных проблем теоретиков
Неумение отличать теорию от практики — одна из основных проблем теоретиков