# 038 — The Curry-Howard-Lambek Correspondence

Actually, instead of me spouting nonsense, some exercises might help. These sort of things helped me a lot in understanding the Curry-Howard(-Lambek) correspondence quite a lot.

Try to write the following logical propositions in Haskell (start with the type signature and then try to implement them):

``````1. (A & (B & C)) -> ((A & B) & C)

2. (A -> (B -> C)) -> (B -> (A -> C))

3. (A -> (B -> C)) -> ((A & B) -> C)

4. ((A & B) -> C) -> (A -> (B -> C))

5. ((A -> B) & (B -> C)) -> (A -> C)

6. (A -> B) -> (C & A) -> (C & B)

7. (A -> B) -> (C -> D) -> (A & C) -> (B & D)

8. (A -> B) -> (A -> C) -> A -> (B & C)
``````

Unless you cheated with `undefined`, you have yourself both a proof and a program for the propositions above

Extra hard: how do these look in Category Theory? Can you “draw” the arrows of these proofs?

It’s also interesting to try and think about how many inhabitants a type might have. We already noted that `forall a. a -> a` has a single inhabitant, `\a -> a`. What about these:

``````f :: forall a. a -> a -> a

g :: forall a. a -> a -> a -> a

h :: forall a b. (a -> b) -> a -> b

i :: forall a b c. (b -> c) -> (a -> b) -> a -> c

j :: forall a. a -> ()

k :: forall a. a -> Bool

l :: Bool -> Bool

m :: forall a. a -> [a]
``````

Can you figure out the introduction and elimination rules (in logic) without looking at the slides?

Can you write them in type theory? What’s the name of the intro/elimination functions in your FP language of choice? How would this look in CT?

1 Like

Mulțumim,

Despre teoria categoriilor, în prezentare (din câte îmi amintesc) Denisa a menționat seria de articole “Category Theory for Programmers” de Bartosz Milewski.

Cartea (PDF) se află aici: https://github.com/hmemcpy/milewski-ctfp-pdf

Există și un Scala Edition.

Cartea asta cred că ar putea fi bună pt clubul de lectură.

1 Like

For whoever works better with an example, let me show you

``````(A & (B & C)) -> ((A & B) & C)
``````

## Logic

``````A & (B & C)          A & (B & C)
----------- (&e1)   ------------- (&e2)
A                     B & C
--- (&e1)  --- (&e2)
B          C
------------------------ (&i)
A & B
----------------------------------------- (&i)
(A & B) & C
``````

## Type Theory

This becomes:

``````(a : A, (b : B, c : C)) -> ((a : A, b : B), c : C)
``````

Which can be proved:

``````(a : A, (b : B, c : C))          (a : A, (b : B, c : C))
----------------------- (&e1)   ------------------------- (&e2)
a : A                                 (b : B, c : C)
------ (&e1)   ------ (&e2)
b : B          c : C
------------------------ (&i)
(a : A, b : B)
-------------------------------------------------------------- (&i)
(a : A, b : B), c : C)

``````

Same thing, in Haskell (called `assoc`, and given three types: `A`, `B`, and `C`):

``````assoc :: (A, (B,C)) -> ((A,B) -> C)
assoc (a, (b,c)) = ((a,b),c)

-- but we can make it generic as well, for any type:
assoc_ :: (a, (b, c)) -> ((a, b), c)
assoc_ (a, (b, c)) = ((a, b), c)
``````

## Category Theory

`T` is the terminal object, and `t : T -> A x (B x C)` is what we start with. We need to be able to obtain an arrow `t' : T -> (A x B) x C)`.

By product `A x (B x C)`, we know there exists `p : A x (B x C) -> A` and `q : A x (B x C) -> B x C`.

By composition, we can obtain the arrows `p . t : T -> A` and `q . t : T -> B x C`.

By product `B x C`, we know there exists `p' : B x C -> B` and `q' : B x C -> C`.

By composition, we can obtain the arrow `p' . q . t : T -> B`.

