Name
Abstract | ||
|---|---|---|
The problem of defining iteration for higher-order nested datatypes of arbitrary (finite)rank is solved within the framework of System Fω of higher-order parametric polymorphism. The proposed solution heavily relies on a general notion of monotonicity as opposed to a syntactic criterion on the shape of the type constructors such as positivity or even being polynomial. Its use is demonstrated for some rank-2 heterogeneous/nested datatypes such as powerlists and de Bruijn terms with explicit substitutions. An important feature is the availability of an iterative definition of the mapping operation (the functoriality)for those rank-1 type transformers (i. e., functions from types to types)arising as least fixed-points of monotone rank-2 type transformers. Strong normalization is shown by an embedding into Fω. The results dualize to greatest fixed-points, hence to coinductive constructors with coiteration. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1007/3-540-39185-1_1 | TYPES |
Keywords | Field | DocType |
system f,rank-2 type transformer,nested datatypes,greatest fixed-points,rank-1 type transformer,higher-order nested datatypes,de bruijn term,higher-order parametric polymorphism,explicit substitution,defining iteration,higher order,parametric polymorphism | Discrete mathematics,Inductive type,Polynomial,Computer science,Parametric polymorphism,Algorithm,Type theory,Data type,De Bruijn sequence,Monotone polygon,Type constructor | Conference |
Volume | ISSN | ISBN |
2646 | 0302-9743 | 3-540-14031-X |
Citations | PageRank | References |
6 | 0.47 | 14 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Abel | 1 | 131 | 9.57 |
| Ralph Matthes | 2 | 201 | 21.67 |