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

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

Comments

[jtootf.livejournal.com]

ох. а можно пример практического применения ? пожалуйста :)

[lomeo.livejournal.com]

Меня всегда сбивают с толку такие вопросы. Если в ответ спросить: а что такое "практическое применение", то ещё не дай бог можно прослыть философом :-) Да и вообще по работе я больше пишу на Яве.

А ты GADT применяешь? Если да - то это тот же GADT, только теперь его можно расписывать в разных модулях. Аналог из ОО - базовый класс и куча его наследников.

Если GADT не применяешь, то доводы за его использование - это более строгий контроль типов.

[jtootf.livejournal.com]

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

GADT'ы до сих пор не применял. за пояснение спасибо, как столкнусь ближе с GADT'ами - вернусь к этому посту и буду думать :)

[lomeo.livejournal.com]

Ну вообще для меня изначально type families это вот такое решение вот таких проблем:

http://lomeo.livejournal.com/19562.html

А сейчас мне удалось увидеть это немного по другому. Я никогда не думал о type families как о dependent types. А DT - это тема, которая мне очень интересна. Я почти одержим такой сильной статической типизацией :)