-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathconclusion.tex
52 lines (45 loc) · 2.66 KB
/
conclusion.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
\chapter{Conclusion}
\label{cha:conclusion}
Many generic programming approaches have problems representing
parametrized types in a meaningful way. Some resort to duplicating the
generic machinery once for the different kinds of the data types they
wish to represent. This leads to code duplication, something generic
programming set out to avoid.
We have developed an extension to the fixed point view on data types
that can represent an arbitrary number of type parameters in a
meaningful way. It uses an container that is indexed by the type
parameter position to hold elements of data types. The index is
restricted to natural numbers, defined on the type level.
This indexed container consists of two data types, one adding types to
a list of types to choose from, the other ending the list. Functions
on this container are defined by two type class instances, one on each
of these data types. Sometimes (most notably in producer functions) a
proof is needed that the index is restricted to natural numbers. We
have defined such proofs, as well as a type class to easily generate
them.
Additionally, we have integrated this approach in the multirec
library, which extends the fixed point view to allow representation of
families of mutually recursive data types. Thus, we can represent
parametrized families. This requires changing the indices on the
functors that multirec uses to type level numbers instead of concrete
types from the family. The source of the version of multirec with our
extension is available \cite{mysvn}.
One open problem is composition of types in multirec. Ideally, one
would be able to define a generic representation for lists, for
example, and later reuse this representation when representing a
family which uses lists. Currently this is only possible by defining
the list representation in the family itself, duplicating the work.
A limitation of the current approach of integrating our extension with
multirec, is that the family is parametrized, not the separate types.
This means that if a type occurs multiple times in a family, each time
applied to different parameters, we cannot represent it. It might be
possible to solve this problem by explicitly representing type
abstraction and application, instead of tagging the parameters of
the family.
Both multirec and our extension use the notion of indexed functors.
These are related to the indexed containers described in
\cite{indexedcontainers}. Similar indexed functors for generic
programming in Haskell are being developed by Conor McBride. In the
future, the combination of these ideas will hopefully lead to a
generic programming library that can conveniently represent an even
larger range of Haskell data types.