deniok: (lambda cube)
[personal profile] deniok
Каждый должен посадить дерево, построить дом, воспитать ребенка и написать статью в Википедии.

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

Date: 2009-02-27 08:30 am (UTC)
From: [identity profile] nivanych.livejournal.com
Получилась лучше, чем английская :-)

Date: 2009-02-27 08:31 am (UTC)
From: [identity profile] deni-ok.livejournal.com
С картинкой :)

Date: 2009-02-27 08:31 am (UTC)
From: [identity profile] nivanych.livejournal.com
Не знаю, стоит ли добавлять табличку из Барендрегта
про разрешимость type checking/inference/inhabitation...

Date: 2009-02-27 08:45 am (UTC)
From: [identity profile] deni-ok.livejournal.com
А, вспоминаю, была такая полезная таблица.

Только из которого Барендрегта? Ссылки нет под рукой, потерял. Вроде в Lambda Calculi with Types нет...

Date: 2009-02-27 09:44 am (UTC)
From: [identity profile] nivanych.livejournal.com
Lambda Calculi with Types, страница 68.

Date: 2009-02-27 09:46 am (UTC)
From: [identity profile] deni-ok.livejournal.com
Да, точно :)
Но это же не с куба системы - они карриевские, а на кубе черчевские.

(no subject)

From: [identity profile] nivanych.livejournal.com - Date: 2009-02-27 10:49 am (UTC) - Expand

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 10:51 am (UTC) - Expand

(no subject)

From: [identity profile] nivanych.livejournal.com - Date: 2009-02-27 11:18 am (UTC) - Expand

Date: 2009-02-27 09:15 am (UTC)
From: [identity profile] lomeo.livejournal.com
Молодец!

Надо такие кубики для детей выпускать. Пусть сидят и вместо домиков складывают свои системы типизированного ЛИ.

Date: 2009-02-27 09:49 am (UTC)
From: [identity profile] antilamer.livejournal.com
Внес свою пару копеек про поддержку в языках программирования.

Date: 2009-02-27 11:18 am (UTC)
From: [identity profile] 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

Date: 2009-02-27 06:54 pm (UTC)
From: [identity profile] 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) :: (* -> *)


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

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 07:40 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:04 pm (UTC) - Expand

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 09:26 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:11 pm (UTC) - Expand

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 09:25 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:35 pm (UTC) - Expand

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 09:59 pm (UTC) - Expand

Date: 2009-02-27 04:11 pm (UTC)
From: [identity profile] kurilka.livejournal.com
т.е. всёж у русской вики есть шанс? :)

Date: 2009-02-27 07:43 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Для того, чтобы работа шла зряче, полезно четко понимать начальные условия :-)

Date: 2009-02-27 09:31 pm (UTC)
From: [identity profile] kurilka.livejournal.com
дак раскрой их :)

Date: 2009-02-27 09:00 pm (UTC)
From: [identity profile] migmit.vox.com (from livejournal.com)
(задумчиво) интересно, куда отнести зависимость кайндов от типов?..

Date: 2009-02-27 09:09 pm (UTC)
From: [identity profile] lomeo.livejournal.com
Кайнды и есть типы. Поэтому к слабой омеге, наверное.

Date: 2009-02-27 09:11 pm (UTC)
From: [identity profile] migmit.vox.com (from livejournal.com)
> Кайнды и есть типы.

Ы? С этого момента поподробнее.

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:24 pm (UTC) - Expand

(no subject)

From: [identity profile] migmit.vox.com - Date: 2009-02-27 09:35 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:38 pm (UTC) - Expand

(no subject)

From: [identity profile] migmit.vox.com - Date: 2009-02-27 09:43 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:47 pm (UTC) - Expand

(no subject)

From: [identity profile] migmit.vox.com - Date: 2009-02-27 10:06 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 10:13 pm (UTC) - Expand

Date: 2009-02-27 09:15 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Ненененене

Кайнды - типы над типами с одним базовым "надтипом" * и одним конструктором (->), да и то последний нужен только если мы допускаем применения типа к типу ( слабую или не очень омегу)

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:25 pm (UTC) - Expand

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 09:28 pm (UTC) - Expand

Date: 2009-02-27 09:12 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Можно забацать лямбда-гиперкуб

Но вроде это всё покрывается PTSами

Date: 2009-02-27 09:38 pm (UTC)
From: [identity profile] migmit.vox.com (from livejournal.com)
Чем-чем?

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 09:50 pm (UTC) - Expand

Date: 2009-02-27 09:12 pm (UTC)
From: [identity profile] lomeo.livejournal.com
Нет, всё таки к Fω.

Date: 2009-02-27 09:24 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Если серьезно, то такой зависимости нет, если мы, конечно не монтируем что-то специальное. Чтобы она была, нужно допустить конструкцию аппликации кайнда к типу, порождающую кайнд:
(k:[]) (a:*)

Date: 2009-02-27 09:36 pm (UTC)
From: [identity profile] migmit.vox.com (from livejournal.com)
> то такой зависимости нет

Э-э-э... То есть, ghc 6.10 не работает?

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:37 pm (UTC) - Expand

(no subject)

From: [identity profile] migmit.vox.com - Date: 2009-02-27 09:41 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:54 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:55 pm (UTC) - Expand

(no subject)

From: [identity profile] migmit.vox.com - Date: 2009-02-27 10:03 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 10:14 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 10:17 pm (UTC) - Expand

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 10:29 pm (UTC) - Expand

(no subject)

From: [identity profile] migmit.vox.com - Date: 2009-02-27 10:35 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 10:35 pm (UTC) - Expand

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 09:55 pm (UTC) - Expand

Date: 2009-02-27 09:36 pm (UTC)
From: [identity profile] lomeo.livejournal.com
Почему вы думаете, что kind - это не тип??

(no subject)

From: [identity profile] migmit.vox.com - Date: 2009-02-27 09:38 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 09:57 pm (UTC) - Expand

(no subject)

From: [identity profile] migmit.vox.com - Date: 2009-02-27 10:01 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-27 10:12 pm (UTC) - Expand

(no subject)

From: [identity profile] deni-ok.livejournal.com - Date: 2009-02-27 10:18 pm (UTC) - Expand

(no subject)

From: [identity profile] lomeo.livejournal.com - Date: 2009-02-28 08:17 am (UTC) - Expand

Ну и кубик у вас :)

Date: 2009-05-03 03:45 pm (UTC)
From: [identity profile] nefia.livejournal.com
А чего это у вас кубик с шестнадцатью вершинами? ;-)

Re: Ну и кубик у вас :)

Date: 2009-05-04 12:52 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
Да ладно 16, остальные 48 просто спрятались ;-)

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 17th, 2025 05:52 pm
Powered by Dreamwidth Studios