Toot

Written by Brendan Zab on 2024-10-22 at 01:41

One frustration I’ve run into when making a type checker/elaborator for a programming language that uses normalisation-by-evaluation in types is the following gap in terminology:

• term / value

• type / ???

I.e. what do I call a type in the semantic domain?

I’ve listed some potential solutions here, but I’m curious if other people have favored approaches to this: https://gist.github.com/brendanzab/61ad11d0e6d007a084365c56035efd79

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

Mentions

Tags