So now, we have the following arrows:

• `p . t : T -> A`
• `p' . q . t : T -> B`

By definition of product, since we know `A x B` is the product of `A` and `B`, and since we have the arrows `T -> A` and `T -> B`, then we know there must be an unique arrow which we’ll name `l : T -> A x B`.

By composition we can obtain the arrow `q' . q . t : T -> C`.

Similarly to the step before, by definition of product, since we know `(A x B) x C` is a product of `A x B` and `C`, and since we have the arrows `l : T -> A x B` and `q' . q . t : T -> C`, then there must exist an unique arrow `t' : (A x B) x C`.

An interesting observation is that you can easily see how they’re all doing the same thing. Let’s try writing the `Haskell` version without taking advantage of pattern matching:

``````assoc :: (a, (b, c)) -> ((a, b), c)
assoc a_bc = ((fst a_bc, fst (snd a_bc)), snd (snd a_bc))

-- or, we could do this:

intro :: a -> b -> (a, b)
intro a b = (a, b)

e1 :: (a, b) -> a
e1 = fst

e2 :: (a, b) -> b
e2 = snd

assoc :: (a, (b, c)) -> ((a, b), c)
assoc a_bc = intro (intro (e1 a_bc) (e1 (e2 a_bc)) (e2 (e2 a_bc))
``````

If you follow the `Logic` proof from bottom to top, you’ll see that it:

• ends with `&i`, which relates to our first (from the left) `intro`
• its left side has an `&i`, which is the second `intro` in our code
• this inner `intro` is composed from `&e1` on the input, or premise, which is identical to what we write
• the `B` is obtained by doing `&e1` on `&e2` on the premise, which is exactly what we do
• its right hand side, `C`, is obtained by doing `&e2` twice, which is identical to our code

If you follow the `CT` proof:

• we could rewrite the `l : T -> A x B` arrow as `<i,j> : T -> A x B`, where `i = p . t : T -> A` and `j = p' . q . t : T -> B`.
• we already have `k = q' . q . t : T -> C`

So let’s look closer at what `i`, `j` and `k` are:

• `i` is `p . t`, which is the left projection of the premise, or `fst a_bc`

You may ask: Why?!? Well, `p . t` means `p after t`. In our case, `t` represents the input, so it’s equivalent to `a_bc`, and `p` is the left projection, which is equivalent to `fst`. Keep in mind that `a . b . c` means `c first, then b, then a` when reading the following.

• `j` is `p' . q . t`, which is `fst (snd a_bc)`
• `l = <i,j>`, so `l = (fst a_bc, fst (snd a_bc))`
• `k` is `snd (snd a_bc)`
• the result, `T -> (A x B) x C` is `< <i,j>, k > = ((fst a_bc, fst (snd a_bc)), snd (snd a_bc))`

If we look back at the Haskell definition:
`assoc a_bc = ((fst a_bc, fst (snd a_bc)), snd (snd a_bc))`

As for the other group, the first exercise is:

``````f :: forall a. a -> a -> a
``````

There are only two implementations/proofs/inhabitants:

``````f1 :: forall a. a -> a -> a
f1 a _ = a

f2 :: forall a. a -> a -> a
f2 _ a = a
``````

These two functions can be obtained through a different function that is a bit more useful:

``````ifThenElse :: Bool -> a -> a -> a
ifThenElse True a _ = a
ifThenElse False _ a = a

f1 :: a -> a -> a
f1 = ifThenElse True

f2 :: a -> a -> a
f2 = ifThenElse False
``````

Not quite sure how to prove this though. It’s probably enough to uncurry and show that `t1 :: T -> A` and `t2 :: T -> A` are the only arrows from `T` to `A`.

Edit: added detailed explanation to the first `Spoiler` on how to see the equivalence between Logic and Haskell, and between Category Theory and Haskell.

1 Like

Mulțumim pentru materiale, excelente exerciții și exemple detaliate!

Schimb un pic direcția cu o întrebare: s-a menționat în tabelul de corespondențe între logică și teoria tipurilor legătura între logica modală și monade. Niște referințe pentru detalii se poate, vă rog?

Eu am găsit un articol și o prezentare destul de hardcore.

Și o precizare din partea mea: O categorie cu un obiect terminal nu are neapărat produse binare. Este necesar să aibă pullbacks (exercițiu rezolvat și cazul particular pentru categoria `Mon`, a monoizilor).

Afirmația este, însă, adevărată pentru toposuri, la care aproape se ajunge în prezentarea Denisei, de îndată ce se introduc CCC.

Scuze pentru confuzie.

1 Like

In paper-ul lui Wadler exista o referire la Computational types from a logic perspective, unde am gasit:

Apoi cateva pagini mai jos:

Unde:

• [Intro] `◇ a` este `return`/`pure`
• [Elim] `◇ a -> (a -> ◇ b) -> ◇ b` este `bind`/`>>=`

Ideea este ca `◇` nu este precis definit, si poate diferi in functie de ce dorim sa facem:

• `◇` poate reprezenta prezenta unei exceptii, caz in care `◇ a = a + 1` (altfel spus, `Maybe a = Just a | Nothing`)
• `◇` poate reprezenta non-determinism, caz in care `◇ a = powerset(a)` (altfel spus, `[] a = [] | a : [a]`)
• `◇` poate reprezenta citirea dintr-un mediu extern, caz in care `◇ a = env^a` (altfel spus, `Reader env a = env -> a` (unde `return = const` si `>>=` este compozitie)

PS: In cautarile mele, am gasit si Modal Logic @Stanford unde apar cateva chestii interesante:

If `A` is a theorem of K, then so is `◻ A`

Care arata exact a `return` / `pure`.

Distribution axiom: `◻ (A -> B) -> (◻ A -> ◻ B)`

Care arata exact ca `<*> :: f (a -> b) -> f a -> f b`

Mai departe se mentioneaza de asemenea ca desi ar fi util in unele cazuri, nu se poate defini `◻ A -> A`, ceea ce este adevarat si pentru monade (dar nu pentru `co-monade`).

Mersi mult pentru detalii și resurse!

Am cîteva elemente de logică modală însușite și astfel că prind bine exemplele de Haskell. Încă încerc să ies din interpretarea pur matematică. Despre monade începusem să citesc de la Moggi (în special ca să-mi scot [sau, mai bine zis, lărgesc] reflexul de a gîndi doar că o monadă este o algebră într-o categorie de functori), așa că, din nou, exemplele tale pică perfect!

Oarecum offtopic: recomand călduros și eu Stanford Encyclopedia of Philosophy! Acoperă cu mult mai mult decît filosofie, are paginile scrise de autori recunoscuți în domeniu, e actualizată periodic, are multe referințe; dau doar cîteva exemple la subiectul curent:

1 Like

Mulțumim pentru exerciții @cvlad! Am continuat exercițiul cu numărul de inhabitants al unui tip. Nu sunt sigur că e corect rezolvat, căci poate mi-au mai scăpat din implementări.

Spoiler
• Pentru `g :: forall a. a -> a -> a -> a`, am găsit trei implementări:
``````g1 a1 a2 a3 = a1
g2 a1 a2 a3 = a2
g3 a1 a2 a3 = a3
``````
• Pentru `h :: forall a b. (a -> b) -> a -> b`, o singură implementare:
``````h = (\$)
``````
• Pentru `i :: forall a b c. (b -> c) -> (a -> b) -> a -> c`, o singură implementare:
``````i = (.)
``````
• Pentru `j :: forall a. a -> ()`, o singură implementare:
``````j = const ()
``````
• Pentru `k :: forall a. a -> Bool`, două implementări:
``````k1 = const True
k2 = const False
``````
• Pentru `l :: Bool -> Bool`, patru implementări:
``````l1 = const True
l2 = const False
l3 = id
l4 = not
``````
• Pentru `m :: forall a. a -> [a]`, un număr infinit (?) de implementări:
``````m0 _ = []
m1 a = [a]
m2 a = [a, a]
...
m∞ a = [a, a, ...]
``````

Pentru varianta categoric teoretică a primului exercițiu, nu mi-e întotdeauna clar cum ar trebui să intrepretez `->` – ca un morfism în categorie sau ca un obiect exponențial?

@dan.oneata Yep, alea sunt rezolvarile care le aveam in cap cand am scris exercitiile. (Ti-am editat post-ul si am pus rezolvariile intr-un spoiler tag, in caz ca vrea si altcineva sa le rezolve).

Cat despre `->`, acesta este intr-adevar un exponential in CT. In principiu, regula mea este urmatoarea:

• daca am de demonstrat A -> B, atunci inseamna ca am un `T -> A` si trebuie sa ajung la `T -> B`, deci nu folosesc exponentiali aici
• daca am `A -> B -> C`, ma folosesc de curry/uncurry si transform in: am `T -> A` si `T -> B` si trebuie sa ajung la `T -> C`
• daca am `(A -> B) -> A -> B`, atunci nu cred ca se poate fara exponentiali, pentru ca trebuie sa avem ca premiza `T -> (A -> B)`
1 Like

@adimanea Pullback este `f : X -> Z` si `g : Y -> Z`, nu? Inteleg cum limita acestuia este produsul `X * Y`, dar ce nu inteleg este de ce nu este suficient sa luam limita categoriei `2` (care are doua elemente fara nicio sageata)?

Edit: Cred ca acelasi lucru pot spune despre coprodus, si anume ca ar fi colimita imaginii categoriei `2`.

EditEdit: Defapt, cred ca limita oricarei discrete category este (n)-produsul, nu?

Ai cumva o referință care să explice de ce “limita pullback-ului este produsul” – sau am înțeles eu greșit? Întreb pentru că nu mi-e foarte clar ce înseamnă “limita unui pullback”, pentru că noțiunea de limită e, de obicei, definită pentru un functor.

Salut,

Eu ce am in cap (si poate fi total gresit) este asa:

• pornim de la o categorie `C`
• alegem categoria discreta `2`
• pentru orice functor `F : 2 -> C` (care practic ne va “alege” doua* obiecte din C)
• pentru orice obiect `x` din `C`, avem un functor constant `Const(x) : 2 -> C` (e.g. daca avem un obiect `A` in `C`, atunci `Const(A)` ne da `A`)
• avem un natural transform: `alpha(x) : Const(x) -> F` astfel incat diagramele comuta (conform regulilor de natural transform)
• exista o sageata unica intre orice obiect `Const(x)` si `lim(F)`, adica `f(x) : Const(x) -> lim(F)`

Atunci, pentru un `F` care “alege” obiectele `1 -> A` si `2 -> B`, atunci daca `lim(F) = AxB` (produsul) atunci `alpha(AxB)(1)` va fi `fst` si `alpha(AxB)(2)` va fi `snd`.

Cred ca daca luam toate variantele posibile de functor `F`, putem spune ca avem produs in categoria `C`. Altfel, daca luam o singura instanta, putem spune doar ca pentru `F` care duce `1 -> A` si `2 -> B`, atunci `lim(F)` va fi produsul `A x B`.

(*) Functorul `F` poate alege un singur element, si asta este cazul de produs `A * A`, care este ok si el.

Edit: Incurcasem sagetile pentru `alpha(x)`; este `Const(x) -> F`.

Da, are sens – limita functorului `F` : 2C ne dă produsul lui `F 1` și `F 2`.

Ce nu înțelesăsem eu era legătura cu pullback-urile. Dar bănuiesc că ideea e că dacă o categorie are pullback-uri, are automat și produse; confrom Wikipedia:

The pullback is similar to the product, but not the same. One may obtain the product by “forgetting” that the morphisms f and g exist, and forgetting that the object `Z` exists.

1 Like

Sigur nu poate funcționa chestia asta, fiindcă ar trebui să ai produse binare în orice categorie, ceea ce nu e adevărat (dar nici nu-s contraexemple “la îndemînă”). Bănuiala mea e că ultimele 2 bulinuțe din argumentarea ta nu țin mereu (transformarea naturală și limF).

Mai rumeg și revin, trebuie să revăd unde se folosește esențial pullback-ul și poate vin și cu un contraexemplu.

Repet, pentru categoriile “obișnuite” cred că merge, de-aia curge natural argumentul tău. Dar sigur există ceva spații topologice sau clase proprii (categorii mari) sau ceva ciudățenii unde nu merge.

Revin cînd am ceva concret.

Edit: Transformările naturale, pullback-urile și chiar produsele nu-s tocmai “gratis”, chiar dacă în categorii de mulțimi sau structuri algebrice sînt clare. Asta e ideea principală pe baza căreia o să încerc să te contrazic. Cu ceva “categorii scheletice” (categorii de diagrame) sau virgulă (comma) sau cu poseturi, nu știu acum. Dar m-aștept să fie ceva subtil.

Edit2: Categoria 2 trebuie să aibă identități, totuși.

Categoria discretă nu e un exemplu de categorie fără produse? (Prin categorie discretă înțeleg o categorie care are ca morfisme doar morfismele identitate)

Da, corect. Ai dreptate.

Poate exprimarea mea ar trebui sa fie "daca exista acest natural transform `alpha(x)`, atunci…? Pentru mine este de multe ori vag ce “ai voie” si ce “nu ai voie” sa faci intr-o categorie.

O construiesc cum vreau? Observ doar ce proprietati are prin alte categorii/functori pe care ii construiesc cum vreau? Depinde de context, si ce incerc sa demonstrez?

Da, cred că e corect cu dacă… Apoi, privitor la “ce ai voie”, de multe ori ideea este să meargă construcția “naturală” (evidentă). Dacă nu merge aia, aproape sigur nu merge în general. Știu că e și mai vag ce zic aici, dar așa am văzut că merg lucrurile.

Alternativ, ca să elimini acest vag și “gut instinct”, definești cum vrei, dar efectiv trebuie să verifici toate axiomele. Pot cădea chestii la cel mai mic detaliu, de-aia trebuie verificate toate detaliile cu construcția ta. Iar cînd ai pretenția unei afirmații “pentru orice categorie”, acolo e extrem de riscant. Concret: există categorii în care epi nu e surjectiv (și mono nu e injectiv). Dar n-aș numi niciodată contraexemplele “naturale”. (Așa cum aș numi, însă, naturală așteptarea ca aceste contraexemple să nu existe.).

2 Likes

Revin, cu întîrziere, cu contraexemplul.

Fie categoria dată de poset-ul a < b, c < b, dar a și c incomparabile.

Atunci ai săgeată x -> y dacă și numai dacă x < y. Deci b este obiectul terminal.

Pe de altă parte, dacă ar fi să existe produsul lui a și b, el ar fi infimumul lor, elementul mai mic decît ambele (pentru că ar trebui să existe proiecțiile pe factori), cu proprietatea de universalitate din definiție.

Or așa ceva nu avem.

Deci e o categorie cu obiect terminal, dar fără produse.

Sper că nu mi-a scăpat ceva.

Daca sagetile sunt `<`, atunci identitatea are alta semnificatie/semantica? Are sens intrebarea? Cred ca am mai dat o data de problema asta si n-am avut pe cine sa intreb

Edit: Si acum ca am incercat un pic sa diger si restul, pentru mine iar incepe sa fie complicat sa inteleg cand “am voie” sa adaug obiecte si sageti in categoria data ca exemplu.

Intuitia imi spune ca daca as avea un produs `a x b`, ar trebui sa fie ceva mai mic si decat `a` si decat `b`, dar cum am `a < b`, atunci este redundant si ar trebui sa fie izomorfic cu `b`, deci ar trebui sa am produs si aici… desi imi este greu momentan sa vad cum demonstrez. Ma mai gandesc.