An open and shut typecase.
Two different ways of defining ad-hoc polymorphic operations commonly occur in programming languages. With the first form polymorphic operations are defined inductively on the structure of types while with the second form polymorphic operations are defined for specific sets of types.In intensional type analysis operations are defined by induction on the structure of types. Therefore no new cases are necessary for user-defined types, because these types are eQuivalent to their underlying structure. However, intensional type analysis is "closed" to extension, as the behavior of the operations cannot be differentiated for the new types, thus destroying the distinctions that these types are designed to express.Haskell type classes on the other hand define polymorphic operations for sets of types. Operations defined by class instances are considered "open"---the programmer can add instances for new types without modifying existing code. However, the operations must be extended with specialized code for each new type, and it may be tedious or even impossible to add extensions that apply to a large universe of new types.Both approaches have their benefits, so it is important to let programmers decide which is most appropriate for their needs. In this paper, we define a language that supports both forms of ad-hoc polymorphism, using the same basic constructs.
INTRODUCTION
With ad-hoc polymorphism the execution of programs depends
on type information. A parametrically polymorphic
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, to
republish, to post on servers or to redistribute to lists, requires prior specific
permission and/or a fee.
September 19-22, 2004, Snowbird, Utah.
function must behave the same for all instantiations. How-
ever, the instance of an ad-hoc polymorphic function for integers
may behave di#erently from the instance for booleans.
We call functions that depend on type information type-directed

Ad-hoc polymorphism is a compelling addition to a typed
programming language. It is well suited for dynamic environments
where it can be used to implement dynamic typ-
ing, dynamic loading and marshalling. It is also essential to
the definition of generic versions of many basic operations
such as equality and structural traversals. In particular,
ad-hoc polymorphism simplifies programming with complicated
data structures, eliminating the need for repetitive
"boilerplate code". For example, the implementation of a
compiler may include many data structures for representing
intermediate languages and many passes over these data
structures. Without type-directed programming, the same
code for traversing abstract syntax must be implemented for
each intermediate language. The generic traversals defined
by ad-hoc polymorphism allow the programmer to concentrate
on the important parts of a transformation.
Currently, there are two forms of ad-hoc polymorphism
in typed, functional languages. The first is based on the
nominal analysis of type information, such as Haskell type
classes [30]. The execution of an ad-hoc operation is determined
solely by the name of the type argument (or the name
of its head constructor, such as list.)
For example, we may use type to implement a polymorphic
structural equality. The type class declares that there
is a type-directed operation called eq and each instance of
the class describes how eq behaves for that type. For composite
types, such as products and lists, equality is defined
in terms of equality for the components of the type.
class Eq a where
eq :: a -> a -> Bool
instance Eq Int where
instance Eq Bool where
instance (Eq a, Eq b) => Eq (a,b) where
instance (Eq a) => Eq [a] where
Nominal analysis naturally limits the domain of an ad-hoc
operation to those types where a definition has been
provided. For example, eq is not defined for function types.
Type-directed operations in a nominal framework are naturally
"open"; at any time they may be extended with instances
for new types, without modifying existing code.
The second form of ad-hoc polymorphism is based on the
structural analysis of types. For example, intensional type
analysis [11] allows programmers to define type-directed operations
by case analysis of the type structure. Polymorphic
equality defined by run-time type analysis may look like the
typecase a of
Bool -> if x then y else not y
(b,c) -> eq (fst x)(fst y) && (snd x)(snd y)
(b->c) -> error "eq not defined for functions"
Because type-directed operations are defined by case analy-
sis, they are naturally "closed" to extension. In fact, cases
for all types must be provided when such operations are
defined.
These two forms of ad-hoc polymorphism di#er in the
way that they treat user-defined types. User-defined types
such as Haskell's newtypes [23], are an important part of
many languages. Although these new types are isomorphic
to existing types, they express application-specific distinctions
that can be made by the type checker. For example,
a programmer may wish to ensure that he does not confuse
phone numbers with ages in an application, even though
both may be represented using integers.
Because nominal operations are open, they must be extended
with instances for each new user-defined type. It
may be tedious and even di#cult to add new operations
that apply to many types. Furthermore, if some types are
defined in separate inaccessible modules then it is impossible
for the programmer to extend the operation to those types.
Instead, he must rely on the definer of the type to add the
instance, and there is no guarantee that she will respect the
invariants of the type-directed operation.
On the other hand, closed operations cannot be extended
to new types. Structural systems treat new types as equal
to their definitions. This approach destroys the distinctions
that the new types are designed to express. A type-directed
operation cannot treat an age di#erently from a
phone number-both are treated as integers. While some
systems allow ad-hoc definitions for user-defined types, there
is a loss of abstraction-a type-directed operation can always
determine a type's underlying representation.
In the presence of user-defined types, neither purely nominal
nor purely structural ad-hoc polymorphism is entirely
satisfactory.
1.1 Combining both forms in one language
This paper unifies the two di#erent forms of ad-hoc polymorphism
in a foundational language, called #L . This language
provides capabilities for both structural and nominal
analysis in a coherent framework, allowing developers
to choose which characteristics they wish to use from each
system.
At the core, #L is a simple system for structural type
analysis augmented with user-defined types. The structural
analysis operator typecase may include branches for these
new names if they are in scope. Naturally, some type-directed
operations may be unable to handle some newly
defined types. Types containing names for which there is no
branch in an operation cannot be allowed as an argument, or
evaluation will become stuck. Therefore, the type system of
#L statically tracks the names used in types and compares
them to the domain of a type analysis operation.
New names are generated dynamically during execution,
so it is desirable to extend type-directed operations with
branches for these new names. For this purpose, we introduce
first-class maps from names to expressions. Intuitively,
these maps are branches for typecase that may be passed
to type-directed operations, extending them to handle the
new names. Also, #L includes support to coerce the types
of expressions so that they do not mention new type names.
We stress that we do not consider #L an appropriate
source language for humans, in much the same way that
F# is not an appropriate source language for humans. As
defined, #L requires that programs be heavily annotated and
written in a highly-stylized fashion. The next step in this
research program is to develop automated assistance for the
common idioms, such as the inference of type arguments and
first-class maps.
1.2 Contributions of this work
The #L language is an important step towards improving
the practicality of type-directed programming. In particu-
lar, this paper has the following contributions:
. We define a language that allows the definition of both
"open" and "closed" type-directed operations. Previous
work has chosen one or the other, augmented with
ad-hoc mechanisms to counter their di#culties.
. We define a language that allows programmers to statically
restrict the domain of type-directed operations
defined in a structural system in a natural manner.
Previous work [11, 4] requires that programmers use
type-level analysis or programming to makes such restrictions

