tag:blogger.com,1999:blog-6839602.post7868504782448649445..comments2017-03-09T15:26:17.288-08:00Comments on Everyone Else is Crazy: Ordinal Notation and Computer ProofJim Applehttp://www.blogger.com/profile/11080395413026172939noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-6839602.post-17216135598686254152007-07-20T21:26:00.000-07:002007-07-20T21:26:00.000-07:00s/instance of ()/instance of Ord/s/instance of ()/instance of Ord/sigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-6839602.post-24608338165392199942007-07-20T21:25:00.000-07:002007-07-20T21:25:00.000-07:00Funny you should post that. I just wrote this and ...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 :-)<BR/><BR/>type One = ()<BR/>type Two = Either One One<BR/>type N = [One]<BR/>type Nplus1 = Either N One<BR/>type NplusN = Either N N<BR/>type NtimesN = (N,N)<BR/>type NpowN = [N]<BR/>type NpowNplusN = Either NpowN Nsigfpehttps://www.blogger.com/profile/08096190433222340957noreply@blogger.com