Meaningfully Typechecking a Language in Idris
Series status: Complete
First post in 2020, last post in 2020
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
2419 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. ...
-
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: ...
-
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. ...