<p>I'm trying to draw a general mental picture about the models and the
denotational semantics of the typed lambda calculus, in its different
variants.</p>

<p>I'm particularly interested in how the semantics changes according to:</p>

<ol>
<li>which forms of recursion are allowed, and</li>
<li>which forms of polymorphism are allowed.</li>
</ol>

<p>I understand that, even if one makes a precise choice about these
options, there are many possible models.  Still, I would like to pick
a few concrete examples (or even one) for each option, and draw them
in my mental picture. Of course, the simplest the better.  I feel
that, at my current stage, I do not benefit much (yet) from abstract
descriptions such as "take <em>any</em> such-and-such category" when I do not
have any idea about how to craft at least one of those.</p>

<p>Since the topic is quite broad, let me ask a specific question:</p>

<p><strong>What would you study next?</strong> References are welcome.</p>

<p>Here's what I have seen so far:</p>

<ul>
<li><p>The STLC has a very simple set-theoretic model. Just interpret basic
types with sets, products with cartesian products, etc. Boring but
simple. Can be generalized to arbitrary CCCs.</p></li>
<li><p>STLC + term-level recursion / fixed points. This is essentially
PCF. We can build models using CPOs ($\omega$CPOs or DCPOs or
...). They are not fully abstract, but I'm not concerned with that.
To compute fixed points, Kleene's fixed point theorem saves the day.</p></li>
<li><p>PCF + type-level recursion. Here things start getting
non-trivial. To solve type-level recursive equations, we can
translate these to recursive domain equations, and solve them by
lifting the Kleene $\omega$-CPO machinery at the domain level.
Essentially, monotonic functions become functors, continuous
functions become continuous functors, and suprema become colimits.
Some issues arise since $\rightarrow$ is contravariant on its first
argument, but restricting the categories at hand to
embedding-projections pairs (which to me look like a special case of
Galois connections) one can make everything covariant.</p></li>
<li><p>Adding predicative polymorphism. By this, I mean allowing types like
$\prod_{\tau:\sf Mono} T(\tau)$ where $\sf Mono$ is the set of monomorphic
types, which do not contain such products. In such way, the product
is a countable one, hence a small one, so we can take the related
product on the CPOs for monotypes without any size issues. Shallow,
but simple.</p></li>
<li><p>Adding impredicative polymorphism, as in System F. Here
$\prod_{\tau:*}$ ranges over all the types, including polymorphic
ones. I'm not sure about how to proceed here. Types are still
countable, but we can't simply relate to a polymorphic type $\tau'$
the product of some selected CPOs as before, since such product would also involve
the CPO of $\tau'$ itself, which we are defining.</p></li>
<li><p>Adding dependent types. Ultimately I'd like to understand how a
dependently typed semantics can be given for a language featuring
unrestricted term-level recursion, and possibly type-level recursion
as well. I tried to read about fibered categories, but I think I'm not yet ready to tackle those, so I'm looking for some smaller steps, first. I will try again in the future, though.</p></li>
</ul>

