The trickery here is basically pushing the type system to the extreme for relatively simple things. I wonder how the type system might cope for more complicated things. Another consequence is type errors. You won’t get something about trying to add a length to a time but rather something like “can’t unify type Pos1 with Zero,” or “error Units<f64,(z,(z,(z,(z,(s<z>,(z,()))))))> does not implement trait Add<Units<f64,(z,(z,(z,(s<z>,(z,(z,()))))))>>.” This is confusing enough in a trivial example but I wonder how this would go if the example were buried deep in the code.
The encodings used in the haskell library were not a church encoding (they could only express integers between about minus 9 and 9) though to be fair they claimed to be only there until better type level literals. I don’t know about the rust implementation.
Coq and Idris are quite weird languages. The reason they use Peano arithmetic at the type level is that it is easy for them to reason about. But in dependently typed languages where the type and value levels aren’t really separate, if you want to prove things about your programs, they also need to use these numbers which means you either need special language support for making them fast or you have slow programs, which is not suitable for the topic of efficient systems for computer mathematics. The other problem is that the computer can’t help much with the types and they require a lot of manually specifying things which many practitioners would consider trivial enough to be tacit. This is not good for having an expressive system for computer mathematics.
Another example of a system which tried to offer better mathematical foundations is fortress. They started out as something like “fortran but better at mathematics and without so much history” and ended up with something a lot more like haskell with a typeclass-like mechanism and mostly function language. They had a lot of issues with making the type system work with mathematics (one case is that it is hard to specify that something can be a (eg) a monoid. In mathematics, it’s often obvious or said very simply, but computers aren’t so good at knowing what is obvious. It can be complicated to say eg “this is a monoid with identity 1 and operation x,” or “this is a monoid with identity 0 and operation +” because your type system needs a way to disambiguate between the two monoids (or the language will need some bad ergonomics where it is very manually expressed). If your type system ends up needing to know about the names of things and having eg type classes dispatch on the operation or something, it could become tricky.
