[Haskell-cafe] Well typed OS
Joachim Durchholz
jo at durchholz.org
Sun Oct 7 16:18:50 UTC 2018
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
More information about the Haskell-Cafe
mailing list