Am 07.10.2018 um 13:47 schrieb Ionuț G. Stan:
a type be generated for each natural number that's in the class file, and I have yet to see an approach that gives each of these types a printable, humanly understandable representation.
Can you give a bit more detail here? Or a pointer to someone who elaborated on this? I got a bit lost on the natural number step, which seems to be some sort of theoretical way to represent those types.
You can make Haskell's type system count, by defining a `Zero` type and a `Succ a` type - well, I think it's a kind (i.e. a type of types). That (and equality) is enough to do natural numbers - you have Zero, One = Succ Zero, Two = Succ Succ Zero, etc. I don't know enough about this stuff to give a recipe, I just saw descriptons of what people were doing. The earliest awesome trick of this kind was somebody who encoded matrix squareness in the type system. (You cannot even define inversion for a non-square matrix, so square matrices are pretty different beasts than non-square ones.) Somebody else (I think) started doing the natural numbers. You can do any kinds of cool tricks with that, such as cleanly expressing that to multiply two matrices, the height of one matrix needs to be the same as the width of the other. In theory, you can express any arithmetic relationships within the type system that way: Addresses, matrix dimension constraints, etc. In practice, any error messages are going to look like "invalid type Succ Succ Succ .... Succ Zero", and you have to count the number of Succs, which sucks (pun intended). I suspect you can also do fractional numbers with that - you essentially translate the axioms some type (or kind) declarations. I'd expect that to be even less usable in practice. However, it's intriguing what you can do with types. Now please take this all with a grain of salt. I never used this kind of stuff in practice, I just saw the reports of people doing this clever insanity, and didn't want to do it myself. The approach never took on if this kind of old lore isn't present in Haskell Café anymore.
BTW, I'm quite familiar with the class file format and have even started writing a bytecode verifier for my own compiler pet project. So, be as specific as you can.
I was more like handwaving at the possibility of turning all assertions over integral numbers into type constraints. I am definitely not recommending doing this in practice! Regards, Jo