ЕС
Не понимаю что ты требуешь. Тапчекер тайпчекает тело, и проверяет совпадения. Все нормально.
Size: a a a
2020 June 10
AZ
Не понимаю что ты требуешь. Тапчекер тайпчекает тело, и проверяет совпадения. Все нормально.
ну так откуда тайпчекер узнает, имеля в виду Int или Nat?
ЕС
ну так откуда тайпчекер узнает, имеля в виду Int или Nat?
Тут нет типов Int, Nat, тут есть значение которое возвращает функция)
ЕС
Давай лучше конкретный пример неработающего с твоей точки зрения кода
ЕС
ну тело функции мы не тайпчекаем значит ? ведь
(x : Int ** myOtherFunc (myFunc x) 10)и например
(x : Nat ** myOtherFunc (myFunc x) 10)требуют разного тела
А конкретно здесь если ты хочешь ограничить чтобы x был больше или равен нулю, пишешь
x: ... && x > 0
x: ... && x > 0
AZ
мне немного лень расписывать
AZ
но учитывая какие у идриса проблемы с простейшим выводом типов, то такая магия либо невозможна в завтиповом языке, либо будет тормозить как черт (а значит, никому не будет нужна)
ЕС
ну так откуда тайпчекер узнает, имеля в виду Int или Nat?
Ну и напоследок: я считаю что числовой тип Nat должен проходить в числовой тип Int без ограничений и необходимого явного преобразования.
ЕС
С тз математики это логично.
ЕС
но учитывая какие у идриса проблемы с простейшим выводом типов, то такая магия либо невозможна в завтиповом языке, либо будет тормозить как черт (а значит, никому не будет нужна)
Ну вот пока не научатся, статическая типизация не оправдывает себя.
DS
но учитывая какие у идриса проблемы с простейшим выводом типов, то такая магия либо невозможна в завтиповом языке, либо будет тормозить как черт (а значит, никому не будет нужна)
Задача вывода типов в языке с зав типами не разрешима по очевидным причинам
ЕС
Задача вывода типов в языке с зав типами не разрешима по очевидным причинам
Хрень несёшь. Попробуй ещё раз.
ЕС
Это в идрисе неразрешима, потому что Идрис, хм, говно
ЕС
Если правильно обложить ограничениями зависимые типы, то вполне задача станет разрешимой. Учитывая ещё то, что большинство из того что предоставляет Идрис, не нужно в современном программировании.
DS
Хрень несёшь. Попробуй ещё раз.
ЕС
Спасибо, но покупать я это не собираюсь.
DS
Спасибо, но покупать я это не собираюсь.
Scihub к вашим услугам
ЕС
Спасибо, я лучше займусь более полезным делом. Когда поймёте как выводить типы можно будет поговорить. До тех пор самым лучшим языком будет питон.
DS
Спасибо, но покупать я это не собираюсь.
Нашел краткий пересказ:
First let me clarify what is proven in that paper: he shows that in a dependent calculus without annotations on the abstractions, it is undecidable to show typeability of a term in a non-empty context. Both of those hypotheses are necessary: in the empty context, typability reduces to that of the simply-typed λ-calculus (decidable by Hindley-Milner) and with the annotations on the abstractions, the usual type-directed algorithm applies.
The idea is to encode a Post correspondence problem as a type conversion problem, and then carefully construct a term which is typeable iff the two specific types are convertible. This uses knowledge of the shape of normal forms, which always exist in this calculus. The article is short and well-written, so I won't go into more detail here.
First let me clarify what is proven in that paper: he shows that in a dependent calculus without annotations on the abstractions, it is undecidable to show typeability of a term in a non-empty context. Both of those hypotheses are necessary: in the empty context, typability reduces to that of the simply-typed λ-calculus (decidable by Hindley-Milner) and with the annotations on the abstractions, the usual type-directed algorithm applies.
The idea is to encode a Post correspondence problem as a type conversion problem, and then carefully construct a term which is typeable iff the two specific types are convertible. This uses knowledge of the shape of normal forms, which always exist in this calculus. The article is short and well-written, so I won't go into more detail here.
DS
Само собой, что для какого-то подмножества языка вывод типов можно будет сделать, но всегда будут термы, для которых тип надо будет явно указать