. We show how to reconcile typecase with the analysis
of higher-order type constructors. Previous work [31]
has based such analysis on the interpretation of type
constructors. In #L , we show how to implement the
same operations with simpler constructs.
. We present a sophisticated system of coercions for converting
between new types and their definitions. We
extend previous work [23, 29, 26] to higher-order coercions
in the presence of type constructor isomorphisms.
The remainder of this paper is as follows. In the next section
we introduce the features of #L through examples. We
first describe the semantics of the core language in Section 3,
and then extend it to be fully reflexive in Section 4. In Section
5 we show how higher-order analysis may be defined
and discuss additional extensions in Section 6. We discuss
related work in Section 7 and conclude in Section 8.
2. PROGRAMMING IN #L
At the core, #L is a polymorphic lambda calculus
25], augmented with type analysis and user-defined types.
The syntax of #L appears in Figure 1. In addition to the
standard kinds, type constructors and terms of F#L includes
labels (l) and sets of labels (L). Labels may be considered
to be "type constants" and model both built-in types
(such as int) and user-defined types.
Kinds
Types
| l labels
| #L.# type of type-poly. terms
| #:L(# type of label-poly. terms
| #s:Ls.# type of set-poly. terms
| L1 #L2 type of typecase branches
Terms
e ::= x | #x:#.e | e1 e2 #-calculus
| i | fix x:#.e integers and recursion
| new # in e label creation
| {{e}} - l=# first-order coercion
higher-order coercion
| typecase # e type analysis
| # | {l # e} | e1 # e2 branches
| #L.e | e[#
| #:L(#).e | e[ - l] label polymorphism
| #s:Ls.e | e[L] label set polymorphism
Labels
l ::= #
variables and constants
Label sets
| # | U empty and universe
| {l} | L1 #L2 singleton and union

Figure

