Podcasts Technology Iowa Type Theory Commute Using GADTs for typed subsetting of your language

Using GADTs for typed subsetting of your language

Published: Jan. 20, 2020, 7 p.m.

b'

One use case for GADTs (as a special case of dependent types) is to form a typed subset of your host language.\\xa0 One creates an EDSL called Expr a, where a is a type of the language (say this language is Haskell).\\xa0 Values of types Expr a are the abstract syntax trees of expressions of type a from your host language.\\xa0 This is just a special case of embedding a typed language into your host language: in this case the typed language is a subset of your host language.

'