гинь-гинь idris plus_right_zero : (n, m : Nat) -> n + m = n -> m = 0
plus_right_zero _ Z Refl impossible
plus_right_zero (S ) Refl impossible

вот это мне сгенерировал идрис, и это прошло totality check, по его мнению n+m=n на натуральных числах невозможно

Haskell idris Если вы встретите человека, который говорит что Haskell должен быть строгим по умолчанию — предложите ему пописать на Idris недельку

idris reddit.com

Coq idris Чувак по фамилии Идрисов будет рассказывать про Coq: techtalks.nsu.ru
Где логика?

Erlang Haskell Agda Coq idris *хз
Нужен (не срочно, но час X всё ближе и ближе) экстрактор в ерланг из каких-нибудь зависимых типов. Ничего не нашёл. Есть чо?

idris The Hitchhiker's Guide to the Curry-Howard Correspondence vimeo.com

idris Тихо-незаметно подбирается к 1.0.