Daniel's Blog

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.