skip to main |
skip to sidebar
## Friday, July 20, 2007

## About Me

## Labels

A blog about typed programming

Subscribe to:
Post Comments (Atom)

- GADTs (7)
- constructive logic (6)
- ordinals (6)
- Haskell (5)
- Leibniz equality (3)
- Simulating Dependent Types with Guarded Algebraic Datatypes (3)
- countability (3)
- C++ (2)
- Coq (2)
- GHC (2)
- Heyting algebra (2)
- V=L (2)
- _|_ (2)
- dependent types (2)
- effect inference (2)
- effects (2)
- lightweight static capabilities (2)
- nested types (2)
- quotient types (2)
- referential transparency (2)
- zero-knowledge proof (2)
- CPOs (1)
- Dependent ML (1)
- Fomega (1)
- Liskov substitutability (1)
- ML (1)
- OOP (1)
- bugs (1)
- cardinal numbers (1)
- conferences (1)
- continuity (1)
- copious free time (1)
- definability (1)
- flow caml (1)
- fuzzy logic (1)
- grammar checking (1)
- impredicativity (1)
- information flow (1)
- kinds (1)
- laypeople (1)
- morphisms (1)
- parallel or (1)
- polymorphism (1)
- refinement types (1)
- sized lists (1)
- static analysis (1)
- termination (1)
- type disequality (1)

## 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