{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
-- By Jesse Tov (ccs.neu.edu!tov), November 2007
-- This is a DRAFT.  Later versions at http://www.ccs.neu.edu/home/tov/.
module Types (
  bot,
  Fail,
  T, F, Prop, OrProp(..),
  Equal(..),
  S, Z, Nat,
  LeNat(..),
) where

bot = undefined

-- Errors:
class Fail x

-- Props:

data T
data F

class Prop a
instance Prop T
instance Prop F

class OrProp a b c | a b -> c where
  orProp :: a -> b -> c
  orProp _ _ = bot
instance OrProp T T T
instance OrProp F T T
instance OrProp T F T
instance OrProp F F F

-- Type reflection and equality:

class Prop b => Equal x y b | x y -> b where
  equal :: x -> y -> b
  equal _ _ = bot

-- Nats:

data Z
data S x

class Nat a where
  reflectNat :: a -> Integer
instance Nat Z where
  reflectNat _ = 0
instance Nat n => Nat (S n) where
  reflectNat _ = 1 + reflectNat (undefined :: n)

instance Show Z where
  show = show . reflectNat
instance (Nat n) => Show (S n) where
  show = show . reflectNat

instance Equal Z Z T
instance Nat n => Equal (S n) Z F
instance Nat n => Equal Z (S n) F
instance (Nat n1, Nat n2, Equal n1 n2 b) => Equal (S n1) (S n2) b

class (Nat n1, Nat n2, Prop b) => LeNat n1 n2 b | n1 n2 -> b where
  leNat    :: n1 -> n2 -> b
  leNat _ _ = bot
instance Nat n2 => LeNat Z n2 T
instance Nat n1 => LeNat (S n1) Z F
instance LeNat n1 n2 b => LeNat (S n1) (S n2) b