просветить

[sassa_nf]

http://www.iai.uni-bonn.de/~jv/mpc08.pdf

improve :: (forall m. TreeLike m => m a) -> Tree a
improve m = abs m

ммм.... почему abs m тут можно подставить? Я думал, что forall m. TreeLike m => m a разрешает любое TreeLike m (тогда abs m is too specific и его нельзя, да?), но такое объявление функции выходит не эквивалентно improve :: TreeLike m => m a -> Tree a.

(abs - это в статье новая функция)

(про экзистенциальные типы читал, но в чём тут трюк не пойму)

порешал. TreeLike m => m a говорит, что функция работает с любым instance. (forall m. TreeLike m => m a) в данном случае означает, что caller обязан не выбирать конкретный instance TreeLike, т.е. caller "работает" с любым instance TreeLike, т.е. полиморфизм "навыворот". Конкретный instance выбирается на основании реализации improve.

Т.о. caller строит деревья с помощью TreeLike leaf и node - тем самым caller декларирует, что ему всё равно, какой именно instance подставить. Тогда improve = abs, выбрав CTree, заставляет caller тоже "пользоваться" leaf и node из CTree, но этот вопрос решается компилятором. Какая замечательная фича.

Comments

[udpn.livejournal.com]

Кажется, что использование чего-то сильнее let-полиморфизма не приводит к появлению понятности в коде. Я плохой человек, да?

Может быть, какие-то теоркаты естественно переписываются через ранк-н?

[sassa-nf.livejournal.com]

Как в теоркатах полиморфизм выразить для меня вообще загадка. Должно получиться что-то вроде "семейство стрелок". Может, в каких-то там n-категориях есть этому феномену объяснение.

До меры понятности в коде мне ещё далеко. Вот хоть как-то въехал в гибкость от такой конструкции, и то хорошо. Но и позывов выражать что-то в ранк-н не чувствую.