Strongly Typed System F in GHC
Please log in to watch this conference skillscast.
There are many examples that demonstrate how to create a strongly typed abstract syntax in Haskell for a language with a simple type system. But there are many fewer examples that allow the embedded language to be polymorphic. I will work through what it takes to do so, touching on variable binding representations, and exploring the limits of dependently-typed programming in GHC.
Q&A
Code for the talk is here: https://github.com/sweirich/challenge
Question: Is there an example of implementing something like this in a language with a surface syntax and parser? I’m guessing one would need to push quite hard on singletons to instantiate the proofs required to construct the AST from the surface syntax.
Answer: I have an example of a typechecker for this AST in the repo. The idea is that you would parse into the weakly-typed AST.
And then use the typechecker to produce the strongly-typed version. https://github.com/sweirich/challenge/blob/canon/debruijn/src/TypeCheck.hs
Question: How far "away" is dependently typed GHC?
Answer: There are a few issues with syntax that hold off combining types and terms together.And there are thorny questions about how dependent types combine with all of the OTHER features of GHC. Richard Eisenberg has been focussed on GHC proposals that give us features that work towards dependent types.
Question: Followup question - How closely are you following the experience reports on using Dependently Typed Haskell in Industry. eg the Galois paper from last year’s ICFP?
Answer: I've been looking at the type theory for combining dependent types with roles, and with linear types, etc. I did a sabbatical at Galois during 2018-2019 to get some experience with their codebase. In fact this talk was inspired by thinking about how to add polymorphism to their strongly-typed intermediate language.
Question: Are there many differences or hurdles when you replace evaluation by substitution with an abstract machine?
Answer: I'm not sure I understand your question. Are you comparing my eval function to a different kind of evaluator that doesn't need substitution?
Maybe one that keeps around an environment or heap instead?
Do you mean like a Krivine machine?
Question: Yeah, like a Krivine machine for STLC.
Answer: I included eval in the talk as a simple motivation for the substitution operation.
Ed Kmett: I'll be doing a boring STLC using a sort of machine-like model in about 5 minutes, but unlike Stephanie I won't be trying so hard to make it safe.
Stephanie: Everyone should go see Ed’s talk. And Ed I'd love to talk to you about benchmarking substitution sometime. https://github.com/sweirich/lennart-lambda
Ed: I loved that paper. It taught me so much back when I was learning Haskell. The cadenza approach is rather different, so it should serve as an interesting point in the design space.
Stephanie: I've been adding a lot of new versions to it to compare different representations of binding. Including both bound and unbound.
YOU MAY ALSO LIKE:
Strongly Typed System F in GHC
Stephanie Weirich
Stephanie Weirich is a Professor of Computer and Information Science at the University of Pennsylvania. She works in the areas of functional programming, type systems, machine-assisted theorem proving and dependent types. Dr. Weirich has served as the program chair of POPL 2019, ICFP 2010 and the 2009 Haskell Symposium. Her awards include the 2016 Most Influential ICFP Paper award (for 2006) for the paper "Simple unification-based type inference for GADTs" and the 2016 ACM SIGPLAN Robin Milner Young Researcher Award.