?

Log in

No account? Create an account
язык, на котором не говорят [entries|archive|friends|userinfo]
beroal

[ website | personal website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]
[ tags | journal tags ]

Reader, Writer monads [Jun. 27th, 2010|11:38 pm]
beroal
[Tags|, , ]

[Update 2010-12-07. The extended version.]

Let C be a CCC. Let (×) be a product bifunctor in C. Cat is CCC, so we can curry (×):

curry (×) : C→(C⇒C)
curry (×) A = λB. A×B

Functor category C⇒C has usual monoidal structure. A monoid in C⇒C is a monad in C. We consider finite products as monoidal structure on C.

curry (×) 1 ≅ id
∀ A B. curry (×) (A×B) ≅ (curry (×) A) ∘ (curry (×) B)

Therefore (curry (×)) preserves monoidal structure, so it transports a monoid to a monad and a comonoid to a comonad. This is a construction for Coreader and Writer. What about Reader and Cowriter? Intuitively, we should use adjunction in CCC, though I can not understand how it is explained formally.
monad comonad
monoid base.Control.Monad.Writer.Writer Cowriter
canonical comonoid in a category with products base.Control.Monad.Reader.Reader Hackage.category-extras.Control.Comonad.Reader.Coreader
LinkReply

Comments:
[User Picture]From: 66george
2010-06-28 12:32 pm (UTC)
Пытаясь понять, как удобнее определять подстановку (больной вопрос), пришёл к странному выводу, что правильные модели для лямбда-исчисления - это не декартово замкнутые категории, а категории с некоторой более богатой структурой. Для простого типового лямбда-исчисления всё понял, для зависимых типов ещё нет, а то статью напишу.
(Reply) (Thread)
[User Picture]From: nivanych
2010-06-29 01:52 pm (UTC)
Это неплохо описано у Jacobs'а.
У него всё описывается через fibrations'ы.
(Reply) (Parent) (Thread)
[User Picture]From: 66george
2010-06-30 08:35 am (UTC)
Ничего там не описано. Если мы подставляем терм в формулу (или в другой терм, как в лямбда-исчислении), приходится переименовывать некоторые связанные переменные, чтобы не было коллизий. Определить строго, как мы это делаем и доказать корректно хорошие свойства подстановки оказывается мучительно трудным делом. Навскидку, почитайте статью вот этого немца, где он пытается всё сделать добросовестно
http://www.cs.nott.ac.uk/~txa/publ/alpha-draft.pdf
и это только маленькая часть литературы, где разные люди пытаются определить подстановку добросовестно, плачут, рыдают и приходят в отчаяние.
(Reply) (Parent) (Thread)
[User Picture]From: beroal
2010-06-30 09:48 am (UTC)
Как обычно, индексы де Брюина делают переименование ненужным. Не знаю правда, поможет ли это в декартово замкнутой категории.
(Reply) (Parent) (Thread)
[User Picture]From: 66george
2010-06-30 10:04 am (UTC)
Кстати, голландский язык очень хитрый. Я спросил у знатока, как читать фамилию Moerdijk, он сказал "Муурдяйк". Ван Гога они зовут "фан Хох". Индексы де Брёйна буквально соответствуют декартово замкнутым категориям, но человек ими пользоваться не может. При попытке же интерпретировать "человеческое" исчисление (с именованными переменными) выясняется, что оно в категорные модели укладывается с мучительным трудом. Обычно в книгах трудные мечта просто опускают. Altenkirch на второй странице насмехается над Барендрегтом (который считается педагогическим талантом), показывая, что и он кое-что опустил.
(Reply) (Parent) (Thread)
[User Picture]From: beroal
2010-06-30 10:29 am (UTC)
Я без понятия, как фамилия de Bruijn читается, я где-то видел написание «де Брюин».

