DS
Ну реально, считать идрис (с его старым и текущим рантаймом) - практическим языком, это буквально смешно.
Size: a a a
2021 February 01
EG
Потому что автор книжки хочет её продать.
Автор книжки == автор языка же.
EG
Чортов тайпскрипт умеет работать с примитивными типами на тайплевеле. Найтли раст умеет. Плюсы умеют десять тысяч лет.
Haskell, как я понимаю, умеет, с определённым количеством прагм.
DS
Автор книжки == автор языка же.
Да, и он тоже хочет его продать. Как ресерч язык он умеренной интересности, потому что вся движуха в агде. (И в коке)
p
Ну реально, считать идрис (с его старым и текущим рантаймом) - практическим языком, это буквально смешно.
Если компилировать в жс то норм. Только ффи поправить
EG
Haskell, как я понимаю, умеет, с определённым количеством прагм.
Но тут я не настоящий сварщик
DS
Haskell, как я понимаю, умеет, с определённым количеством прагм.
Скала тоже умеет, но это не проблема, если авторы языка этим озоботились.
EG
Скала и завтипы умеет, как я понимаю, осталось портировать это из скалы в менее объёмный язык
DS
Скала и завтипы умеет, как я понимаю, осталось портировать это из скалы в менее объёмный язык
Ограниченные зав типы.
Т.е. там выражаются зависимые пара и зависимая функция, но прям полноценный зав тип язык из них собрать не оч практично.
Т.е. там выражаются зависимые пара и зависимая функция, но прям полноценный зав тип язык из них собрать не оч практично.
s
Было бы что особо понимать в зав типах. Там нет прям какой-то дикого мозголобия или особой математики
Зависимые типы это всего лишь внутренний язык локально декартово замкнутой категории.
EG
Полноценный завтип язык это в любом случае что-то очень теоретическое
DS
Зависимые типы это всего лишь внутренний язык локально декартово замкнутой категории.
Ну примерно о чём я и говорю, вещь элементарная же.
EG
Зависимые типы это всего лишь внутренний язык локально декартово замкнутой категории.
Gentoo устанавливается тремя простыми командами...
DS
Полноценный завтип язык это в любом случае что-то очень теоретическое
Просто потому что ни у кого ещё не возникло интереса сделать реализацию без упора на пруфы
r
Просто потому что ни у кого ещё не возникло интереса сделать реализацию без упора на пруфы
В смысле с продвинутым пруф-ассистентом? Сравнить какие-нибудь foo: a b -> Vect (a+b) и foo b a без него просто так не получится
DS
red75prime
В смысле с продвинутым пруф-ассистентом? Сравнить какие-нибудь foo: a b -> Vect (a+b) и foo b a без него просто так не получится
Не, речь скорее про то, чтобы просто воспользоваться зав типами как основой для мощной системы типов, где легко оперировать тайплевелом и т.п.
DS
Без упора на использование этих фичей непосредственно в пруфах
DS
А чтобы получить всякие Type -> Type без необходимости в отдельных тайпевел конструкциях типа type families/match types/associated types и т.п.
DS
Чтобы иметь единый язык для тайп и value левела
p
У меня такое было