Size: a a a

2020 August 17

AZ

Alex Zhukovsky in rust_offtopic
ладно лень спорить, это вопрос как назвать
источник

p

polunin.ai in rust_offtopic
Alex Zhukovsky
я не вижу разницы между "никогда не присвоено значение" и "значение типа боттом"
Значений типа Боттом не существует
источник

AZ

Alex Zhukovsky in rust_offtopic
я лично воспринимаю боттомы как тип населенный специальными значениями, вы можете считать что он просто никогда не возвращает управление, разницы вроде нет
источник

p

polunin.ai in rust_offtopic
На то он и боттом
источник

AZ

Alex Zhukovsky in rust_offtopic
polunin.ai
Только bottom ненасеоенныц тип поэтому пофиг
я вот с этим вообще спорил. То что боттом не насселен не значит что пофиг. В идрисе тотальность это вопрос разрешимости тайпчекинга
источник

p

polunin.ai in rust_offtopic
Alex Zhukovsky
я вот с этим вообще спорил. То что боттом не насселен не значит что пофиг. В идрисе тотальность это вопрос разрешимости тайпчекинга
Последнее предложение что значит?
источник

r

red75prime in rust_offtopic
polunin.ai
Последнее предложение что значит?
Если идрис может вывести тип функции, то функция - тотальна, насколько я понял. Но на самом деле нет - вывод типов и проверка тотальности в идрисе разделены.
источник

AZ

Alex Zhukovsky in rust_offtopic
polunin.ai
Последнее предложение что значит?
идрис не разрешает использовать нетотальные функции на тайплевеле
источник

T1

Tony 123 in rust_offtopic
red75prime
Если идрис может вывести тип функции, то функция - тотальна, насколько я понял. Но на самом деле нет - вывод типов и проверка тотальности в идрисе разделены.
По-моему определение тотальной функции немного другое, разве нет?
источник

r

red75prime in rust_offtopic
Alex Zhukovsky
идрис не разрешает использовать нетотальные функции на тайплевеле
Позволяет, вообще-то
foo : Nat -> Nat
foo = foo

bar : (a : Nat) -> Vect (foo a) Nat
bar a = bar a
источник

AZ

Alex Zhukovsky in rust_offtopic
red75prime
Позволяет, вообще-то
foo : Nat -> Nat
foo = foo

bar : (a : Nat) -> Vect (foo a) Nat
bar a = bar a
хм, странно
источник

AZ

Alex Zhukovsky in rust_offtopic
но в любом случае плохая идея так делать
источник

DS

Doge Shibu in rust_offtopic
Ну идрис - это же не прувер, в нём пофигу
источник

p

polunin.ai in rust_offtopic
red75prime
Позволяет, вообще-то
foo : Nat -> Nat
foo = foo

bar : (a : Nat) -> Vect (foo a) Nat
bar a = bar a
Не должно скомпилироваться
источник

r

red75prime in rust_offtopic
polunin.ai
Не должно скомпилироваться
Компилируется, проверил. По-умолчанию консервативный детектор нетотальности отключён.
источник

AZ

Alex Zhukovsky in rust_offtopic
Doge Shibu
Ну идрис - это же не прувер, в нём пофигу
что пофигу? Я не вижу зачем на тайплевеле нетотальные функции иметь
источник

AZ

Alex Zhukovsky in rust_offtopic
из тайпчекера в базку ходить?
источник

DS

Doge Shibu in rust_offtopic
Alex Zhukovsky
из тайпчекера в базку ходить?
Ну да, тайппровайдер сделать, например
источник

AZ

Alex Zhukovsky in rust_offtopic
не нравится мне такая идея хз
источник

AZ

Alex Zhukovsky in rust_offtopic
для этого макросы есть
источник