Лямбда-куб, статья в русской Википедии

[deniok]

Каждый должен посадить дерево, построить дом, воспитать ребенка и написать статью в Википедии.

Критикуйте, если что не так, а ещё лучше правьте прямо там.

Comments

[antilamer.livejournal.com]

Внес свою пару копеек про поддержку в языках программирования.

[deni-ok.livejournal.com]

Мне кажется, что в ограниченной форме лямбда омегу и Хаскелл98 поддерживает. Ну, то есть, наполовину - конструкторы типов есть (List a) :: * -> * (тип, зависящий от типа). Применили к типу Int :: *, получили (List Int) :: *. А лямбда-абстракции для этого дела нету: (\ (a :: *) -> (a -> a)) :: (* -> *) не запишешь. То есть типовый комбинатор D, такой что
D Int возвращает Int -> Int
D Bool возвращает Bool -> Bool
etc

Кстати на data families это можно как-то задать? Я пишу:

data family D :: * -> *

type Arr a b = (->) a b

data instance D b = Arr b b

Теперь в GHCi

*TypeFam> let f1 = (\x -> x) :: Arr Int Int
*TypeFam> :t f1
f1 :: Int -> Int
*TypeFam> let f2 = (\x -> x) :: D Int

:1:10:
    The lambda expression `\ x -> x' has one argument,
    but its type `D Int' has none
    In the expression: (\ x -> x) :: D Int
    In the definition of `f2': f2 = (\ x -> x) :: D Int

[lomeo.livejournal.com]

Делай на type families такие вещи

type family D a

type Arr a b = (->) a b

type instance D b = Arr b b

Насчёт лямбда абстракции нет, что-то не понял
Ты не об этом?

D = (&Lambda A. A -> A) :: (* -> *)

в типизированной полиморфной лямбде.

[deni-ok.livejournal.com]

Вот спасибочки, а то я пока type family и data family с трудом различаю.

А про лямбду над типами, да ты понял правильно. Большая лямбда - это какой ключик GHC надо заюзать? ;-)

[lomeo.livejournal.com]

Чёрт, я не подумал, что ты про Хаскель :-)

[deni-ok.livejournal.com]

Два двоеточия - о чем еще думать? ;-)

[lomeo.livejournal.com]

Ещё! Дай плз в статье ссылку на свой перевод главы из Барендрегта и на слайды с пометкой, что на русском.

[deni-ok.livejournal.com]

Я стесняюсь. Сам дай :)))

[lomeo.livejournal.com]

Дал, но

1. Ссылка не рабочая сейчас почему-то.
2. Я не знаю в какой форме правильно это делать.

[deni-ok.livejournal.com]

Это к dtim, очевидно последствия http://dtim.livejournal.com/180975.html