Daniel's Blog

Meaningfully Typechecking a Language in Idris

In this series, I use the dependently-typed programming language Idris to implement relatively simple typechecking of a simple object language. However, I do so with a twist: the typechecker produces expressions that are guaranteed to be safe to evaluate. The interpreter then doesn’t have to worry about checking for type errors.

• Meaningfully Typechecking a Language in Idris

  2416 words, about 12 minutes to read.

  This term, I’m a TA for Oregon State University’s Programming Languages course. The students in the course are tasked with using Haskell to implement a programming language of their own design. . . .

• Meaningfully Typechecking a Language in Idris, Revisited

  2970 words, about 14 minutes to read.

  Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. The gist of the post was as follows: . . .

• Meaningfully Typechecking a Language in Idris, With Tuples

  2232 words, about 11 minutes to read.

  Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. I then followed it up with Meaningfully Typechecking a Language in Idris, Revisited. . . .