2

System F is a great way to simply reason about types when programming a prototype. Other than implementing it myself, I'd like to use an existing implementation.

When looking for implementations, there doesn't seem to be any - and I'm not sure why.

My question is: What is the canonical implementation of System F?

hawkeye
  • 34,745
  • 30
  • 150
  • 304
  • I'm not sure about "canonicity", but you can have a look at the implementations (in OCaml) by B.C. Pierce [here](https://www.cis.upenn.edu/~bcpierce/tapl/checkers/fullpoly/) and [here](https://www.cis.upenn.edu/~bcpierce/tapl/checkers/fullomega). The implementations are described in his [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/) book. – Anton Trunov Jun 26 '16 at 06:54
  • Cool - can you expand that into an answer? – hawkeye Jul 06 '16 at 12:28
  • All right -- it's done. – Anton Trunov Jul 06 '16 at 13:10

1 Answers1

1

The Types and Programming Languages book by B.C. Pierce is famous (among other things) for providing and discussing implementations of typed lambda calculi in OCaml.

The book provides an implementation of System F, called fullpoly and explains the implementation details in Chapter 25. fullpoly extends an implementation of simply-typed lambda calculus with booleans -- simplebool.

The instructions for building and executing those typecheckers and interpreters can be found here.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43