I’ve been playing around with making a dependently typed language. It’s based upon Martin-Löf Type Theory (commonly just called Type Theory, TT). Turns out that implementing a dependent type system is a great way to learn how to use one! I had written code to translate from my toy languages’ terms into TT - but I wanted a compiler, so that I could execute it somewhere outside of the evaluator/norm
![Idris as a Library - BAM Weblog](https://cdn-ak-scissors.b.st-hatena.com/image/square/3c5df4c4f3d75f04b6f6578db63813d7514eaf90/height=288;version=1;width=512/http%3A%2F%2Fbrianmckenna.org%2Fblog%2Fstatic%2Flanguage-tt-target.png)