Пушка нахуй.
По обоим пунктам.

#osofnz/1

reply

ну вот, я как раз ищу примеры. Есть чо? А если найду?

(про п.2 — понятно, typed metaprogramming ещё, и всё?)

#osofnz/2

reply

тебе с практической точки зрения или вообще?

#osofnz/3

reply

если про гадты — я как-то разобрался, а в посте было такое полуумное трололо. Конечно, неконструктивное.
Если про зависимые типы и подобное — мне про них ВСЁ интересно, и с практической стороны, и с теоретической. Прекрасно понимаю, что для практического использования нужно и теорией владеть, да я и не против.
Кстати, есть пост и каменты в жыжыцэ, http://gds.livejournal.com/63409.html (привожу на всякий случай; даже не знаю, нужно ли).

#osofnz/4

reply

блин, там в комментах столько нажористого, что я даже про ужин забыл

счас прочитаю всё, дабы не повторяться

#osofnz/5

reply

мы старались :]
мнение (даже несмотря на повторы) очень интересно.

#osofnz/6

reply

ну, от меня полезного будет мало, я сам много чего узнал счас нового (и записал на прочтение несколько ссылок). в прикладных задачах я ограничиваюсь сермяжным Haskell'ем, минимально используя вещи вроде GADT'ов

но вот в свободное время занимался (и лениво продолжаю) вычислительной теорией категорий — реализацией конструктивных утверждений (это счас довольно модно, вообще говоря). рано или поздно возникает желание описать что-нибудь вроде индексированных категорий, а для этого требуются explicit type universes. может быть, это можно сделать и на Haskell с расширениями, но на той же Agda это можно сделать определённо. аналогично, вообще говоря, со многими другими алгебраическими структурами. как-то так

#osofnz/7

reply