Type families

[lomeo]

Только недавно понял, что это то же самое, что и 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

Только их ещё и расширять можно. Так что алгебраические типы данных, которые можно выписывать в разных модулях уже есть :-)