Datatype-generic Programming in Haskell
An introduction
Andres Löh
Well-Typed LLP

30 May 2011

Haven’t you ever wondered
how deriving works?

Equality on binary trees

data T = L | N T T
Let’s try ourselves:Equality on binary trees

data T = L | N T T
Let’s try ourselves:eqT :: T → T → BooleqT L
L= TrueeqT (N x1 y1 ) (N x2 y2 ) = eqT x1 x2 ∧ eqT y1 y2= FalseeqTEquality on binary trees

data T = L | N T T
Let’s try ourselves:eqT :: T → T → BooleqT L
L= TrueeqT (N x1 y1 ) (N x2 y2 ) = eqT x1 x2 ∧ eqT y1 y2= FalseeqTEasy enough, let’s try another . . .

Equality on another type

data Choice = I Int | C Char | B Choice Bool | S ChoiceEquality on another type

data Choice = I Int | C Char | B Choice Bool | S Choice

eqChoice :: Choice → Choice → BooleqChoice (I n1) (I n2) = eqInt n1 n2
eqChoice (C c1 ) (C c2 ) = eqChar c1 c2
eqChoice (B x1 b1 ) (B x2 b2 ) = eqChoice x1 x2 ∧ eqBool b1 b2
eqChoice= FalseEquality on another type

data Choice = I Int | C Char | B Choice Bool | S Choice

eqChoice :: Choice → Choice → BooleqChoice (I n1) (I n2) = eqInt n1 n2
eqChoice (C c1 ) (C c2 ) = eqChar c1 c2
eqChoice (B x1 b1 ) (B x2 b2 ) = eqChoice x1 x2 ∧ eqBool b1 b2
eqChoice= FalseDo you see a pattern?

A pattern for defining equality

I How many cases does the function definition have?
I What is on the right hand sides?

A pattern for defining equality

I How many cases does the function definition have?
I What is on the right hand sides?
I How many clauses are there in the conjunctions on eachright hand side?

A pattern for defining equality

I How many cases does the function definition have?
I What is on the right hand sides?
I How many clauses are there in the conjunctions on eachright hand side?
Relevant concepts:
I number of constructors in datatype,
I number of fields per constructor,
I recursion leads to recursion,
I other types lead to invocation of equality on those types.

More datatypes
data Tree a = Leaf a | Node (Tree a) (Tree a)
Like before, but with labels in the leaves.
How to define equality now?

More datatypes
data Tree a = Leaf a | Node (Tree a) (Tree a)
Like before, but with labels in the leaves.
How to define equality now?
We need equality on a !

More datatypes
data Tree a = Leaf a | Node (Tree a) (Tree a)
Like before, but with labels in the leaves.
How to define equality now?
We need equality on a !
eqTree :: (a → a → Bool) → Tree a → Tree a → BooleqTree eqa (Leaf n1) (Leaf n2) = eqa n1 n2
eqTree eqa (Node x1 y1 ) (Node x2 y2 ) = eqTree eqa x1 x2 ∧eqTree eqa y1 y2
eqTree eqa= FalseType classes

Note how the definition of eqTree is perfectly suited for a typeclass instance:
instance Eq a ⇒ Eq (Tree a) where(==) = eqTree (==)

Type classes

Note how the definition of eqTree is perfectly suited for a typeclass instance:
instance Eq a ⇒ Eq (Tree a) where(==) = eqTree (==)
In fact, type classes are usually implemented as dictionaries,
and an instance declaration is translated into a dictionarytransformer.

Yet another equality function
This is often called a rose tree:
data Rose a = Fork a [Rose a]Yet another equality function
This is often called a rose tree:
data Rose a = Fork a [Rose a]
Let’s assume we already have:eqList :: (a → a → Bool) → [a] → [a] → BoolHow to define eqRose ?

