B
так надо же быть сильным и независимым
Size: a a a
2021 May 26
AN
опять по кругу. Я думал увенчает успех какая то формула красивая.
ΑZ
зависимых типов есть два: сигма и произведение.
Сигма: зависимая пара
Пи: зависимая функция
Сигма: зависимая пара
(someVariable ** SomeType someVariable) - т.е. пара, где первый элемент тапла определяет ТИП второгоПи: зависимая функция
zeros : (n : Nat) -> Vect n Int - т.е. параметры определяют ТИП результатаTK
На самом деле тот, кто догадался отвязать тип от значения - гений
B
так, когда гаты
AN
ну правильно. Но где рантайм тут в определении. Мне кажется это уже шаг в сторону. В теории типов нету никаких рантаймов, разве нет?
ΑZ
так тут рантайма и нет
AN
там какие то термы, какие то универсы. прочая херня.
ΑZ
я ни слова про рантайм ещё не скаал
B
так тогда можно это все на темплейтах провернуть
AN
Ну вот в расте зависимая функция это как бэ Asoc.Types
ΑZ
нельзя. В темплейте n будет типом. Возможно синлтоном который выглядит как терм, но не терм
AN
о... А что есть терм?
AN
в чем отличие от конст дженериков тех же?
B
терминал
B
)))
ΑZ
тебе формально или по-человечески? Если по-человечески то терм это переменная
AN
т.е. рантайм. блин
ΑZ
ну можно формально без рантайма подойти
ΑZ
но все равно типом он не будет)