Name
Abstract | ||
|---|---|---|
In this paper we use the Epigram language to define the universe of regular tree types—closed under empty, unit, sum, product and least fixpoint. We then present a generic decision procedure for Epigram's in-built equality at each type, taking a complementary approach to that of Benke, Dybjer and Jansson [7]. We also give a generic definition of map, taking our inspiration from Jansson and Jeuring [21]. Finally, we equip the regular universe with the partial derivative which can be interpreted functionally as Huet's notion of ‘zipper', as suggested by McBride in [27] and implemented (without the fixpoint case) in Generic Haskell by Hinze, Jeuring and Löh [18]. We aim to show through these examples that generic programming can be ordinary programming in a dependently typed language. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/11617990_16 | TYPES |
Keywords | Field | DocType |
generic haskell,ordinary programming,generic programming,complementary approach,fixpoint case,regular universe,regular tree type,generic definition,epigram language,generic decision procedure,dependent types | Programming language,Functional programming,Computer science,Algorithm,Type theory,Zipper,Haskell,Declarative programming,Fixed point,Generic programming,Type constructor | Conference |
Volume | ISSN | ISBN |
3839 | 0302-9743 | 3-540-31428-8 |
Citations | PageRank | References |
15 | 0.80 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Morris | 1 | 15 | 0.80 |
| Thorsten Altenkirch | 2 | 668 | 56.85 |
| Conor McBride | 3 | 752 | 47.89 |