Yet another equality function
This is often called a rose tree:
data Rose a = Fork a [Rose a]
Let’s assume we already have:eqList :: (a → a → Bool) → [a] → [a] → BoolHow to define eqRose ?
eqRose :: (a → a → Bool) → Rose a → Rose a → BooleqRose eqa (Fork x1 xs1 ) (Fork x2 xs2 ) =eqa x1 x2 ∧ eqList (eqRose eqa) xs1 xs2
No fallback case needed because there is only one constructor.

More concepts

I Parameterization of types is reflected by parameterizationof the functions.
I Application of parameterized types is reflected byapplication of the functions.

The equality pattern
An informal description

In order to define equality for a datatype:
I introduce a parameter for each parameter of the datatype,
I introduce a case for each constructor of the datatype,
I introduce a final catch-all case returning

False ,

I for each of the other cases, compare the constructor fields

pair-wise and combine them using (∧) ,I for each field, use the appropriate equality function;

combine equality functions and use the parameter
functions as needed.

The equality pattern
An informal description

In order to define equality for a datatype:
I introduce a parameter for each parameter of the datatype,
I introduce a case for each constructor of the datatype,
I introduce a final catch-all case returning

False ,

I for each of the other cases, compare the constructor fields

pair-wise and combine them using (∧) ,I for each field, use the appropriate equality function;

combine equality functions and use the parameter
functions as needed.
If we can describe it, can we write a program to do it?

Interlude:
type isomorphisms

Isomorphism between types

Two types A and B are called isomorphic if we havefunctionsf :: A → B
g :: B → A
that are mutual inverses, i.e., if
f ◦ g ≡ idg ◦ f ≡ id

Example
Lists and Snoc-lists are isomorphic

data SnocList a = Lin | SnocList a :> aExample
Lists and Snoc-lists are isomorphic

data SnocList a = Lin | SnocList a :> alistToSnocList :: [a] → SnocList a
listToSnocList [ ]= LinlistToSnocList (x : xs) = listToSnocList xs :> x
snocListToList :: SnocList a → [a]snocListToList Lin= []snocListToList (xs :> x ) = x : snocListToList xs
We can prove that these are inverses.

The idea of datatype-generic programming
If we can represent a type as an isomorphic type that iscomposed out of a limited number of type constructors, then we
can define a function on each of the type constructors and gain
a function that works on the original type – and in fact on any
representable type.

The idea of datatype-generic programming
If we can represent a type as an isomorphic type that iscomposed out of a limited number of type constructors, then we
can define a function on each of the type constructors and gain
a function that works on the original type – and in fact on any
representable type.
In fact, we do not even quite need an isomorphic type.
For a type A , we need a type B and from :: A → B andto :: B → A such thatto ◦ from ≡ id
We call such a combination an embedding-projection pair.

Choice between constructors
Which type best encodes choice between constructors?

Choice between constructors
Which type best encodes choice between constructors?
Well, let’s restrict to two constructors first.

Choice between constructors
Which type best encodes choice between constructors?
Well, let’s restrict to two constructors first.
Booleans encode choice, but do not provide information what
the choice is about.

Choice between constructors
Which type best encodes choice between constructors?
Well, let’s restrict to two constructors first.
Booleans encode choice, but do not provide information what
the choice is about.
data Either a b = Left a | Right a

Choice between constructors
Which type best encodes choice between constructors?
Well, let’s restrict to two constructors first.
Booleans encode choice, but do not provide information what
the choice is about.
data Either a b = Left a | Right a
Choice between three things:
type Either3 a b c = Either a (Either b c)

Combining constructor fields

Which type best encodes combining fields?

Combining constructor fields

Which type best encodes combining fields?
Again, let’s just consider two of them.

Combining constructor fields

Which type best encodes combining fields?
Again, let’s just consider two of them.
data (a, b) = (a, b)

Combining constructor fields

Which type best encodes combining fields?
Again, let’s just consider two of them.
data (a, b) = (a, b)
Combining three fields:
type Triple a b c = (a, (b, c))What about constructors without arguments?

We need another type.

What about constructors without arguments?

We need another type.
Well, how many values does a constructor without argument
encode?

