p
В моем языке тип любого значение - это само значение. То есть для значения 0 его тип является 0. Это открывает нам следующие возможности:
1. Нам не нужно вводить дополнительно зависимые типы как отдельную сущность, мы можем просто указать в качестве дженерика например 0 и это будет работать отлично.
2. При этом нет необходимости использовать сигмо-типы там, где конкретный завтип неизвестен на этапе компиляции.
3. Можно тайпчекать то, что не тайпчекается обычными завтипами, например:
foo: Vect n (elem: 1..10) -> Vect n (elem + 1)
Это запись значит что мы ко всем элементам из вектора должны добавить 1. Если мы этого не сделаем, то компилятор будет ругаться на нас. В идрисе например чтобы выразить это ты будешь заебываться в доказательствах, а у меня это автоматически будет выводиться.
1. Нам не нужно вводить дополнительно зависимые типы как отдельную сущность, мы можем просто указать в качестве дженерика например 0 и это будет работать отлично.
2. При этом нет необходимости использовать сигмо-типы там, где конкретный завтип неизвестен на этапе компиляции.
3. Можно тайпчекать то, что не тайпчекается обычными завтипами, например:
foo: Vect n (elem: 1..10) -> Vect n (elem + 1)
Это запись значит что мы ко всем элементам из вектора должны добавить 1. Если мы этого не сделаем, то компилятор будет ругаться на нас. В идрисе например чтобы выразить это ты будешь заебываться в доказательствах, а у меня это автоматически будет выводиться.