Ancestors

Toot

Written by Brendan Zab on 2024-10-15 at 05:41

In case it’s useful to anyone, I’ve added an example of bidirectional elaboration for a polymorphic lambda calculus to my language garden, using normalisation-by-evaluation for comparing types: https://github.com/brendanzab/language-garden/tree/main/elab-system-f-bidirectional

Note that I’ve not implemented implicit instantiation of type applications and pattern unification – that would be a separate project, but I’ve provided links to sfpl and elaboration-zoo which show how to implement this.

=> More informations about this toot | More toots from brendan@types.pl

Descendants