Funny you should post that. I just wrote this and I need to compare notes with someone. I think I'm representing (some) ordinals as Haskell types here (not values, types). Essentially all ordinals that can be constructed from a finite number of applications of addition, multiplication and exponentiation to 1. But the important thing is that I'm not just modelling the underlying sets with types. I'm modelling the actual *ordinals* with types because () is an instance of () and so each of these types is also an instance of Ord. Does this look correct? Ordinal arithmetic isn't my field :-)
type One = () type Two = Either One One type N = [One] type Nplus1 = Either N One type NplusN = Either N N type NtimesN = (N,N) type NpowN = [N] type NpowNplusN = Either NpowN N
2 comments:
Funny you should post that. I just wrote this and I need to compare notes with someone. I think I'm representing (some) ordinals as Haskell types here (not values, types). Essentially all ordinals that can be constructed from a finite number of applications of addition, multiplication and exponentiation to 1. But the important thing is that I'm not just modelling the underlying sets with types. I'm modelling the actual *ordinals* with types because () is an instance of () and so each of these types is also an instance of Ord. Does this look correct? Ordinal arithmetic isn't my field :-)
type One = ()
type Two = Either One One
type N = [One]
type Nplus1 = Either N One
type NplusN = Either N N
type NtimesN = (N,N)
type NpowN = [N]
type NpowNplusN = Either NpowN N
s/instance of ()/instance of Ord/
Post a Comment