GADTs and typed environments

The Writing an interpreter with OCaml GADTs finishes with

It is possible to have a typed interpreter that avoids the type reconstruction (and the string comparison!) by enforcing the correspondence between variable indices and environments at the type level, but that gets complicated.

Does anyone have an example?

I’m rewriting my compiler from Zig to OCaml and need to implement value environments to know the expression that variables hold at any given moment. I use this for inlining.

You probably can take a look on this code that I made a long time ago: mirage-lambda/src/typedtree.ml at master · mirage/mirage-lambda · GitHub It’s a typed lambda calculus with a typed environment. You can also see the not so beautiful way to transform a simple AST to the GADT (with all proofs) here: mirage-lambda/src/typedtree.ml at a89b265b552f8b63ff725fc942f41a276fabb4f5 · mirage/mirage-lambda · GitHub

2 Likes