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-11 05:11 pm (UTC)no subject
Date: 2012-10-11 05:21 pm (UTC)no subject
Date: 2012-10-11 05:41 pm (UTC)no subject
Date: 2012-10-11 05:48 pm (UTC)Во всяких F#/C# ленивость такая же - все энергичное, а итераторы ленивые.
no subject
Date: 2012-10-11 05:46 pm (UTC)no subject
Date: 2012-10-11 06:50 pm (UTC)Но можно и похитрее типы взять для лямбда-исчисления.
$ ocaml Objective Caml version 3.12.1+rc1 # ((fun x -> (x x)) (fun x -> (x x)));; Error: This expression has type 'a -> 'b but an expression was expected of type 'a # #rectypes;; <----- magic here # ((fun x -> (x x)) (fun x -> (x x)));; ^CInterrupted. # let f () = ((fun x -> (x x)) (fun x -> (x x)));; val f : unit -> 'a = <fun> # fun x -> x x;; - : ('a -> 'b as 'a) -> 'b = <fun> #no subject
Date: 2012-10-12 11:49 am (UTC)no subject
Date: 2012-10-11 07:53 pm (UTC)мы получили тип изоморфный
F a → a, т.е. тип, который можно применять к себе. А значит можем написать\x → x xкак\(F f) → f (F f)), а полный Y-комбинатор какno subject
Date: 2012-10-11 07:54 pm (UTC)no subject
Date: 2012-10-12 05:33 am (UTC)no subject
Date: 2012-10-12 08:32 am (UTC)let f x = x . f x in f :: (b -> b) -> a -> b
no subject
Date: 2012-10-12 02:28 pm (UTC)newtype Y a = Y {(|$) :: Y a -> a} y = let z w f = f $ (w |$ w) f in Y z |$ Y zY-комбинатор. Без скрытых fix-ов.
no subject
Date: 2012-10-13 12:32 pm (UTC)Да ладно. Просто они в конструкторы типов спрятаны.
В хаскеле же типы эквирекурсивные.
no subject
Date: 2012-10-13 12:40 pm (UTC)Они не могут быть спрятаны в конструкторы типов. Конструкторы типов — вещь абсолютно примитивная, никакой логики в них нет. Конструктор просто навешивает бирку на значение.
no subject
Date: 2012-10-13 02:15 pm (UTC)no subject
Date: 2012-10-13 02:23 pm (UTC)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", на всякий пожарный).