​​A pure functional language for type-level programming in #rust

At its core, Tyrade supports recursive enum types (kinds, technically) and pure recursive functions.

https://github.com/willcrichton/tyrade

Tyrade is a proof-of-concept language showing how Rust traits enable a general purpose type-level programming model. Its goal is to show that type-level programming is possible for useful tasks (not writing Turing machines), and programs can be written in a reasonable way. Here's what the language looks like: