Typelevel.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Typelevel where

import Prelude hiding (sum)

-- type-level natural numbers
data Zero = Zero
data Succ a = Succ a

class ToInt a where
  toInt :: a -> Int

class Sum a b c | a b -> c, a c -> b where

instance Sum Zero b b where

instance Sum a b c => Sum (Succ a) b (Succ c) where

two = Succ (Succ Zero)
three = Succ two

sum :: Sum a b c => a -> b -> c
sum _ _ = undefined :: c

-- load this into ghci and input ":t sum two three"