CC BY-SA 3.0
2016-08-29T13:01:40.067Z
PER models seem like a natural next thing to study.
Andrej Bauer
CC BY-SA 3.0
2016-08-29T15:46:34.307Z
@chi, what do you count as denotational semantics?
Martin Berger
CC BY-SA 3.0
2016-08-29T16:44:18.380Z
@MartinBerger Good point. I guess I have a bias towards domain-theoretic semantics (à la Winskel's book) since I want to handle non-termination. I'm also willing to explore set-theoretical models for some terminating fragment, especially if they can be extended to cover non-termination as well. I'm not much familiar on those at the moment, though.
chi
CC BY-SA 3.0
2016-08-29T17:31:30.560Z
@chi How about logical formulae ordered by implication?
Martin Berger
CC BY-SA 3.0
2016-08-29T18:26:38.920Z
@MartinBerger You mean to interpret a lambda term as a (ordered) set of formulae? I'm trying to figure out how that would work...
chi
CC BY-SA 3.0
2016-08-29T18:30:15.090Z
@AndrejBauer Thanks. The first random paper I just browsed used a shallow approach to polymorphism: intersect all the PERs for every $\tau$ ranging over monotypes. I'll look further to find something deeper, so to encompass e.g. System F.
chi
CC BY-SA 3.0
2016-08-29T18:35:21.330Z
@chi We have a draft [here](http://users.sussex.ac.uk/~mfb21/publications/icalp06/completeness-full.pdf). It's not a very  well-developed approach currently.
Martin Berger
CC BY-SA 3.0
2016-08-29T18:58:11.573Z
For System F things are a bit more complicated. There's usually more category theory involved.
Andrej Bauer
CC BY-SA 3.0
2016-08-29T20:07:55.053Z
@AndrejBauer Would you recommend starting from any particular approach, even if abstract, for System F?
chi
CC BY-SA 3.0
2016-08-30T12:16:39.690Z
Maybe Paul Taylor's Appendix A of http://www.paultaylor.eu/stable/prot.pdf, that's a classic. If you want to dive into category theory you could try the recent paper by Ghani, Nordvall and Simpson (http://link.springer.com/chapter/10.1007%2F978-3-662-49630-5_1 or https://pure.strath.ac.uk/portal/en/publications/comprehensive-parametric-polymorphism(db9cd888-7a11-40ea-95d6-bfcfd2213d9d).html for a pdf)
Andrej Bauer
<reference-request><pl.programming-languages><type-theory><lambda-calculus><denotational-semantics>
Typed Lambda Calculus models and denotations
chi
# Typed Lambda Calculus models and denotations

(Asked by: username_0 on 2016-08-29)

I'm trying to draw a general mental picture about the models and the
denotational semantics of the typed lambda calculus, in its different
variants.

I'm particularly interested in how the semantics changes according to:

1. which forms of recursion are allowed, and
2. which forms of polymorphism are allowed.

I understand that, even if one makes a precise choice about these
options, there are many possible models. Still, I would like to pick
a few concrete examples (or even one) for each option, and draw them
in my mental picture. Of course, the simplest the better. I feel
that, at my current stage, I do not benefit much (yet) from abstract
descriptions such as "take *any* such-and-such category" when I do not
have any idea about how to craft at least one of those.

Since the topic is quite broad, let me ask a specific question:

**What would you study next?** References are welcome.

Here's what I have seen so far:

* The STLC has a very simple set-theoretic model. Just interpret basic
  types with sets, products with cartesian products, etc. Boring but
  simple. Can be generalized to arbitrary CCCs.
* STLC + term-level recursion / fixed points. This is essentially
  PCF. We can build models using CPOs ($\omega$CPOs or DCPOs or
  ...). They are not fully abstract, but I'm not concerned with that.
  To compute fixed points, Kleene's fixed point theorem saves the day.
* PCF + type-level recursion. Here things start getting
  non-trivial. To solve type-level recursive equations, we can
  translate these to recursive domain equations, and solve them by
  lifting the Kleene $\omega$-CPO machinery at the domain level.
  Essentially, monotonic functions become functors, continuous
  functions become continuous functors, and suprema become colimits.
  Some issues arise since $\rightarrow$ is contravariant on its first
  argument, but restricting the categories at hand to
  embedding-projections pairs (which to me look like a special case of
  Galois connections) one can make everything covariant.
* Adding predicative polymorphism. By this, I mean allowing types like
  $\prod\_{\tau:\sf Mono} T(\tau)$ where $\sf Mono$ is the set of monomorphic
  types, which do not contain such products. In such way, the product
  is a countable one, hence a small one, so we can take the related
  product on the CPOs for monotypes without any size issues. Shallow,
  but simple.
* Adding impredicative polymorphism, as in System F. Here
  $\prod\_{\tau:\*}$ ranges over all the types, including polymorphic
  ones. I'm not sure about how to proceed here. Types are still
  countable, but we can't simply relate to a polymorphic type $\tau'$
  the product of some selected CPOs as before, since such product would also involve
  the CPO of $\tau'$ itself, which we are defining.
* Adding dependent types. Ultimately I'd like to understand how a
  dependently typed semantics can be given for a language featuring
  unrestricted term-level recursion, and possibly type-level recursion
  as well. I tried to read about fibered categories, but I think I'm not yet ready to tackle those, so I'm looking for some smaller steps, first. I will try again in the future, though.

**Tags:** reference-request, pl.programming-languages, type-theory, lambda-calculus, denotational-semantics
> **Comments:**
> **username_1**: PER models seem like a natural next thing to study.  
> **username_2**: @chi, what do you count as denotational semantics?  
> **username_0**: @MartinBerger Good point. I guess I have a bias towards domain-theoretic semantics (à la Winskel's book) since I want to handle non-termination. I'm also willing to explore set-theoretical models for some terminating fragment, especially if they can be extended to cover non-termination as well. I'm not much familiar on those at the moment, though.  
> **username_2**: @chi How about logical formulae ordered by implication?  
> **username_0**: @MartinBerger You mean to interpret a lambda term as a (ordered) set of formulae? I'm trying to figure out how that would work...  
> **username_0**: @AndrejBauer Thanks. The first random paper I just browsed used a shallow approach to polymorphism: intersect all the PERs for every $\tau$ ranging over monotypes. I'll look further to find something deeper, so to encompass e.g. System F.  
> **username_2**: @chi We have a draft [here](http://users.sussex.ac.uk/~mfb21/publications/icalp06/completeness-full.pdf). It's not a very  well-developed approach currently.  
> **username_1**: For System F things are a bit more complicated. There's usually more category theory involved.  
> **username_0**: @AndrejBauer Would you recommend starting from any particular approach, even if abstract, for System F?  
> **username_1**: Maybe Paul Taylor's Appendix A of http://www.paultaylor.eu/stable/prot.pdf, that's a classic. If you want to dive into category theory you could try the recent paper by Ghani, Nordvall and Simpson (http://link.springer.com/chapter/10.1007%2F978-3-662-49630-5_1 or https://pure.strath.ac.uk/portal/en/publications/comprehensive-parametric-polymorphism(db9cd888-7a11-40ea-95d6-bfcfd2213d9d).html for a pdf)  

---

## 0 answers

