038 — The Curry-Howard-Lambek Correspondence


#1

Thank you everyone for attending! The slides are available at https://drive.google.com/file/d/1ghFPbIZ4r8-291f6weszNxLwMXu1U8kx/view (few minor corrections to come tomorrow)

I think I’ll try to write up a post tomorrow with an example of a simple program in Haskell, translated to Type Theory, Logic and Category Theory since this seems to be something useful to have next to the (awesome) slides.


#2

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 :slight_smile:

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?


#3

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ă.


#4

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

(A & (B & C)) -> ((A & B) & C)
Spoiler alert, full solution inside

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
Spoiler alert, full solution inside

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.


#5

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. :slight_smile:


Ș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.


#6

Salut @adimanea!

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).


#7

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:


#8

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, ...]

#9

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?


#10

@dan.oneata Yep, alea sunt rezolvarile care le aveam in cap cand am scris exercitiile. :+1: (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)

#11

@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?


#12

Salut @cvlad!

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.


#13

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.


#14

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.


#15

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. :slight_smile:

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.


#16

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)


#17

Da, corect. Ai dreptate.


#18

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? :slight_smile:


#19

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.).