gds 05.03.2012 14:39 umodni729F798C

gadt'ы — только для typed [e]dsl evaluation
dependent types — только для проверки границ массивов
дискасс блеять.

1. rtsome 05.03.2012 15:33

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

2. gdsrtsome /1 05.03.2012 15:36

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

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

3. jtootf 09.03.2012 15:51

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

4. gdsjtootf /3 09.03.2012 15:56

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

5. jtootfgds /4 09.03.2012 18:06

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

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

6. gdsjtootf /5 09.03.2012 18:14

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

7. jtootfgds /6 09.03.2012 20:15

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

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

Do you really want to delete ?