[
Используй корекурсию
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2022 January 24
ПС
толстый троллинг какой-то, как можно иметь корекурсию, но не иметь полноту по Тьюрингу
ПС
а, ну они точно так же забили на проблемы с завершаемостью, как и плюсы
в принципе базированно, когда и без этого компиляция может быть неразрешима
в принципе базированно, когда и без этого компиляция может быть неразрешима
[
Так у хаскеля именно из-за этого компиляция может быть неразрешима😅
[
Ещё на макросах вечный цикл можно сделать, конечно, но тут уже сам себе злобный буратино
AC
Можно, но это unsound. Либо ограниченно использовать, но это бессмысленно.
ПС
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
...[
Ну и я про это. Из-за этих расширений тайплевел и нетотальный.
AC
Э-ээ... Легко? Оно же так получается "по умолчанию". coCIC или как там его?
ПС
я уже нашёл что-то в мануале кока, да
https://coq.inria.fr/refman/language/core/coinductive.html
https://coq.inria.fr/refman/language/core/coinductive.html
ПС
Не осознал слова "нетотальный тайплевел" при первом прочтении, извините x)
[
[
Функции в типах, всё такое
ПС
я про какое-нибудь
x :: Nat = fix succ
y :: Fin x = 0
ПС
Неужели unsound и при условии, что вычисление термов завершается?
AC
Так для sound нужно чтобы вычисление типов завершалось — термы как раз завершаться не обязаны.
ПС