Oℕ
Поэтому да, если бы, например поддержка лимитов была встроена в функциональный язые, можно было бы описывать тайпклассы с законами и требованием доказать их при объявлении инстанса, и это можно было бы (наверное) сделать без полноценных завтипов
Size: a a a
2020 February 23
Oℕ
Сомнительная штука, учитывая, что у них на четвертом скрине написано "specialisation"
Спасибо за Ваше мнение
CD
Спасибо за Ваше мнение
Это называется практичность. Наличие невыявленных подобных помарок является признаком низкой популярности, что в свою очередь - слабым свидетельством наличия каких-то скрытых проблем :)
Oℕ
Это называется практичность. Наличие невыявленных подобных помарок является признаком низкой популярности, что в свою очередь - слабым свидетельством наличия каких-то скрытых проблем :)
Спасибо за пояснение
МБ
Поэтому да, если бы, например поддержка лимитов была встроена в функциональный язые, можно было бы описывать тайпклассы с законами и требованием доказать их при объявлении инстанса, и это можно было бы (наверное) сделать без полноценных завтипов
Всё упрётся в понятие равенства, мне кажется. И без зав. типов не обойдётся. А пределы нельзя через сопряжения вводить?
Oℕ
Глобальные можно
Oℕ
Всё упрётся в понятие равенства, мне кажется. И без зав. типов не обойдётся. А пределы нельзя через сопряжения вводить?
Равенство не обязательно должно быть "типом", так что не понимаю, почему не обойдётся
Oℕ
Есть языки доказательств, где есть равенства, и нет завтипов
МБ
Равенство не обязательно должно быть "типом", так что не понимаю, почему не обойдётся
А как доказывать свойства конусов?
Oℕ
А как доказывать свойства конусов?
Что за свойства конусов
Oℕ
Я говорю не о языке для формализации теорката, а о языке, где есть лимиты и колимиты наряду с суммой, произведением и простой рекурсией для определения типов данных
NI
Я говорю не о языке для формализации теорката, а о языке, где есть лимиты и колимиты наряду с суммой, произведением и простой рекурсией для определения типов данных
И записываются, наверняка, через расширения Кана.
Которые, в свою очередь, записываются через параметричность.
;-)
Которые, в свою очередь, записываются через параметричность.
;-)
МБ
А как пределы задавать?.. Хм. Это же, всё равно, нужно понятие индекса, функтора... Автоматически можно ли предел построить?
МБ
И записываются, наверняка, через расширения Кана.
Которые, в свою очередь, записываются через параметричность.
;-)
Которые, в свою очередь, записываются через параметричность.
;-)
А можно пример? Вот, допустим, в языке нет суммы объектов. Как её выразить?
NI
А можно пример? Вот, допустим, в языке нет суммы объектов. Как её выразить?
Не знаю, можно ли так, чтоб совсем ничего не было базового...
Oℕ
А как пределы задавать?.. Хм. Это же, всё равно, нужно понятие индекса, функтора... Автоматически можно ли предел построить?
Пределы выражаются через продакты и эквалайзеры
Конечные пределы через конечные продакты и эквалайзеры.
Если у вас есть базовый опыт работы, этого должно хватить для представления общего вида предела - это тип зависимых рекордов, первая часть полей не зависит друг от друга, вторая часть полей - это равенства, зависимые от первой части полей
Конечные пределы через конечные продакты и эквалайзеры.
Если у вас есть базовый опыт работы, этого должно хватить для представления общего вида предела - это тип зависимых рекордов, первая часть полей не зависит друг от друга, вторая часть полей - это равенства, зависимые от первой части полей
Oℕ
Можно создать некоторую специализированную теорию типов, где будут термы двух форм - обычные и описывающие равенства между обычными.
Такая теория не будет завтипной, но пределы в ней выразить можно.
Такая теория не будет завтипной, но пределы в ней выразить можно.
Oℕ
Так же можно выразить и копределы - АДТ, снабжённый набором декларарируемых равенств между термами, с использованием конструкторов.
Функция, объявляющая паттерн-матчинг, обязана доказать, что ветки патерн-матчинга уважают, объявленные в типе равенства, как это делается в случае с HIT
Функция, объявляющая паттерн-матчинг, обязана доказать, что ветки патерн-матчинга уважают, объявленные в типе равенства, как это делается в случае с HIT
V
Не знаю, можно ли так, чтоб совсем ничего не было базового...
Сумму можно выразить через равенства, сигма-типы, пи-типы и импредикативную вселенную утверждений.
V
ну и аксиома K там нужна еще