It’s been like a year and half since I’ve publicly shared something I’ve written but I figured someone might find these notes interesting. Please comment if you have any questions. Hopefully I’ll be sharing more sometime soon.

Also, as long as I’m posting things, I have been in the mood to write recently and was wondering if anyone had suggestions for introductory type theory concepts they’re curious about? Maybe even stuff to do with just functional programming?

A lot of this is past the limits of my knowledge of math, but one part jumped out at me:

The unfortunate bit of this model is that it’s not extensional.

Could you unpack why this is? I’ve just learned what “extensional” means, and this is one of those really satisfying moments when there’s a term with rigorous definition for a half-shaped concept that’s been rolling around in the back of my head. In this case, what about the definition of the model means it’s not extensional?

The basic idea is that in this model we can distinguish between the denotations of f and g even if f(x) = g(x) for all x. This is because f and g ended up coded as the collection of finite fragments of their graphs and there’s no guarantee that distinct collections will produce distinct functions.

The goal is that by using Godel numbering we can encode a continuous function P(N) -> P(N) as an element of P(N). If we used finite sets we would instead have P(P_fin(N)) which would not give us the desired retraction D -> D –> D that we need in order to define the lambda calculus.

Different sort of graph: rather than a graph of a term (Bohm tree) I’m referring to the graph of the function that a lambda term represents. Bohm trees are another way to give a nice semantics to the lambda calculus though.

Also, as long as I’m posting things, I have been in the mood to write recently and was wondering if anyone had suggestions for introductory type theory concepts they’re curious about? Maybe even stuff to do with just functional programming?

The next “what are you working on this week” thread on Monday morning would be a great place to get attention to this question.

A lot of this is past the limits of my knowledge of math, but one part jumped out at me:

Could you unpack why this is? I’ve just learned what “extensional” means, and this is one of those really satisfying moments when there’s a term with rigorous definition for a half-shaped concept that’s been rolling around in the back of my head. In this case, what about the definition of the model means it’s not extensional?

The basic idea is that in this model we can distinguish between the denotations of

`f`

and`g`

even if`f(x) = g(x)`

for all`x`

. This is because`f`

and`g`

ended up coded as the collection of finite fragments of their graphs and there’s no guarantee that distinct collections will produce distinct functions.Github says: “Sorry, this file is invalid so it cannot be displayed.”

Excitingly, it works for me.. I love computers. Is it corrupted if you download it?

No, the download link delivers a working PDF.

It works now. There must have been a glitch with Github.

[Comment removed by author]

The goal is that by using Godel numbering we can encode a continuous function P(N) -> P(N) as an element of P(N). If we used finite sets we would instead have P(P_fin(N)) which would not give us the desired retraction D -> D –> D that we need in order to define the lambda calculus.

Aren’t Böhm trees already a graph model of the lambda calculus?

Different sort of graph: rather than a graph of a term (Bohm tree) I’m referring to the graph of the function that a lambda term represents. Bohm trees are another way to give a nice semantics to the lambda calculus though.