PLClub Discussion Group

Strongly-typed System F in GHC

On Friday, I’m going to be doing a dry-run for my Chalmers seminar a week from today.

I’ve decided to make my seminar a tutorial on de Bruin indices and well-typed interpreters, with the challenge of constructing a well-typed interpreter for System F in Haskell.

Your homework is to:

1. review Haskell syntax, especially for GADTs (https://downloads.haskell.org/ghc/8.8.3/docs/html/users_guide/glasgow_exts.html#generalised-algebraic-data-types-gadts) and DataKinds. My talk features a lot of Haskell code.

2. review the typing rules of the Simply-Typed Lambda Calculus and System F, to the level that they are described in wikipedia. https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus https://en.wikipedia.org/wiki/System_F

If you are eager to dive in, I’ve also written everything up, including all of the Haskell code and an explanation of my System F version in this repo:

https://github.com/sweirich/challenge/blob/canon/debruijn/README.md

I will be advertising this repository/write-up as part of my talk, so do send me comments about where the writing is unclear. (Or pull requests!)