What about constructors without arguments?

We need another type.
Well, how many values does a constructor without argument
encode?
data () = ()Representing types

Representing types
To keep representation and original types apart, let’s define
isomorphic copies of the types we need:data U=U
data a :+: b = L a | R bdata a :∗ : b = a :∗: b

Representing types
To keep representation and original types apart, let’s define
isomorphic copies of the types we need:data U=U
data a :+: b = L a | R bdata a :∗ : b = a :∗: b
We can now get started:
data Bool = False | True
How do we represent Bool ?

Representing types
To keep representation and original types apart, let’s define
isomorphic copies of the types we need:data U=U
data a :+: b = L a | R bdata a :∗ : b = a :∗: b
We can now get started:
data Bool = False | True
How do we represent Bool ?
type RepBool = U :+: U

A class for representable types

class Representable a wheretype Rep afrom :: a → Rep a
to :: Rep a → a

A class for representable types

class Representable a wheretype Rep afrom :: a → Rep a
to :: Rep a → a
The type Rep is an associated type. GHC allows us to define
datatypes and type synonyms within classes, depending on theclass parameter(s).

Representable Booleansinstance Representable Bool wheretype Rep Bool = U :+: Ufrom False = L U
from True = R U
toto(L U) = False(R U) = True

Representable Booleansinstance Representable Bool wheretype Rep Bool = U :+: Ufrom False = L U
from True = R U
toto(L U) = False(R U) = True

Question
Are Bool and Rep Bool isomorphic?

Representable lists
instance Representable [a] wheretype Rep [a] = U :+: (a :∗: [a])from [ ]from (x : xs)
to
to

=L U
= R (x :∗ : xs)(L U) = [](R (x :∗ : xs)) = x : xs

Representable lists
instance Representable [a] wheretype Rep [a] = U :+: (a :∗: [a])from [ ]from (x : xs)
to
to

=L U
= R (x :∗ : xs)(L U) = [](R (x :∗ : xs)) = x : xs

Note that the representation of recursive types mentions theoriginal types – if needed, we can apply the transformation
multiple times.

Representable lists
instance Representable [a] wheretype Rep [a] = U :+: (a :∗: [a])from [ ]from (x : xs)
to
to

=L U
= R (x :∗ : xs)(L U) = [](R (x :∗ : xs)) = x : xs

Note that the representation of recursive types mentions theoriginal types – if needed, we can apply the transformation
multiple times.
Note further that we do not require Representable a .

Representable trees

instance Representable (Tree a) wheretype Rep (Tree a) = a :+: (Tree a : ∗: Tree a)from (Leaf n)=L nfrom (Node x y ) = R (x :∗: y)
to
to

(L n
) = Leaf n(R (x :∗ : y)) = Node x yRepresentable rose trees

instance Representable (Rose a) wheretype Rep (Rose a) = a :∗ : [Rose a]from (Fork x xs) = x :∗ : xs
to(x :∗ : xs ) = Fork x xs

Representing primitive types

For some types, it does not make sense to define a structuralrepresentation – for such types, we will have to define genericfunctions directly.
instance Representable Int wheretype Rep Int = Intfrom = id
to = id

Back to equality

Intermediate summary

I We have defined class

Representable that maps

datatypes to representations built up from U , (:+:) ,(:∗ :) and other datatypes.
I If we can define equality on the representation types, thenwe should be able to obtain a generic equality function.
I Let us apply the informal recipe from earlier.

Equality on sums

eqSum :: ( a→a→ Bool) →(b→b → Bool) →a :+: b → a :+: b → BooleqSum eqa eqb (L a1 ) (L a2 ) = eqa a1 a2
eqSum eqa eqb (R a1 ) (R a2 ) = eqb a1 a2= FalseeqSum eqa eqb

Equality on products

eqProd :: ( a→a→ Bool) →(b→b → Bool) →a :∗: b → a :∗ : b → BooleqProd eqa eqb (a1 : ∗: b1 ) (a2 : ∗: b2 ) =eqa a1 a2 ∧ eqb b1 b2

Equality on units

eqUnit :: U → U → BooleqUnit U U = True

What now?

A class for generic equality
class GEq a where
geq :: a → a → Bool

A class for generic equality
class GEq a where
geq :: a → a → Bool
instance (GEq a, GEq b) ⇒ GEq (a :+: b) where
geq = eqSum geq geq
instance (GEq a, GEq b) ⇒ GEq (a :∗ : b) where
geq = eqProd geq geq
instance
geq = eqUnit

GEq U

where

A class for generic equality
class GEq a where
geq :: a → a → Bool
instance (GEq a, GEq b) ⇒ GEq (a :+: b) where
geq = eqSum geq geq
instance (GEq a, GEq b) ⇒ GEq (a :∗ : b) where
geq = eqProd geq geq
instance
geq = eqUnit

GEq U

where

GEq Int

where

Instances for primitive types:
instance
geq = eqInt

Dispatching to the representation type
eq :: (Representable a, GEq (Rep a)) ⇒ a → a → Booleq x y = geq (from x) (from y)Dispatching to the representation type
eq :: (Representable a, GEq (Rep a)) ⇒ a → a → Booleq x y = geq (from x) (from y)Defining generic instances is now trivial:
instance
GEq Boolwhere
geq = eq
instance GEq a ⇒ GEq [a]wheregeq = eq
instance GEq a ⇒ GEq (Tree a) where
geq = eq
instance GEq a ⇒ GEq (Rose a) where
geq = eq

Have we wonorhave we lost?

Amount of work
Question
Haven’t we just replaced some tedious work (defining equality
for a type) by some other tedious work (defining a
representation for a type)?

Amount of work
Question
Haven’t we just replaced some tedious work (defining equality
for a type) by some other tedious work (defining a
representation for a type)?
Yes, but:
I The representation has to be given only once, and works

for potentially many generic functions.
I Since there is a single representation per type, it could be

generated automatically by some other means (compiler
support, TH).

Other generic functions

Coding and decoding

We want to define
data Bit = O | I
encode :: (Representable a, GEncode (Rep a)) ⇒ a → [Bit]decode :: (Representable a, GDecode (Rep a)) ⇒ BitParser atype BitParser a = [Bit] → Maybe (a, [Bit])such that encoding and then decoding yields the original value.

What about constructor names?
Seems that the representation we have does not provide
constructor name info.

What about constructor names?
Seems that the representation we have does not provide
constructor name info.
So let us extend the representation:
data C c a = C a
Note that c does not appear on the right hand side.

What about constructor names?
Seems that the representation we have does not provide
constructor name info.
So let us extend the representation:
data C c a = C a
Note that c does not appear on the right hand side.
But c is supposed to be in this class:class Constructor c where
conName :: t c a → String

Trees with constructors
data TreeLeaf
instance Constructor TreeLeaf where
conName = "Leaf"
data TreeNodeinstance Constructor TreeNode where
conName = "Node"Trees with constructors
data TreeLeaf
instance Constructor TreeLeaf where
conName = "Leaf"
data TreeNodeinstance Constructor TreeNode where
conName = "Node"instance Representable (Tree a) wheretype Rep (Tree a) = C TreeLeaf a :+:C TreeNode (Tree a :∗ : Tree a)from (Leaf nfrom (Node x ytoto) = L (C n)) = R (C (x :∗ : y))(L (C n)) = Leaf n(R (C (x :∗ : y))) = Node x yDefining functions on constructors

instance (GShow a, Constructor c) ⇒ GShow (C c a) where
gshow c@(C a)| null args = conName c| otherwise = "(" ++ conName c ++" "++ args ++ ")"where args = gshow aDefining functions on constructors

instance (GShow a, Constructor c) ⇒ GShow (C c a) where
gshow c@(C a)| null args = conName c| otherwise = "(" ++ conName c ++" "++ args ++ ")"where args = gshow a

