Clojure, лямбды, черви, термы
Oct. 11th, 2012 07:58 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
metaclass(#(% %) #(% %)) - StackOverflow на кложуре
((fn [x] (x x)) (fn [x] (x x))) - StackOverflow на кложуре (более явная запись предущего)
на хаскеле даже на \x -> x x сразу ругается тайпчекер
(λx.xx)(λx.xx) - это оно же?
((fn [x] (x x)) (fn [x] (x x))) - StackOverflow на кложуре (более явная запись предущего)
на хаскеле даже на \x -> x x сразу ругается тайпчекер
(λx.xx)(λx.xx) - это оно же?
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2012-10-13 12:40 pm (UTC)no subject
Date: 2012-10-13 02:16 pm (UTC)При компиляции и
let a = 1 : aникаких фиксов не содержит.no subject
Date: 2012-10-13 04:48 pm (UTC)Ну да. А семантика конструктора типов — тривиальнейшая.
> Этот изоморфизм мы не смогли бы построить сами, если бы компилятор не умел делать вид, что он существует.
Почему делать вид-то? Тип ОПРЕДЕЛЁН так, чтобы этот изоморфизм существовал. И я не понимаю, что значит "построить": он есть по определению типа.
no subject
Date: 2012-10-14 02:54 pm (UTC)Вы можете возразить, что в денотационной семантике ваше выражение нигде не использует fix (который переход к точной верхней грани последовательности всё более определённых выражений). Но это лишь потому, что вы отложили его до момента, когда надо будет вычислять применение функции к конкретному значению.
Впрочем, ведь и Data.Function.fix тоже откладывает этот момент, только он использует явную рекурсию через let (примитив языка), а Ваш вариант — явную рекурсию на типах (тоже встроенную в язык), но поскольку она делается в другой строчке, то якобы её не было :)
no subject
Date: 2012-10-14 03:43 pm (UTC)Конечно. fix — он на уровне значений.
> Но это лишь потому, что вы отложили его до момента, когда надо будет вычислять применение функции к конкретному значению.
Чего-чего? Это что я куда отложил?
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.
Ден. семантику для хаскела я не знаю — кстати, буду благодарен, если Вы посоветуете почитать что-нибудь, — но ожидаю увидеть в ней то же явление.
no subject
Date: 2012-10-20 01:44 pm (UTC)С ней дело не настолько чисто.
С ней, как раз, всё кристально чисто.
> Давайте для простоты забудем о полиморфизме и посмотрим с точки зрения наивной теоретико-множественной интерпретации.
Нет, вот этого не надо. "Наивная теоретико-множественная интерпретация" — прямой путь в ад. Давайте по-нормальному: семантика Скотта и подходящая категория частично-упорядоченных множеств.
> Ден. семантику для хаскела я не знаю — кстати, буду благодарен, если Вы посоветуете почитать что-нибудь, — но ожидаю увидеть в ней то же явление.
Во-первых, я не вполне понимаю, что вы подразумеваете под "явлением".
Во-вторых, что конкретно почитать — не скажу, но гуглить надо семантику Скотта, теорию доменов, потом ещё, если будет настроение, найти такую вещь как "dI-domains" (вторая буква — заглавная "i", на всякий пожарный).