Ну если говорить только о значениях и закрыть глаза на типы, то конечно :)
Я вообще предполагал, по совету (http://nponeccop.livejournal.com/287952.html?thread=2373840#t2373840) nponeccop, что речь идёт о денотационной семантике. С ней дело не настолько чисто.
Давайте для простоты забудем о полиморфизме и посмотрим с точки зрения наивной теоретико-множественной интерпретации. Пока мы говорим о нерекурсивных типах, то всё понятно: это действительно навешивание бирок для размеченных объединений, построение кортежей и функциональные типы. Есть примитивные операции: аппликация, проекции, вложения, предикаты (сравнения конструкторов) — с понятным теоретико-множественным смыслом, и когда мы комбинируем эти операции, мы получаем простые функции, которые можно целиком определить, разбив область определения на конечное число областей и на каждой из них задав результат только с помощью аппликаций.
В частности, покуда мы не разрешаем рекурсивные типы, если композиция двух функций в какой-то точке вычисляется в _|_, то одна из двух исходных в соответствующем месте вычисляется в _|_ (simply typed гарантирует завершимость).
Что происходит при наличии рекурсивных типов? Теперь оказывается, что комбинацией примитивных операций можно получить рекурсивную функцию, которую нельзя задать в денотационной семантике явным уравнением ("на первом куске вот такое правило, на втором вот такое, всего кусков эн"), а только задать как предел последовательности итераций. Вы сами привели пример. В частности, _|_ теперь может возникнуть не только оттого, что кто-то явно вернул undefined, но и из-за зацикливания.
Собственно, я на то и хотел обратить внимание: 1) хотя Вы и определили y в терминах только применение одних элементарных термов к другим, теоретико-множественная интерпретация этой функции рекурсивна; 2) это происходит потому, что для (некоторых) рекурсивных типов денотационная семантика банальной аппликации существенно использует рекурсию (внезапно).
PS. Это всё, строго говоря, не про хаскел, так как у него нет интерпретации в категории Set. Ден. семантику для хаскела я не знаю — кстати, буду благодарен, если Вы посоветуете почитать что-нибудь, — но ожидаю увидеть в ней то же явление.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2012-10-20 12:26 pm (UTC)Я вообще предполагал, по совету (http://nponeccop.livejournal.com/287952.html?thread=2373840#t2373840)
С ней дело не настолько чисто.
Давайте для простоты забудем о полиморфизме и посмотрим с точки зрения наивной теоретико-множественной интерпретации. Пока мы говорим о нерекурсивных типах, то всё понятно: это действительно навешивание бирок для размеченных объединений, построение кортежей и функциональные типы. Есть примитивные операции: аппликация, проекции, вложения, предикаты (сравнения конструкторов) — с понятным теоретико-множественным смыслом, и когда мы комбинируем эти операции, мы получаем простые функции, которые можно целиком определить, разбив область определения на конечное число областей и на каждой из них задав результат только с помощью аппликаций.
В частности, покуда мы не разрешаем рекурсивные типы, если композиция двух функций в какой-то точке вычисляется в _|_, то одна из двух исходных в соответствующем месте вычисляется в _|_ (simply typed гарантирует завершимость).
Что происходит при наличии рекурсивных типов? Теперь оказывается, что комбинацией примитивных операций можно получить рекурсивную функцию, которую нельзя задать в денотационной семантике явным уравнением ("на первом куске вот такое правило, на втором вот такое, всего кусков эн"), а только задать как предел последовательности итераций. Вы сами привели пример.
В частности, _|_ теперь может возникнуть не только оттого, что кто-то явно вернул undefined, но и из-за зацикливания.
Собственно, я на то и хотел обратить внимание:
1) хотя Вы и определили
yв терминах только применение одних элементарных термов к другим, теоретико-множественная интерпретация этой функции рекурсивна;2) это происходит потому, что для (некоторых) рекурсивных типов денотационная семантика банальной аппликации существенно использует рекурсию (внезапно).
PS. Это всё, строго говоря, не про хаскел, так как у него нет интерпретации в категории Set.
Ден. семантику для хаскела я не знаю — кстати, буду благодарен, если Вы посоветуете почитать что-нибудь, — но ожидаю увидеть в ней то же явление.