А вы можете объяснить мне, чему в теории категорий соответствует бета-редукция?
(Reply) (Parent) (Thread)
[User Picture]From: 66george
2010-06-30 11:08 am (UTC)
Если писать равенства (а не редукции), то аксиомы лямбда-исчисления с индексами де Брёйна почти буквально соответствуют аксиомам декартово замкнутой категории. Если мы хотим писать редукции, то можно и аксиомы д.з.к. записать не в виде равенств, а в виде редукций и "вычислять", на эту тему следует искать по словам categorical combinators, categorical abstract machine. Возможно, это не то, о чём спрашивали? Категорный язык - это, по сути, некоторая форма комбинаторов.
(Reply) (Parent) (Thread)
[User Picture]From: beroal
2010-07-01 07:16 am (UTC)
Не совсем понимаю, чем равенства отличаются от редукций. Ну допустим у меня есть равенство
(λ v.t0) t1 = t1[v:=t0]
Какой аксиоме CCC оно соответствует?
(Reply) (Parent) (Thread)
[User Picture]From: 66george
2010-07-01 12:14 pm (UTC)
Хи-хи, у вас ошибка, правильно так
(λ v.t0) t1 = t0[v:=t1]
Добавим контекст Г. Исчисление типовое, надо ещё писать тип переменной v
Г |- (λ v:A.t0) t1 = t0[v:=t1]
Это соответствует аксиоме
Ev <λ(t0),t1> = t0
[Error: Irreparable invalid markup ('<id,>') in entry. Owner must fix manually. Raw contents below.]

Хи-хи, у вас ошибка, правильно так
(λ v.t0) t1 = t0[v:=t1]
Добавим контекст Г. Исчисление типовое, надо ещё писать тип переменной v
Г |- (λ v:A.t0) t1 = t0[v:=t1]
Это соответствует аксиоме
Ev <λ(t0),t1> = t0 <id, t1>
Если Г - некоторый объект, нарисуйте стрелки t0:ГхA->B и t1:Г->A
Если это не аксиома, то теорема (аксиомы можно по-разному выбирать)
(Reply) (Parent) (Thread)
[User Picture]From: beroal
2010-07-02 04:23 am (UTC)
Теперь понятнее. Если использовать индексы de Bruijn, то окружение есть последовательность, и Γ есть произведение последовательности объектов. При β-редукция нас интересует только переменная, которая находится на краю Γ.

В качестве аксиомы я предпочитаю «λ is a natural isomorphism».
доказательство
// definition of eval
λ eval = id (A⇒B)
// λ is natural
λ (eval ∘ (λ t0 × id A)) = id (A⇒B) ∘ λ t0
// id
λ (eval ∘ (λ t0 × id A)) = λ t0
// λ is an isomorphism
eval ∘ (λ t0 × id A) = t0
// (∘ ⟨id Γ, t1⟩)
eval ∘ (λ t0 × id A) ∘ ⟨id Γ, t1⟩ = t0 ∘ ⟨id Γ, t1⟩
// properties of product and functorial product
eval ∘ ⟨λ t0 ∘ id Γ, id A ∘ t1⟩ = t0 ∘ ⟨id Γ, t1⟩
// id
eval ∘ ⟨λ t0, t1⟩ = t0 ∘ ⟨id Γ, t1⟩

Хи-хи, у вас ошибка, правильно так
С кем не бывает. ;)
(Reply) (Parent) (Thread)
[User Picture]From: 66george
2010-07-02 09:40 am (UTC)
Да, терму соответствует стрелка из его контекста в его тип. Переменные де Брёйна - это просто проекции (первая, вторая, третья и т.д., считать от конца) Связывается лямбдой всегда крайняя переменная. Теперь возьмите Барендрегта "Ламбда-исчисление, его синтаксис и семантика" и почитайте раздел про категорные модели. А потом приложение C про переменные де Брёйна.
(Reply) (Parent) (Thread)
[User Picture]From: beroal
2010-07-03 03:01 am (UTC)
Ну, Барендрегт рассматривает бестиповое лямбда-исчисление и CCC с рефлексивным объектом. В нашем случае это лишнее усложнение. По крайней мере это я обнаружил в «5.5. Модели в произвольных декартово замкнутых категориях.»

А Bruijn действительно пишется Брёйн. :/
(Reply) (Parent) (Thread)
[User Picture]From: nivanych
2010-06-30 12:37 pm (UTC)
Что-то, видимо, плохо я его вспомнил.
Спасибо, почитаю.
(Reply) (Parent) (Thread)