r
Доказательства писать объективно сложнее, чем сляпать что-то, что работает в типичных случаях.
Size: a a a
2020 December 29
DS
red75prime
Доказательства писать объективно сложнее, чем сляпать что-то, что работает в типичных случаях.
Зависимые типы не только ради пруфов нужны
DS
Они резко упрощают весь тайплевел
DS
Где у тебя будет стройная и разумная система вместо стандартного набора хаков
T1
Зависимые типы не только ради пруфов нужны
+
H
Они резко упрощают весь тайплевел
а можно один пример как они упрощают?
r
Где у тебя будет стройная и разумная система вместо стандартного набора хаков
Упрощают математическую структуру тайплевела. Но из этого не следует, что они упрощают понимание кода большинством программистов.
DS
red75prime
Упрощают математическую структуру тайплевела. Но из этого не следует, что они упрощают понимание кода большинством программистов.
Ты сравни как в том же расте делаются тайплевел вычисления в каком-нибудь франке и как такое делается на зав типах
DS
Второе куда проще для понимания, чем первое.
DS
а можно один пример как они упрощают?
Простой пример, чтобы сделать функцию из типы в тип тебе сейчас нужно городить трейты с ассосиатед типами или тайп фамили, если они у тебя есть в языке.
В языке с зависимыми типами - ты пишешь обычную функцию из типа в тип
В языке с зависимыми типами - ты пишешь обычную функцию из типа в тип
H
точно, забыл
r
Ты сравни как в том же расте делаются тайплевел вычисления в каком-нибудь франке и как такое делается на зав типах
Предполагаю, что для многих это просто подкапотная магия. И их больше интересует вменяемый интерфейс.
DS
red75prime
Предполагаю, что для многих это просто подкапотная магия. И их больше интересует вменяемый интерфейс.
И в зависимых типах и интерфейс у подобных дел будет куда более вменяемый.
Потому что тот же франк деталями своей реализации течет повсюду
Потому что тот же франк деталями своей реализации течет повсюду
H
r
И в зависимых типах и интерфейс у подобных дел будет куда более вменяемый.
Потому что тот же франк деталями своей реализации течет повсюду
Потому что тот же франк деталями своей реализации течет повсюду
Ну, может быть. Подумали бы ещё несколько лет и раст стал бы первым в мире функциональным системным языком с зависимыми типами, получившим достаточно широкое распространение в индустрии. 🙄
DS
Ну и кстати, смотрели бы нормально авторы раста на ФП языки у них бы и дерайвинг был бы человеческий, а не как сейчас
DS
Уже один GeneralizedNewtypeDeriving эргономику улучшил бы ощутимо
DS
Я уж молчу про DeriveVia
DS
И DeriveGeneric тоже было бы замечательно
в
Уже один GeneralizedNewtypeDeriving эргономику улучшил бы ощутимо
это же тайпроли надо вводить, чтобы такое заработало