Только недавно понял, что это то же самое, что и GADT:
data Z
data S n
data family List n a
data instance List Z a = Nil
data instance List (S n) a = Cons a (List n a)
--например
cadr :: List (S (S n)) a -> a
cadr (Cons _ (Cons x _)) = x
Только их ещё и расширять можно. Так что алгебраические типы данных, которые можно выписывать в разных
(
Read more... )