This is precisly the sort of thing you could do if we finally had implemented inductive types in Julia
In type theory, a system has inductive types if it has facilities for creating a new type from constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.
The standard example is encoding the natural numbers using Peano's ...
Another formalistic language I want Julia to learn from is agda .
Programming in pure type theory involves a lot of tedious and repetitive proofs, and Agda has no support for tactics. Instead, Agda has support for automation via reflection . The reflection mechanism allows one to quote program fragments into – or unquote them from – the abstract syntax tree. The way reflection is used is similar to the way Template Haskell works.[8]
Reflection is also what Julia metaprogramming is based on, so extend the type system of Julia?
The new features don’t have to exactly resemble a previous language, just learn from it.
Are inductive types threatening to other aspects of the Julia language that would cause trade-off?
What you want is an inductive type so that the type system can make formal proofs about odd and even integers… I’ve been wanting this for a long time now.
@jeff.bezanson this is on more people’s wishlist now!