Haskell type-level programming using functional dependencies and type families

FunDep.hs

{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

-- Type-level functions using functional dependencies

module DepFun where

data Zero
data Succ a

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three

zero = undefined :: Zero
one = undefined :: One
two = undefined :: Two
three = undefined :: Three
four = undefined :: Four
sixteen = mult four four

class Add a b c | a b -> c where
    add :: a -> b -> c
    add _ _ = undefined

instance Add Zero b b
instance Add One b (Succ b)
instance Add a b c => Add (Succ a) b (Succ c)

class Minus a b c | a b -> c where
    minus :: a -> b -> c
    minus _ _ = undefined

instance Minus a Zero a
instance Minus a b (Succ c) => Minus a (Succ b) c

class Val a where val :: a -> Integer
instance Val Zero where val = const 0
instance Val a => Val (Succ a) where
    val x = 1 + val prev
        where prev = minus x one

class Mult a b c | a b -> c where
    mult :: a -> b -> c
    mult _ _ = undefined

instance Mult Zero a Zero
instance Mult One a a
instance (Mult a b d, Add b d c) => Mult (Succ a) b c

foo = print 16
bar = print . val $ mult four four

main = foo >> bar

TypeFam.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

data Zero
data Succ a

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three

zero = undefined :: Zero
one = undefined :: Succ Zero
two = undefined :: Succ One
three = undefined :: Succ Two
four = undefined :: Succ Three
sixteen = mult four four

type family Add a b
type instance Add Zero b = b
type instance Add (Succ a) b = Succ (Add a b)

type family Minus a b
type instance Minus a Zero = a
type instance Minus (Succ a) (Succ b) = Minus a b

type family Mult a b
type instance Mult Zero a = Zero
type instance Mult (Succ a) b = Add (Mult a b) b

add :: a -> b -> Add a b
add = undefined

minus :: a -> b -> Minus a b
minus = undefined

mult :: a -> b -> Mult a b
mult = undefined

class Value a where value :: a -> Integer

instance Value Zero where
    value = const 0

instance Value a => Value (Succ a) where
    value x = 1 + (value (minus x one))