Здравствуйте, dotneter, Вы писали:

D>Кто нибудь может в пяти строчках кода и паре предложений выразить суть и
Суть в том что с типом связываются значения времени исполнения.
Например:

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

В данном случае описывается список тип которого параметризован не только типом элементов содержащихся в списке но и длинной этого списка.
Первый конструктор создает пустой список с типом которого связано значение 0.
Второй конструктор интереснее.
Первый (неявный) аргумент это длинна исходного списка.
Второй элемент.
Третий исходный список с типом которого связанна длинна.
И с результатом связанна длинна исходного списка плюс один.

D>основные бенефиты идеи?
Например мы хотим написать функцию которая принимает два списка одинаковой длинны и возвращает список кортежей.
Сигнатуру функции можно описать так:

zip : {n : Nat} -> {A : Set} -> {B : Set} -> (l1 : Vec A n) -> (l2 : Vec B n) -> Vec (A, B) n

Теперь если компилятор не будет уверен что в эту функцию передают списки одинаковой длинны то программа не скомпилируется.
Если программа скомпилируется то Компилятор также будет в курсе что тот список что вернула данная функция равен по длине двум исходным.

Это позволяет доказывать кучу утверждений и как следствие не писать код обработки подавляющего большинства нештатных ситуаций ибо их просто не может быть.
Как следствие если не лениться писать правильные типы то можно избавиться не только от кучи проверок в функции на тему, а не подсунули ли нам какую гадость и что делать если таки подсунули, но и юнит/интеграционных тестов ибо система типов их перекрывает с большим запасом.