July 10th, 2012

glider

вопрос по агде

Вдохновленный метой, сел читать про Агду. Накопал отличную паперку, в которой вроде не надо знать всякого матана, называется The Power of Pi: http://www.google.ch/search?client=opera&rls=en&q=the+power+of+pi&sourceid=opera&ie=utf-8&oe=utf-8&channel=suggest.

Сразу возник вопрос, который хочу задать, чтобы самому не тупить сто лет (как показала мета, тупить в одиночку - плохая привычка, от которой надо избавляться). Итак, на третьей страничке аффтары объясняют как в Агде строить вьюшки и приводят вот такой пример, который позволяет паттерн-матчить листы в обратном порядке:

.

Что за дела? append - походу, обычная функция (т.е. не конструктор даных). Каким образом мы можем по ней матчиться? Чудеса. upd. Все оказалось очень просто - см. каменты.

Еще вот один вопрос есть. Пару вещей, которые я пытался читать про Агду, прямо таки пышут матаном. Intuitionistic type theory, productive coinductive type families и прочий ад не дают мне продвинуться дальше пары страниц. Какой учебник надо прочитать, чтобы дочитать этот хардкор до конца и не сойти с ума?