[Haskell-cafe] Well typed OS

[Joachim Durchholz]

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