Iowa Type Theory Commute

Using GADTs for typed subsetting of your language


Listen Later

One use case for GADTs (as a special case of dependent types) is to form a typed subset of your host language.  One creates an EDSL called Expr a, where a is a type of the language (say this language is Haskell).  Values of types Expr a are the abstract syntax trees of expressions of type a from your host language.  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.

...more
View all episodesView all episodes
Download on the App Store

Iowa Type Theory CommuteBy Aaron Stump

  • 5
  • 5
  • 5
  • 5
  • 5

5

16 ratings