AZ
ладно лень спорить, это вопрос как назвать
Size: a a a
2020 August 17
p
я не вижу разницы между "никогда не присвоено значение" и "значение типа боттом"
Значений типа Боттом не существует
AZ
я лично воспринимаю боттомы как тип населенный специальными значениями, вы можете считать что он просто никогда не возвращает управление, разницы вроде нет
p
На то он и боттом
AZ
Только bottom ненасеоенныц тип поэтому пофиг
я вот с этим вообще спорил. То что боттом не насселен не значит что пофиг. В идрисе тотальность это вопрос разрешимости тайпчекинга
p
я вот с этим вообще спорил. То что боттом не насселен не значит что пофиг. В идрисе тотальность это вопрос разрешимости тайпчекинга
Последнее предложение что значит?
r
Последнее предложение что значит?
Если идрис может вывести тип функции, то функция - тотальна, насколько я понял. Но на самом деле нет - вывод типов и проверка тотальности в идрисе разделены.
AZ
Последнее предложение что значит?
идрис не разрешает использовать нетотальные функции на тайплевеле
T1
red75prime
Если идрис может вывести тип функции, то функция - тотальна, насколько я понял. Но на самом деле нет - вывод типов и проверка тотальности в идрисе разделены.
По-моему определение тотальной функции немного другое, разве нет?
r
идрис не разрешает использовать нетотальные функции на тайплевеле
Позволяет, вообще-то
foo : Nat -> Nat
foo = foo
bar : (a : Nat) -> Vect (foo a) Nat
bar a = bar a
AZ
red75prime
Позволяет, вообще-то
foo : Nat -> Nat
foo = foo
bar : (a : Nat) -> Vect (foo a) Nat
bar a = bar a
хм, странно
AZ
но в любом случае плохая идея так делать
DS
Ну идрис - это же не прувер, в нём пофигу
p
red75prime
Позволяет, вообще-то
foo : Nat -> Nat
foo = foo
bar : (a : Nat) -> Vect (foo a) Nat
bar a = bar a
Не должно скомпилироваться
r
Не должно скомпилироваться
Компилируется, проверил. По-умолчанию консервативный детектор нетотальности отключён.
AZ
Ну идрис - это же не прувер, в нём пофигу
что пофигу? Я не вижу зачем на тайплевеле нетотальные функции иметь
AZ
из тайпчекера в базку ходить?
DS
из тайпчекера в базку ходить?
Ну да, тайппровайдер сделать, например
AZ
не нравится мне такая идея хз
AZ
для этого макросы есть