Generics Examples

This is work in progress On this page I will give some examples of generic functions written in different styles. I will show the differences between the styles and show what the shortcomings of the different styles are.

Then I will try to describe a form of generic programming which combines the strong points of the different styles and is built on the class system of Haskell.

Generic equals

Derivable Type Classes

Below we see a type class Eq with an generic default method for equality. We also see an instance declaration on lists after which we can use the equality function on lists.

class Eq t where
  (==), (/=) :: t -> t -> Bool
  (==){| Unit |} Unit Unit = True
  (==){| a :+: b |} (Inl x) (Inl x') = x == x'
  (==){| a :+: b |} (Inr y) (Inr y') = y == y'
  (==){| a :+: b |} _        _       = False
  (==){| a :*: b |} (x :*: y) (x' :*: y') = x == x' && y == y'

instance Eq t => Eq [t]
instance Eq a => Eq (Set a) where
  s == s' = s `subset` s' && s' `subset` s
  
> eq [1,2,3] [1,2,3]
True

eq :: (Eq t) => t -> t -> Bool   

Some properties:

• The function (==) can only be used on types which are instances of Eq.
• Generic functions can only be defined on types of kind *.
• We can override an generic definition for specific types and give our own implementation for equals (see the equality on Set).
• We cannot locally redefine our generic function. For instance we cannot locally redefine our equals function on characters to do an case insensitive comparision.

Classic Generic Haskell

Below we see a generic defination for equals and how we can use it in Generic Haskell. We also see how we can use the generic definition.

type Eq{[ * ]} t t'      = t -> t' -> Bool
type Eq{[ k -> l ]} t t' = forall u u'. Eq{[ k ]} u u' -> Eq{[ l ]} (t u) (t' u')

(==){| t::k |} :: Eq{[ k ]} t t
(==){| Unit |} Unit Unit = True
(==){| :+: |} eqA eqB (Inl a) (Inl a') = eqA a a'
(==){| :+: |} eqA eqB (Inr b) (Inr b') = eqB b b'
(==){| :+: |} eqA eqB  _       _       = False
(==){| :*: |} eqA eqB (a :*: b) (a' :*: b') = eqA a a' && eqB b b'   

(==){| Set a |} eqA eqB s s' = s `subset` s' && s' `subset` s
 
> eq{| [Int] |} [1,2,3] [1,2,3]  
True
> let f x y = toUpper x == toUpper y in eq{| [] |} f "uhc" "UHC"
True 

eq{| [Int] |} :: [Int] -> [Int] -> Bool
eq{| [] |}    :: (a -> b -> Bool) -> [a] -> [b] -> Bool 

Some properties we see here:

• Generic functions can be applied to all types.
• Generic functions can be defined on types of all kinds.
• Explicit type annotation everywere. not a very good description
• Explicit passing of recursive functions.
• Easy replacement of recursive functions. not a very good description
• For types of different kinds we have different signatures.
• We can overide generic functions for specific types.

Dependency-style Haskell

eq{| t |} :: (generalize{| δa |} a a' |-> (eq{| δa |} a -> a' -> Bool) => a -> a' -> Bool) t t 
eq{| Unit |} Unit Unit = True
eq{| δa :+: δb |} (Inl a) (Inl a') = eq{| δa |} a a'
eq{| δa :+: δb |} (Inr b) (Inr b') = eq{| δb |} b b'
eq{| δa :+: δb |} _       _        = False
eq{| δa :*: δb |} (a :*: b) (a' :*: b') = eq{| δa |} a a' && eq{| δb |} b b'

eq{| Set δa |}  s s' = s `subset` s' && s' `subset` s

> eq{| [Int] |} [1,2,3] [1,2,3]
True
> let eq{| δa |} x y = toUpper x == toUpper y in eq{| [δa] |} "uhc" "UHC"
True

eq{| [Int] |} :: [Int] -> [Int] -> Bool
eq{| [δa] |} :: forall b b'. (eq{|δa|} :: b -> b' -> Bool) => [b] -> [b'] -> Bool      

Some properties we see here:

• Generic functions can be applied to all types.
• Generic function can be defined on types of all kinds.
• Explicit type annotation everywere.
• No explicit passing of recursive functions.
• Easy replacement of recursive functions.
• For every use of the generic function we have the same number of arguments (but context might differ).
• We can overide generic functions for specific types.

Generic UHC

Goal: Combinate dependency-style generics and derivable type classes.

class Eq t where
  (==), (/=) :: t -> t -> Bool
  (==){| Unit |} Unit Unit = True
  (==){| a :+: b |} (Inl x) (Inl x') = x == x'
  (==){| a :+: b |} (Inr y) (Inr y') = y == y'
  (==){| a :+: b |} _        _       = False
  (==){| a :*: b |} (x :*: y) (x' :*: y') = x == x' && y == y'

instance Eq (Set a) where
  s == s' = s `subset` s' && s' `subset` s

>[1,2,3] == [1,2,3]
True
> let instance Eq δa where 
      x == x = toUpper x == toUpper y 
  in (=={|[δa]|} "uhc" "UHC"
True

Generic map

Derivable Type Classes

We can't implement a generic map using derivable type classes. more needed...

Classic Generic Haskell

type Map {[ * ]} t1 t2 = t1 -> t2
type Map {[ k -> l ]} t1 t2 = forall u1 u2. Map {[ k ]} u1 u2 -> Map {[ l ]} (t1 u1) (t2 u2)

gmap {| t :: k |} :: Map {[ k ]} t t
gmap {| Unit |} = id
gmap {| :+: |} gmapA gmapB (Inl a)     = Inl (gmapA a)
gmap {| :+: |} gmapA gmapB (Inr b)     = Inr (gmapB b)
gmap {| :*: |} gmapA gmapB (a :*: b)   = (gmapA a) :*: (gmapB b)

fmap{| t :: * -> * |} f = gmap {| t |} f 

> gmap{| String |} "hello world"
"hello world"
> gmap{| [] |} toUpper "hello world"
"HELLO WORLD"
> fmap toUpper "hello world"
"HELLO WORLD"

gmap{| String |} :: String -> String
gmap{| [] |}::(a -> b) -> [a] -> [b]

Dependency-style Generic Haskell

gmap{| t |} :: (generalize{| δa |} b b' |-> (gmap{| δa |} :: (b -> b')) =>  b -> b') t t 
gmap{| Unit |} = Unit
gmap{| δa :+: δb |} (Inl a) = (Inl gmap{| δa |} a)
gmap{| δa :+: δb |} (Inr a) = (Inr gmap{| δb |} b)
gmap{| δa :*: δb |} (a :*: b) = gmap{| δa |} a :*: gmap{| δb |} b

fmap{| t:: * -> * |} f x = let gmap{| δa |} = f in gmap {| t δa |} x 

> gmap{| String |} "hello world"   
"hello world"
> let gmap{| δa |} = toUpper in gmap{| [δa] |} "hello world"
"HELLO WORLD"
> fmap toUpper "Hello world"
"HELLO WORLD"

gmap{| String |} :: String -> String
gmap{| [δa] |} :: (map{| δa |} :: b -> c) => [b] -> [c]    

Generic UHC

class GMap t where 
   gmap :: t -> t 
   gmap{| Unit |} Unit = Unit
   gmap{| a :+: b |} (Inl a) = Inl (gmap a)
   gmap{| a :+: b |} (Inr b) = Inr (gmap b)
   gmap(| a :*: b |} (a :*: b) = gmap a :*: gmap b

> let instance GMap δa where
     gmap = toUpper
  in gmap{| [δa] |} "hello world"
"HELLO WORLD"

-- ArjanOosting - 06 Oct 2003