instance (GEq a) ⇒ GEq (C c a) wheregeq (C x) (C y) = geq x yA library for generic programming

What we have discussed so far is available on Hackage as alibrary called instant-generics.
I

Representable instances for most prelude types.

I Template Haskell generation ofRepresentable instances.

I A number of example generic functions.
I Additional markers in the representation to distinguishpositions of type variables from other fields.

Is this the only way?

Many design choices

No!
There are lots of approaches (too many) to generic
programming in Haskell.

Many design choices

No!
There are lots of approaches (too many) to generic
programming in Haskell.
I The main question is exactly how we represent thedatatypes – we have already seen what kind of freedom
we have.
I The view dictates which datatypes we can represent easily,

and which generic functions can be defined.

Other notable approaches
Constructor-based views

The Scrap your boilerplate library takes a very simple view onvalues:C x1 ... xn
Every value in a datatype is a constructor applied to a numberof arguments.

Other notable approaches
Constructor-based views

The Scrap your boilerplate library takes a very simple view onvalues:C x1 ... xn
Every value in a datatype is a constructor applied to a numberof arguments.
Using SYB, it is easy to define traversals and queries.

Other notable approaches
Children-based views

The Uniplate library is a simplification of SYB that just shows
how in a recursive structure we can get to the children, andback from the children to the structure.
uniplate :: Uniplate a ⇒ a → ([a], [a] → a)Other notable approaches
Children-based views

The Uniplate library is a simplification of SYB that just shows
how in a recursive structure we can get to the children, andback from the children to the structure.
uniplate :: Uniplate a ⇒ a → ([a], [a] → a)
While a bit less powerful than SYB, this is one of the simplest
Generic Programming libraries around, and allows to define thesame kind of traversals and queries as SYB.

Other notable approaches
Fixed-point views

The regular and multirec libraries work with representations
that abstract from the recursion by means of a fixed-point
combinator, in addition to revealing the sums-of-productstructureOther notable approaches
Fixed-point views

The regular and multirec libraries work with representations
that abstract from the recursion by means of a fixed-point
combinator, in addition to revealing the sums-of-productstructure
data Fix f = In (f (Fix f))out (In f) = f

Other notable approaches
Fixed-point views

The regular and multirec libraries work with representations
that abstract from the recursion by means of a fixed-point
combinator, in addition to revealing the sums-of-productstructure
data Fix f = In (f (Fix f))out (In f) = f
Using a fixed-point view, we can more easily capture functions
that make use of the recursive structure of a type, such as folds
and unfolds (catamorphisms and anamorphisms).

GHC implementation

An approach that is quite similar to instant-generics has justbeen implemented directly in GHC, and will be available in theupcoming 7.2.1 release together with the Hackage librarygeneric-deriving.

GHC implementation

An approach that is quite similar to instant-generics has justbeen implemented directly in GHC, and will be available in theupcoming 7.2.1 release together with the Hackage librarygeneric-deriving.
With this approach, GHC can automatically (without using TH)
generate the representations for you.

Outlook: dependent types
Dependently typed programming languages such as Agda
allow types to depend on terms. For example,
Vec Int 5
could be a vector of integers of length 5 .

Outlook: dependent types
Dependently typed programming languages such as Agda
allow types to depend on terms. For example,
Vec Int 5
could be a vector of integers of length 5 .
We can also compute types from values, then. So we candefine grammars of types as normal datatypes, and interpretthem as the types they describe.

Outlook: dependent types
Dependently typed programming languages such as Agda
allow types to depend on terms. For example,
Vec Int 5
could be a vector of integers of length 5 .
We can also compute types from values, then. So we candefine grammars of types as normal datatypes, and interpretthem as the types they describe.
Makes it easy to play with many different views (universes).

Other topics

There is more than we can cover in this lecture:
I Looking at all the other GP approaches closely.
I Comparison with template meta-programming.
I Efficiency of generic functions.
I Type-indexed types.
I ...

Questions?