import Data.Bits

-- kolekce

class Collection c a | c -> a where
  create::[a] -> c
  contains::c -> a -> Bool

instance Eq a => Collection [a] a where
  create = id
  contains s e = e `elem` s

instance Collection Integer Int where
 create [] = 0
 create (h : t) = (shift 1 h) + create t
 contains s e = (shift 1 e .&. s) /= 0

-- aritmetika

data Zero = Zero
data Succ a = Succ a
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four
type Six = Succ Five
type Seven = Succ Six
type Eight = Succ Seven
type Nine = Succ Eight 
type Ten = Succ Nine

class IsNum n where
  showNum::n->Int
instance IsNum Zero where
  showNum _ = 0
instance IsNum a => IsNum (Succ a) where
  showNum _ = 1 + showNum (undefined :: a)

class Plus a b c | a b -> c where
  plus::a->b->c
  plus=undefined
instance Plus Zero a a where
instance Plus x a y => Plus (Succ x) a (Succ y) where

class Krat a b c | a b -> c where
  krat::a->b->c
  krat=undefined
instance Krat Zero a Zero where
instance (Krat x a y, Plus y a z) => Krat (Succ x) a z where

-- obecne k-tice

data T x y = T x y deriving (Show)

class Sel t n x | t n -> x where
  sel::t->n->x
instance Sel (T x y) Zero x where
  sel (T a _) _ = a
instance Sel y n x => Sel (T a y) (Succ n) x where
  sel (T _ y) _ = sel y (undefined::n)

class Cons f t x | t x -> f where
  consM::(t->x)->f

instance Cons x () x where
  consM m = m ()

instance Cons f b x => Cons (a->f) (T a b) x where
  consM m a = consM (\b -> m (T a b))

typedId::a->a->a
typedId _ x = x

cons::Cons f t t => t->f
cons typ = consM (typedId typ)

-- consM id nefunguje, protoze typ id je forall a . a -> a, a z f neplyne t

type T1 x = T x ()
t1::T1 x
t1 = undefined
type T2 x y = T x (T1 y)
t2::T2 x y
t2 = undefined
type T3 x y z = T x (T2 y z)
t3::T3 x y z
t3 = undefined
type T4 x y z u = T x (T3 y z u)
t4::T4 x y z u
t4 = undefined
type T5 x y z u v = T x (T4 y z u v)
t5::T5 x y z u v
t5 = undefined

class Spoj x y z | x y -> z where
  spoj::x->y->z

instance Spoj () x x where
  spoj () t = t

instance Spoj b x y => Spoj (T a b) x (T a y) where
  spoj (T a b) x = T a (spoj b x)