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