1: The core #L language
An important point is that #L supports run-time analysis
of type information instead of requiring that all type-directed
operations be resolved at compile time. Run-time
analysis is necessary because there are many situations
where types are not known at compile time. For example,
large programs, where the benefit of type-directed programming
is most important, are not compiled in their entirety.
Furthermore, separate compilation, dynamic loading or run-time
code generation requires run-time type analysis. Even
within a single compilation unit, not all type information
may be available at compile time because of first-class polymorphism
(where a data structure may hide some type in-
or polymorphic recursion (where each iteration
of a loop is instantiated with a di#erent type).
In the following subsections, we describe the important
features of #L in more detail.
2.1 Generative types
The #L language includes a simple mechanism for users to
define new type constants. We call all type constants labels
to emphasize the fact that they do not #-vary. Arbitrary label
constants are written as #
annotated with their kinds.
Some distinguished constants in this language are constructors
for primitive types. The label #
0 is a nullary constructor
for the type of integers, and #
1 is the the binary constructor
for function types. We use the syntactic sugar # int
and # to refer to these two labels. However, when these
labels appear in types, we use the notation int to stand for
# int and #1 #2 to stand for the function type #1 #2 . In
the examples, we extend this language with new forms of
types, such as booleans (bool), products (#1 - #2 ), and lists
(list # ), and add new label constants, written # bool , #- and
list , to form those types.
The expression new # in e creates user-defined
labels. This expression dynamically generates a new label
constant and binds it to the label variable #. Inside the
scope e, the type # is isomorphic to the type # of kind #.
The operators {{-}}
# and {{- # coerce expressions to and
from the types # and # . When # is apparent from context
we elide that annotation, as in the example below.
new
Unlike other forms of user-defined types, such as Haskell
newtypes, this mechanism dynamically creates new "types".
Generating these new labels requires an operational e#ect
at run time. However, the coercions that convert between
the new label and its definition have no run-time cost. We
chose this mechanism to model generative types in #L for
its simplicity. A more sophisticated language could base its
mechanism for type generativity on a module system.
Note that even though run-time type analysis destroys
the parametricity created by a type polymorphism (#)
users may still hide the implementation details of abstract
datatypes with these generative types. Once outside the
scope of a new label, it is impossible to determine its underlying
definition. For example, we know that the polymorphic
function f below must treat its term argument parametrically
because, even in the presence of run-time type analysis,
it cannot coerce it to the type int.
. in
new
2.2 Type analysis with a restricted domain
The term typecase # e may be used to define type-directed
operations in #L . This operator determines the
head (or outermost) label of the normal form of its type
argument # , such as # int , #- , or # list . It then selects the
appropriate branch from the finite map e from labels to ex-
pressions. For example, the expression typecase int {# int #
evaluates to 1.
The finite map in typecase may be formed from a singleton
map (such as {# int # e int }) or the join of two finite
maps e1 # e2 . In a join, if the domains are not disjoint,
the second map has precedence. Compound maps such as
are abbreviated as
A challenging part of the design of #L is ensuring that
there is a matching branch for the analyzed type. For ex-
ample, stuck expressions such as typecase bool {# int # 2}
should not type check, because there is no branch for the
boolean type (or rather its label).
For this reason, when checking a typecase expression,
#L calculates the set of labels that may appear within the
analyzed type and requires that set to be a subset of the
set of labels that have branches in typecase. Label sets
in #L may be empty, #, may contain a single label, {l},
may be the union of two label sets, L1 #L2 , or may be the
entire universe of labels, U . Analogously to finite maps,
{l1 , . , l n} abbreviates {l1 } # {ln}.
To allow type polymorphism, we annotate a quantified
type variable with the set of labels that may appear in types
that instantiate it. For example, below we know that # will
be instantiated only by a type formed from the labels # int
and # bool (i.e., by int or bool), so # will have a match in the
typecase expression.
If we annotate a type variable with U then it is unanalyzable
because no typecase can cover all branches. 1
A more realistic use of typecase is for polymorphic equal-
ity. The function eq below implements a polymorphic
equality function for data objects composed of integers,
booleans, products and lists. In the following examples, let
list }.
fix eq:(#L0 . # bool).
#L0). typecase #
{ # int # eqint,
# bool #x:bool. #y:bool.
if x then y else (not y),
#1 :#L0 . #2 :#L0 .
](fst x)(fst y)
list #L0 . #x:(list #y:(list #).
all2 (eq[#]) x y }
Product types have two subcomponents so the branch for
#- abstracts two type variables for those subcomponents.
Likewise, the # list case abstracts the type of list elements.
In general, the type of each branch in typecase is determined
by the kind of the matched label. After typecase
determines the head label of its argument, it steps to the
corresponding map branch and applies that branch to any
arguments that were applied to the head label. For exam-
ple, applying polymorphic equality to the type of integer
lists results in the # list branch being applied to int.
eq[list int] #L0 . #x:(list #y:(list #).
all2 (eq[#]) x y) [int]
#x:(list int). #y:(list int). all2 (eq[int]) x y
The ability to restrict the arguments of a polytypic function
is valuable. For example, the polytypic equality function
cannot be applied to values of function type. Here, #L
naturally makes this restriction by omitting # from the set
of labels for the argument of eq.
2.3 Generative types and type analysis
The function eq is closed to extension. However, with
the creation of new labels there may be many more types
of expressions that programmers would like to apply eq to.
In #L , we provide two solutions to this problem. We can
rewrite eq to be extensible with new branches for the new
labels. Otherwise, we can leave eq as it is and at application,
coerce all the arguments to eq so that their types do not
contain new labels.
2.3.1 Extensible type analysis
In #L , we can rewrite eq to be extensible with new
branches for new labels. Programmers may provide new
typecase branches as an additional argument to eq. The
type of this argument, a first-class map from labels to ex-
pressions, is written as L1 # L2 . The first component
1 While the flexibility of having unanalyzable types is impor-
tant, this approach is not the best way to support parametric
polymorphism-it does not allow types to be partly abstract
and partly transparent.
of this type is the domain of the map. The second and
third components are used to describe the types of these
branches. 2 Using first-class maps, we can pass a branch for
int's into the following operation:
#x:({# int }# .bool)# int }).
typecase int ({# bool # true} #x)
For simplicity, #L makes no attempt to enforce that the
domains of joined maps are disjoint. Instead, maps are or-
dered, and existing branches may be shadowed because the
rightmost matching branch will be selected. In the following
expression, if {# int # false} is supplied for x, the expression
will evaluate to false.
#x:({# int }# .bool)# int }).
typecase int ({# bool # false, # int # true} # x)
Redefining the behavior of typecase for int may not be what
the programmer intended, but allowing such a scenario does
not a#ect the soundness of #L . If the programmer wished
to prevent this redefinition, she could join x on the left.
However, even if a type-directed function abstracts a map
for typecase, it is still not extensible. The type of that
map specifies the labels that are in its domain. Branches
for newly created labels cannot be supplied. Therefore, #L
includes label-set polymorphism. A typical idiom for an extensible
operation is to abstract a set of labels, a map for
that set, and then require that the argument to the polytypic
function be composed of those labels plus any labels
that already have branches in typecase. We call functions
that have been defined in this manner "open". For exam-
ple, we can create an open version of eq as follows (again let
list }). In the code below, s is a variable
describing the domain of labels in the map y. The eq function
may be instantiated with types containing labels from
L0 or s.
#s:Ls.#y:(s# bool)#s #L0).
fix eq:# (s #L0 ). # bool.
#(s #L0). typecase #
list # .}
With this version of eq, we can treat labels di#erently from
their underlying representations. For example, if dollar
amounts are stored as floating point numbers, we can round
them to two decimal places before comparing them.
This calculus explicitly witnesses the design complexity
of open polytypic operations. Suppose we wished to call an
open operation, called important in the body of an open se-
rializer, called tostring. Intuitively, important elides part
of a data structure by deciding whether recursion should
continue. Because tostring can be applied to any type that
provides a map for new labels, important must also be
applicable to all those types.
There are two ways to write tostring. The first is to supply
the branches for important as an additional argument
2 The type of a branch is determined by the kind of the label
matched by that branch, as well as these two components.
The precise specification of that relationship appears in Section
3.
to tostring, as below.
#s:Ls.#y tos :(s # string) #s #-}).
fix tostring. #s #-}).
typecase #
(y tos #
](fst x)
then tostring[s][#1 ](fst x)
else "." in
then tostring[s][#2 ](snd x)
else "." in
"(" ++ s1 ++ "," s2 ++ ")"})
Dependency-Style Generic Haskell [20] uses this technique.
In that language, the additional arguments are automatically
inferred by the compiler. However, the dependencies
still show up in the type of an operation, hindering the modularity
of the program.
A second solution is to provide to tostring a mechanism
for coercing away the labels in the set s before the call to
important. In that case, important would not be able to
specialize its execution to the newly provided labels. How-
ever, if tostring called many open operations, or if it were
somehow infeasible to supply a map for important, then
that may be the only reasonable implementation.
In contrast, a closed polytypic operation may easily call
other closed polytypic functions.
2.3.2 Higher-order coercions
Not all type-directed operations should be extensible.
Programmers may wish to reason about their operation in
a "closed world". Furthermore, even if an operation is ex-
tensible, for many new labels the behavior of the operation
should be identical to that for their underlying representa-
tion. Although a data structure containing a new label #
may be converted so that it does not mention the new label
(by repeated use of {{- # ), it still may be di#cult or computationally
expensive to coerce the components of a large
data structure. For example, coercing a list of #'s to a list of
int's requires deconstructing the list, coercing each element
individually and creating a new list.
To avoid this unnecessary e#ort, both when the program
is written and when it is executed, we add higher-order coercions
to #L . These terms provide an e#cient mechanism
for coercing values with labeled types between their underlying
representations and back. Like first-order coercions,
these operations have no run-time e#ect; they merely alter
the types of expressions.
For example, suppose we define a new label equivalent to
a pair of integers with new int-int and we have a variable
x with type list #. Say also that we have a closed, type-directed
operation f of type # int , # int.
The call f [list #] x does not type check because # is not
in the domain of f . However, we do know that that # is isomorphic
to int so we could call f after coercing the type of
the elements of the list by mapping the first-order coercion
across the list.
f [list int] (map (#y:#. {{y}}
However, operationally, this map destructs and rebuilds the
Type Contexts # ::= - empty context
| #-bound type vars
| #:L(#) label variables
| #, s:Ls label set variables
| #L #-bound type vars
Signatures #, l:#
Contexts #, x:#
l=#
| # | {l # e} | v1 # v2
| #L.e | #:L(#).e | #s:Ls.e
Tycon paths #

Figure

2: Syntax necessary for the static and dynamic
semantics
list, which could be computationally expensive. Higher-order
coercions can coerce x to be of type list int without
computational cost.
[list
In general, a higher-order coercion is annotated with a
type constructor (in this case list) that describes the location
of the label to coerce in the type of the term.
3. THE CORE LANGUAGE
Next we describe the semantics of core #L in detail, including
the dynamic and static semantics of the mechanisms
described in the previous section. The semantics of this language
is defined by a number of judgments, the most important
of which are described below. These judgments employ
a number of new syntactic categories, which are listed in

Figure

2. For reference, the complete semantics of this language
appears in Appendix A.
The judgment states that a term e is
well-formed with type #, in type context #, term context
#, and possibly using type isomorphisms described by #.
Type isomorphisms are induced by new expressions that
introduce new label variables isomorphic to types. To show
that terms are well typed often requires determining the
kinds of types, with the judgment #, and the set of
possible labels that may appear in types, with the judgment
# | L.
The judgment describes the small-step call-
by-value operational semantics of the language. It says that
a term e with a set of labels L steps to a new term e # with a
possibly larger set of labels L # . During the evaluation of the
new operator, the label-set component allows the selection
of a fresh label that has not previously been used. In this
way, it resembles an allocation semantics [22, 8]. The initial
state of execution includes all type constants, such as # int
and # , in L. The semantics for the #-calculus fragment of
#L , including fix and integers, is standard, so we will not
discuss it further.
3.1 Semantics of generative types
The dynamic and static rules for new are:
new # in e # L#
l=#
# int
l=#
l 1

Figure

3: Operational semantics for higher-order coercions (excerpt)
new # in e : #
Dynamically, the new operation chooses a label constant
that has not been previously referred to and substitutes it
for the label variable # within the scope of e. Statically, #
must not appear in the type # of e, so that it does not escape
its scope. When type checking e, the isomorphism between
# and # is available through the coercions.
The primitive coercions change the head constructor in
the type of their arguments.
l=#[l] | #
The syntax # ] denotes a type where # is the head of the
type path #. A path is a sequence of applications of several
type arguments. Operationally, the primitive coercion "-"
cancels the primitive coercion "+".
Higher-order coercions extend the expressiveness of the
primitive coercions to allow the non-head positions of a type
to change. As described in the last section, they are useful
for coercing the types of values stored in data structures.
These coercions are annotated with a type constructor #
that describes the part of the data structure to be coerced.
l | #
Intuitively, a higher-order coercion "maps" the primitive coercions
over an expression, guided by the type constructor
# .

Figure

lists some of the rules that describe the operational
semantics of this term. The weak-head normal form of
the constructor # determines the operation of higher-order
coercions. This form is determined through the following
kind-directed relation:
The first rule assures that if a type is of kind #, then it
normalizes to its weak-head normal form. The relation
# is a standard weak-head reduction relation, and
is listed in the Appendix. If a type is not of kind # the
second rule applies, so that eventually it will reduce to a
nesting of abstractions around a weak-head normal form.
Because the type constructor annotation # on a higher-order
coercion must be of kind # for some kind #, we
know that it will reduce to a type constructor of the form
#. We also know that # will a path headed by a variable
or constant, a universal type, or a branch type. The form
of # determines the execution of the higher-order coercion.
If # is a path beginning with a type variable #, then that
is a location where a first-order coercion should be used.
However, there may be other parts of the value that should
be coerced (i.e., there may be other occurrences of # in
the path besides the head position) so inside the first-order
coercion is another higher-order coercion.
Otherwise the form of # must match the value in the body
of the coercion. For each form of value there is an operational
rule. For example, if # is int then the value must be
an integer, and the coercion goes away-no primitive coercions
are necessary. If the value is a function, then semantics
pushes the coercion through the function, changing the type
of its argument and the body of the function. Similar rules
apply to other value forms.
3.2 Semantics of type analysis
The rule describing the execution of typecase is below:
This rule uses the relation # to determine the
weak-head normal form of the analyzed type # . This form
must be some label #
i at the head of a type path #. Then,
typecase chooses the rightmost matching branch from its
map argument, v, and steps to the specified term, applying
some series of type arguments as specified by the term path
p. This term path is derived from # in an obvious fashion.
The static semantics of typecase is defined by the following
rule.
# | L # L1 # L2 # L # L1
The most important part of this rule is that it checks that
# may be safely analyzed by typecase. Whatever the head
of the normal form of # is, there must be a corresponding
branch in typecase. The judgment # | L conservatively
determines the set of labels that could appear as part of the
type # . This judgment states that in the typing context #,
the type # may mention labels in the set L. The important
rules for this judgment are those for labels and variables.
l | {l}
# | L
In the first rule above, labels are added to the set when they
are used as types. The second two rules correspond to the
two forms of type variable binding. Type variables bound
from the term language are annotated with the set of labels
that may appear in types that are used to instantiate them.
However, variables that are bound by type-level abstractions
do not have any such annotation, and consequently do not
contribute to the label set. This last rule is sound because
the appropriate labels will be recorded when the type-level
abstraction is applied.
Not all types are analyzable in the core #L language. The
types of first-class maps and polymorphic expressions may
not be analyzed because they do not have normal forms that
have labels at their heads. In the next section, we show how
to extend the calculus so that such types may be represented
by labels, and therefore analyzed. For this core language
however, we prevent such types from being the argument to
typecase by not including rules to determine a label set for
those types.
Once the rule for type checking typecase determines the
labels that could appear in the argument type, it looks at
the type of the first-class map to determine the domain of
the map. Given some map e with domain L1 and a type
argument # that mentions labels in L, this rule checks that
the map can handle all possible labels in # with L # L1 .
The result type of typecase depends on the type of the
map argument, L1 # L2 . The most important rule for
checking maps is the rule for singleton maps below.
The first component of the map type (in this case l) describes
the domain of the map and the second two components (#
and L # ) describe the types of the branches of the map. The
judgments ensure that the label
l and label set L are well-formed with respect to the type
context #. For labels of higher kind, typecase will apply
the matching branch to all of the arguments in the path
to the matched label. Therefore, the branch for that label
must quantify over all of those arguments. The correct type
for this branch is determined by the kind of the label, with
the polykinded type notation # L#. This notation is
defined by the following rules:
The label set component of this kind-indexed type is used as
the restriction for the quantified type variables. To ensure
that it is safe to apply each branch to any subcomponents
of the type argument, the rule for typecase requires that
the second label set in the type of the map be at least as big
as the first label set.
It is important for the expressiveness of this calculus that
the typecase rule conservatively determines the set of labels
that may occur anywhere in its type argument. It is also
sound to define a version of this rule that determines the
possible labels in the head position of the type, because
that is all that are examined by typecase. However, in
that case, branches that match labels of higher kinds must
use U as the restriction for their quantified type variables.
Only determining the head labels of types does not provide
any information about the labels of other parts of the type.
That precision would prevent important examples from
being expressible in this calculus. Many type-directed operations
(such as polymorphic equality) are folds or cata-
morphisms over the structure of types. To determine the
behavior of the algorithm for composite types, such as product
types, the function must make recursive calls for the
subcomponents of the type. Those recursive calls will type
check only if we can show that the subcomponents satisfy
the label set requirements of the entire operation. But as
mentioned above, it must be assumed that those subcomponents
have label set U and are unanalyzable.
3.3 Properties
The #L language is type sound, following from the usual
progress and preservation theorems [32]. The proofs of these
theorems are inductions over the derivations defined.
Theorem 3.1 (Progress). If # int , # /
# dom(#) and
then e is value, or if
then there exist some L # , e # such that
Theorem 3.2 (Preservation). If # int , # /
and
then there exists # , with
that # e # and # .
We have also shown that the coercions are not necessary to
the operational semantics. An untyped calculus where the
coercions have been erased (preserving types for analysis)
has the same operational behavior as this calculus. In other
words, expressions in #L evaluate to a value if and only
if their coercion-erased versions evaluate to the coercion-
erased value.
4. FULL REFLEXIVITY
The core language demonstrates the basic idea of extensible
typecase expressions, but does not o#er the capability
of full reflexivity. Some types cannot be analyzed by
typecase. The full #L language addresses this problem and
extends the set of analyzable types to include all types. For
more expressiveness, the full language also includes label
and label set runtime analysis operators. In the rest of this
section we discuss these extensions. The modifications to
Kinds #1 #2
Labels l ::= .
Label sets L ::= .
Types # | l | #1#2
|
| #s:Ls.#L | #L#
Terms e ::= .
| setcase L #
| lindex l
Setcase # e# e {} , # e# , U # eU }
branches

Figure

4: Modifications for full reflexivity
label polymorphism
label set polymorphism
# kind polymorphism

Figure

5: Distinguished label kinds
the syntax of core #L to support full reflexivity appear in

Figure

4.
In core #L language universal types and map types cannot
be the argument to typecase. The full language introduces
distinguished labels to represent constructors of universal
types and map types. The kinds of the distinguished labels
are shown in Figure 5. These types now become syntactic
sugar for applications of the appropriate labels, as shown in

Figure

7. These new distinguished labels require new forms
of abstractions in the type level; for labels (#:L(# ), for
label sets (#s:Ls.# ) and for kinds (#. This addition is
also reflected at the kind level: Kinds include the kinds of the
core #L , kinds for label abstractions (L(#1) #2 ), kinds for
label set constructors (Ls #) and finally universal kinds
(#), which are the kinds of kind abstractions in the type
level.
There is one implication in the addition of these new abstraction
forms. Polykinded types cannot be determined
statically in general, as the kind over which they are parameterized
may be unknown at compile time. Therefore
polykinded types are part of the syntax of the full language,
instead of being derived forms. The type equivalence relation
encodes the fact that they are equivalent to certain
simpler types. The interesting equivalences are given in Figure
6. Notice that polykinded types do not have a label constructor
in Figure 7. At run time, closed polykinded types
will always be reduced to one of the other type forms.
Although typecase allows a programmer to determine
if a label matches one of a given set of labels, it does not
provide her with a way to learn about new labels. There-
fore, full #L language introduces an operator lindex, which
returns the integer associated with its argument label con-
stant. This operator provides the programmer a way to

Figure

int # int #1 #2 #1 #2

Figure

7: Syntactic sugar for types
distinguish between labels at run time. The rule for lindex
is straightforward.
lindex #
Another addition is that of a label set analysis operator
setcase. Because the language of label sets is fixed, setcase
has branches for all possible forms of label set-empty, sin-
gleton, union and universe. Operationally, setcase behaves
much like typecase, converting its argument to a normal
form, so that equivalent label sets have the same behavior,
and then stepping to the appropriate branch.
To demonstrate label and label set analysis, consider the
following example, a function that computes a string representation
of any label set. Assume that the language is
extended with strings and operations for concatenation and
conversion to/from integers.
fix settostring:#:Ls. string.#:Ls.
setcase #
{ # "",
#s1 :Ls.#s2 :Ls.
The rule to type check setcase is below.
setcase L {# e# e {} ,
In this rule, e {} must be able to take any label as its argu-
ment, whatever the kind of the label. Therefore this expression
must be kind polymorphic.
5. HIGHER-ORDER ANALYSIS
Higher-order type analysis [31] is an extension of run-time
analysis to types of higher-order kind. It is used to define
operations in terms of parameterized data structures, such
as lists and trees. These operations must be able to distinguish
between the type parameter and the rest of the type.
For example, a generic "length" operation that determines
the length of a list and the number of nodes in a tree must be
able to distinguish between the data (no matter what type
it is) and the rest of the structure. Because #L can generate
new labels at run time, it can make such distinctions.
The result of higher-order analysis depends on the kind
of the analyzed constructor. In previous systems [31, 12]
a type-directed operation is defined as an interpretation of
a type constructor. Type functions are mapped to term
type applications to term applications, and type
variables to term variables. In that way, equivalences in
the term language reflect equivalences in the type language.
Even though the types (# .int) bool and bool are syntactically
di#erent, they are semantically the same type, and
so analysis produces the same results.
However, in #L , analysis is over the weak-head normal
form of types. Because equal types have the same normal
form, such equivalences are already preserved. Furthermore,
because we know that all constructors of kind # are
equivalent to type functions (by extensionality) we can encode
the analysis of such a constructor as a polymorphic
term function, whose body uses typecase to analyze a constructor
of kind #. Generalizing to all kinds, we can encode
higher-order analysis with first-order analysis.
For example, suppose f is an open polytypic operation
of type #s:Ls.#s).(s#s # L) #. Say we want
to use the instance of f for the type # of kind #, and
that L contains all the labels in # . To do so, we modify the
call site of f to be a polymorphic function, because that is
the interpretation of type functions. This function abstracts
the type argument # and a branch x as the interpretation
of #. It then creates a new label for # and passes a branch
to f that maps the new label to the interpretation of #.
That way, no matter what type # is instantiated with, its
interpretation will always be x.
#L.#x:#.new # in
6. EXTENSIONS
branches. One di#culty of working with #L is
that typecase must always have a branch for the label of
its argument. We showed earlier how to work around this
using higher-order coercions or first-class maps. However,
in some cases it is more natural to provide default branches
that apply when no other branches match a label. To do so
we add another form of map { # e} with a domain of all
labels. With this extension, type variables restricted by U
are not parametric.
This branch matches labels of any kind, so its type depends
on the kind of the matched label. Therefore the type is
kind polymorphic. Because of this polymorphism, within
#L there are no reasonable terms that could be a default
branch. However, with addition linguistic mechanisms such
as exceptions, these default branches provide another way
to treat new type names.
Recursive uncoercions. New types in #L may be recursively
defined. However, if they are, higher-order coercions
cannot completely eliminate a new label from the type of an
expression. Instead, the coercion will unroll the type once,
leaving an occurrence of the new label. It is possible to use
first-order coercions to recursively remove all occurrences of
a new type, but this will result in unnecessarily decomposing
and rebuilding the data structure. Because coercions
have no computational content, it is reasonable to provide
a primitive operator J-K - l=# for this uncoercing.
Because it is impossible to know statically what the exact
shape of e is, the unrolled type of e is hidden using
an existential type. Where the type "bottoms out" we use
int, although we could use any other type. For example, if
then the following list could be uncoerced
as follows:
J{{inr #1, {{inr #3, {{inl #}}
The resulting existential package could then be opened and
its contents used as the arguments to a type-directed operation
that cannot handle the label #.
Record and variant types. Current systems for type-directed
programming have trouble with record and variant
types, because of the names of fields and constructors. Often
these systems translate these types into some internal
representation before analysis [2]. Because labels are an integral
part of #L , with a small extension we can use them
to represent these types natively.
The extension that we need for record and variant types is
finite type maps from from labels to types of kind #. Finite
type maps are new syntactic category with their own form
of abstraction and application in both the type and term
languages, as well as finite map analysis. Rules analogous
to those for label set subsumption, membership and equality
can be defined for these finite maps.
# ::= . | Map #
e ::= . | #m:Map.e | e[M] | mapcase M #
The distinguished label # rec of kind (Map #) forms record
types from finite maps. As with many versions of records,
these types are equivalent up to permutation. Record terms
are formed from empty records #, singletons
concatenation e1 # e2 . If l is in the domain of the record
type, the record projection e.l is well-formed. Because we
provide abstractions over finite maps, these records get a
form of row polymorphism [24] for free. It is straightforward
to develop similar extensions for variants.
The key di#erence between records and the branches used
by typecase is that for a record, each label must be of
kind #. If arbitrarily-kinded labels were allowed, then code
analyzing record types would need to be kind polymorphic,
limiting its usefulness.
7. RELATED WORK
There is much research on type-directed programming.
Run-time type analysis allows the structural analysis of dynamic
type information. Abadi, et al. introduced a type
"dynamic" to which types could be coerced, and later via
case analysis, extracted [1]. The core semantics of typecase
in #L is similar to the intensional polymorphism of Harper
and Morrisett [11]. However, #L does not include a type-level
analysis operator. Our extension of #L to be fully reflexive
follows a similar extension of Harper and Morrisett's
language by Trifonov, Saha, and Shao [28]. Weirich [31] extended
run-time analysis to higher-order type constructors
following the work of Hinze [12].
Generic programming uses the structure of datatypes to
generate specialized operations at compile time. The Charity
language [3] automatically generates folds for datatypes.
PolyP [15] is an extension of Haskell that allows the definition
of polytypic operations based on positive, regular
datatypes. Functorial ML [17] bases polytypic operations on
the composition of functors, and has lead to the programming
language FISh [16]. Generic Haskell [2], following the
work of Hinze [12] allows polytypic functions to be indexed
by any type or type constructor.
Nominal forms of ad-hoc polymorphism are usually used
for overloading. Type classes in Haskell [30] implement overloading
by defining classes of types that have instances for
a set of polytypic operations. Hinze and Peyton Jones [13]
explored an extension to automatically derive type class instances
by looking at the underlying structure of new types.
Dependency-style Generic Haskell [20] revises the Generic
Haskell language to be based on the names of types instead
of their structure. However, to automatically define more
generic functions, it converts user-defined types into their
underlying structural representations if a specific definition
has not been provided.
Many languages use a form of generative types to represent
application-specific abstractions. For example, Standard
ML [21] and Haskell [23] rely on datatype generativity
in type inference. Modern module systems also provide
generative types [5]. When the definition of the new type
is known, the type isomorphisms of this paper di#er from
calculi with type equalities (such as provided by Harper and
Lillibridge [10] or Stone and Harper [27]) in that they require
explicit terms to coerce between a type name and its
definition. While explicit coercions are more di#cult for
the programmer to use, they simplify the semantics of the
generative types. Explicit coercions also make sense in conjunction
with type-directed programming because even if
the definition is known, the distinction should still be made
during dynamic type analysis.
A few researchers have considered the combination of generative
types with forms of dynamic type analysis. Glew's [8]
source language dynamically checks predeclared subtyping
relationships between type names. L-ammel and Peyton
Jones [18] used dynamic type equality checks to implement
a number of polytypic iterators. Rossberg's #N calculus [26]
dynamically checks types (possibly containing new names)
for equality. Rossberg's language also includes higher-order
coercions to allow type isomorphisms to behave like existen-
tials, hiding type information inside a pre-computed expres-
sion. However, his coercions have a di#erent semantics from
ours. Higher-order coercions are reminiscent of the colored
brackets of Grossman et al. [9], which are also used by Leifer
et al. [19] to preserve type generativity when marshalling.
8. DISCUSSION
In conclusion, the #L language provides a good way to
understand the properties of both nominal and structural
analysis. Because it can represent both forms, it makes
apparent the advantages and disadvantages of each. We
view #L as a solid foundation for the design of a user-level
language that incorporates both versions of polytypism.
In the design of #L , we explored many alternatives to simplify
the language. For example, we tried combining labels
and label sets into the same syntactic category as types,
thereby eliminating the need for separate abstraction forms.
However, this combination dramatically increases the complexity
of the semantics. The fact that this change allows
new expressions to create new names for not just types, but
label sets and even labels, complicates the process of determining
the appropriate set of labels used in a type constructor

Aside from developing a usable source language, there are
a number other extensions that would be worthwhile to con-
sider. First, our type definitions provide a simplistic form
of generativity; we plan to extend #L with a module system
possessing more sophisticated type generativity. Further-
more, type analysis is especially useful for applications such
as marshalling and dynamic loading, so it would useful to
develop a distributed calculus based upon #L . To avoid the
need for a centralized server to provide unique type names,
name generation could be done randomly from some large
domain, with very low probability of collision.
Finally, to increase the expressiveness of the core lan-
guage, we plan to extend it in two ways. First, typecase
makes restrictions on all labels that appear in its argument
so that it can express catamorphisms the structure of the
type language. However, not every type-directed function is
a catamorphism. Some operations only determine the head
form of the type. Others are hybrids, applicable to a specific
pattern of type structure. For example, if we were to add
references to the calculus, we could extend eq to all refer-
ences, even if their contents are not comparable, by using
pointer equality. This calculus cannot express that pattern.
Furthermore, some operations are only applicable to very
specific patterns. For example, an operation may be applicable
only to functions that take integers as arguments,
such as functions of the form int # int or int # int # int.
These operations are still expressible in the core calculus,
but there is no way to statically determine whether the type
argument satisfies one of these patterns, so dynamic checks
must be used. To approach this problem, we plan to investigate
pattern calculi that may be able to more precisely specify
the domain of type-directed operations. For example, the
mechanisms of languages designed to support native XML
processing [14, 6] can statically enforce that tree-structured
data has a very particular form.
Furthermore, it is also important to add type-level analysis
of types to the language. As shown in past work, it is
impossible to assign types to some type-directed functions
without this feature. One way to do so might be to extend
the primitive-recursive operator of Trifonov et al. [28]
to include first-class maps from labels to types.

Acknowledgments

Thanks to Steve Zdancewic, Benjamin Pierce, and Andreas
Rossberg for helpful discussion.
9.



--R

Dynamic typing in a statically-typed language
The Generic Haskell user's guide.
About Charity.
Flexible type analysis.
A type system for higher-order modules
Regular object types.

Type dispatch for named hierarchical types.
Syntactic type abstraction.

Compiling polymorphism using intensional type analysis.
Polytypic values possess polykinded types.
Jones. Derivable type classes.
Regular expression pattern matching for XML.

Programming in FISh.
Functorial ML.
Jones. Scrap your boilerplate: a practical design pattern for generic programming.
Global abstraction-safe marshalling with hash types

The Definition of Standard ML (Revised).
Abstract models of memory management.
Jones, editor. Haskell 98 Language and Libraries: The Revised Report.
Records and variants as a natural extension of ML.
Types, abstraction and parametric polymorphism.
Generativity and dynamic opacity for abstract types.
Deciding type equivalence in a language with singleton kinds.
Fully reflexive intensional type analysis.
Typed compilation of recursive datatypes.
How to make ad-hoc polymorphism less ad-hoc

A syntactic approach to type soundness.
--TR

--CTR
Ralf Lmmel , Simon Peyton Jones, Scrap your boilerplate with class: extensible generic functions, ACM SIGPLAN Notices, v.40 n.9, September 2005
Geoffrey Washburn , Stephanie Weirich, Good advice for type-directed programming aspect-oriented programming and extensible generic functions, Proceedings of the 2006 ACM SIGPLAN workshop on Generic programming, September 16-16, 2006, Portland, Oregon, USA
John Billings , Peter Sewell , Mark Shinwell , Rok Strnia, Type-safe distributed programming for OCaml, Proceedings of the 2006 workshop on ML, September 16-16, 2006, Portland, Oregon, USA
ad-hoc polymorphism;reflexivity;intensional type analysis;generativity