WebHome
- Education Page?
- Description?
- Literature?
- Schedule?
- Assignments?

Center
Master Program
Generics Examples

Uhc
%X% _This is work in progress_ %X%
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.
<verbatim>
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   
</verbatim>
Some properties:
   * The function _(==)_ can only be used on types which are instances of _Eq_. 
   * %X% Generic functions can only be defined on types of kind *. 
   * %Y% We can override an generic definition for specific types and give our own implementation for equals (see the equality on Set). 
   * %X% 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.
<verbatim>
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 
</verbatim>
Some properties we see here:
   * %Y% Generic functions can be applied to all types. 
   * %Y% Generic functions can be defined on types of all kinds.
   * %X% Explicit type annotation everywere. _not a very good description_
   * %X% Explicit passing of recursive functions.
   * %Y% Easy replacement of recursive functions. _not a very good description_
   * %X% For types of different kinds we have different signatures.
   * %Y% We can overide generic functions for specific types. 

---+++ Dependency-style Haskell
<verbatim>
eq{| t |} :: (generalize{| &delta;a |} a a' |-> (eq{| &delta;a |} a -> a' -> Bool) => a -> a' -> Bool) t t 
eq{| Unit |} Unit Unit = True
eq{| &delta;a :+: &delta;b |} (Inl a) (Inl a') = eq{| &delta;a |} a a'
eq{| &delta;a :+: &delta;b |} (Inr b) (Inr b') = eq{| &delta;b |} b b'
eq{| &delta;a :+: &delta;b |} _       _        = False
eq{| &delta;a :*: &delta;b |} (a :*: b) (a' :*: b') = eq{| &delta;a |} a a' && eq{| &delta;b |} b b'

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

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

eq{| [Int] |} :: [Int] -> [Int] -> Bool
eq{| [&delta;a] |} :: forall b b'. (eq{|&delta;a|} :: b -> b' -> Bool) => [b] -> [b'] -> Bool      
</verbatim>
Some properties we see here:
   * %Y% Generic functions can be applied to all types. 
   * %Y% Generic function can be defined on types of all kinds.
   * %X% Explicit type annotation everywere.
   * %Y% *No* explicit passing of recursive functions.
   * %Y% Easy replacement of recursive functions.
   * %Y% For every use of the generic function we have the *same* number of arguments (but context might differ).
   * %Y% We can overide generic functions for specific types. 

---+++ Generic UHC 
Goal: Combinate dependency-style generics and derivable type classes. 
<verbatim>
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 &delta;a where 
      x == x = toUpper x == toUpper y 
  in (=={|[&delta;a]|} "uhc" "UHC"
True
</verbatim>

---++ Generic map
---+++ Derivable Type Classes 
We can't implement a generic _map_ using derivable type classes. _more needed..._

---+++ Classic Generic Haskell
<verbatim>
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]
</verbatim>

---+++ Dependency-style Generic Haskell
<verbatim>
gmap{| t |} :: (generalize{| &delta;a |} b b' |-> (gmap{| &delta;a |} :: (b -> b')) =>  b -> b') t t 
gmap{| Unit |} = Unit
gmap{| &delta;a :+: &delta;b |} (Inl a) = (Inl gmap{| &delta;a |} a)
gmap{| &delta;a :+: &delta;b |} (Inr a) = (Inr gmap{| &delta;b |} b)
gmap{| &delta;a :*: &delta;b |} (a :*: b) = gmap{| &delta;a |} a :*: gmap{| &delta;b |} b

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

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

gmap{| String |} :: String -> String
gmap{| [&delta;a] |} :: (map{| &delta;a |} :: b -> c) => [b] -> [c]    
</verbatim>

---+++ Generic UHC
<verbatim>
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 &delta;a where
     gmap = toUpper
  in gmap{| [&delta;a] |} "hello world"
"HELLO WORLD"
</verbatim>

-- Main.ArjanOosting - 06 Oct 2003