[TYPES] Annotating an AST with (existential) types, with ordered contexts - à la Dunfield Krishnaswami
Vanessa McHale
vamchale at gmail.com
Sat Mar 19 19:40:35 EDT 2022
Hi all,
I am trying to write a compiler with existential types. I understand that the Dunfield-Krishnaswami approach with ordered contexts is the new/cool way to do type inference.
However, I am stumped as to how to annotate a term with all the solved variables (when using ordered contexts). Is this possible? Is there any guidance/existing literature?
As an example, I’d like to be able to know/use the type of f in the below:
(λf. (f (λx. x)) (f ())) (λx. x)
Thanks,
Vanessa McHale
More information about the Types-list
mailing list