Polymorphic Variants in Haskell
Koji Kagawa
RISE, Kagawa University2217-20 Hayashi-cho, Takamatsu, Kagawa 761-0396, JAPANkagawa@eng.kagawa-u.ac.jp
Abstract
In languages that support polymorphic variants, a single variantvalue can be passed to many contexts that accept diﬀerent sets ofconstructors. Polymorphic variants are potentially useful for appli-cation domains such as interpreters, graphical user interface (GUI)libraries and database interfaces, where the number of necessaryconstructors cannot be determined in advance.The type system of Haskell, when extended with parametrictype classes (or multi-parameter type classes with functional de-pendencies), has enough power to mimic polymorphic variants.This paper, ﬁrst, explains how to encode polymorphic variants inHaskell’s type system (Haskell 98 + popular extensions). However,this encoding of polymorphic variants are rarely used in practice.This is probably because it is quite tedious for programmers towrite mimic codes by hand and because the problem of ambigu-ity would embarrass programmers.Therefore, the paper proposes an extension of Haskell’s typeclasses that supports polymorphic variants directly. This type sys-tem can produce vanilla Haskell codes as a result of type inference.Therefore it behaves as a preprocessor which translate the extendedlanguage into plain old Haskell. Programmers would be able to usepolymorphic variants without worrying nasty problems such as am-biguities.
1.Introduction
1.1Polymorphic Record and Variant Calculus
Extensions of the Hindley-Milner type system with polymorphicrecord and variant calculi have been extensively studied and knownfor years (e.g. [20, 22, 6]).Variants and records are dual concepts in the theory of program-ming languages. Polymorphic record calculi allow a single functionto be applied to many record types with diﬀerent sets of labels.We can consider polymorphic record calculi as a basis of object-oriented programming languages. In this sense, polymorphic recordcalculi are widely used in the real world.On the other hand, polymorphic variant calculi allow a singlevalue to be passed to many functions which accept diﬀerent setsof constructors. Theoretically, they are dual to polymorphic recordcalculi, and therefore we could use polymorphic variant calculi in
Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor proﬁt or commercial advantage and that copies bear this notice and the full citationon the ﬁrst page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior speciﬁc permission and/or a fee.
Copyright c⃝ ACM [to be supplied] . . . $5.00.
order to introduce extensible algebraic datatypes into functionalprogramming languages. And practically, there are some applica-tion domains where extensible algebraic datatypes are (potentially)useful, as we see in the next section.
1.2Potential Applications of Polymorphic Variants
Suppose that we are writing an interpreter for a tiny language. Weneed a datatype for its abstract syntax.
data Expr = Var String | App Expr Expr| Lambda String Expr
Here, Lambda "x" (Var"x") is an internal representation ofthe expression “λx.x.” Then, for example, we can deﬁne the “eval”function for this datatype.
eval (Var x) env= lookup x enveval (App f e) env= . . .(eval f env) . . .. . .(eval e env) . . .eval (Lambda x e) env = . . .
Later, we may want a variation with a new constructor in or-der to treat specially, for example, full (saturated) function applica-tions.
data ExprF extends Expr = FullApp ExprF [ExprF]
(This declaration means that ExprF is a datatype which has allthe constructors of Expr as well as a new constructor FullApp.Note that this is a tentative syntax used for explanation only andnot the one we will propose in this paper — we will introduceanother declaration form later.) And then, we deﬁne, for example,the “print” function for this extended datatype.
print (Var str)= show strprint (App e1 e2)= . . .print e1 . . .. . .print e2 . . .print (FullApp f es) = . . .print (Lambda x e)= . . .print e . . .
On the other hand, we may want to keep eval being deﬁnedfor only Expr, by converting FullApp into multiple App’s beforevalues of the datatype are supplied into eval.We can think of several variations and situations where we wantto use slightly diﬀerent datatypes for abstract syntax trees, whichshare, however, the core constructors.
1.3A Problem of Polymorphic Variant Calculi
As you see, polymorphic variants are potentially useful for somedomains. In practice, however, polymorphic variants are rarelyused. The only practical programming language handling polymor-phic variants is, to the author’s best knowledge, Objective Camlsince ver. 3 [4]. The Standard ML has only one extensible datatypeexn — the type of exceptions. Haskell can mimic polymorphicvariants using (multi-parameter) type classes. However, there are
12006/6/10
some diﬃculties to be used in practice, which we will explain moreprecisely later (Section 2).We could explain the reason of this situation rather abstractlyusing the following table, where Var. stands for polymorphic vari-ant calculi and Rec. stands for polymorphic record calculi.
existing functionsnew functions
existingconstructorsOKVar.:OKRec.:NG
newconstructors
Var.:NGRec.:OKOK
In polymorphic record calculi, it is easy to add a new constructor— when a new constructor (or, in OO methodology, class) is addedby extending an existing one with new ﬁelds, functions deﬁnedfor the existing constructor can be still applied to objects of theextended type (left lower). On the other hand, in polymorphicvariant calculi, though it is easy to add a new function deﬁned bycase analysis (right upper), when a variant type is extended by anew constructor, existing functions that use case analysis cannotbe applied for the new constructor (left lower). Actually, the dualcase of the latter situation corresponds to adding a new function toexisting constructors in polymorphic record calculi (right upper).It is known to be hard to do this (to add a new method to existingclasses) in object-oriented programming languages, and the “visitorpattern” [3] is invented for this very purpose.The fact that it is diﬃcult to add both new data constructors andnew operations without modifying existing code is called the exten-sibility problem and has been extensively studied (e.g., [2, 23, 17]).The problem, though symmetrical, seems to have severer impacton polymorphic variant calculi than on polymorphic record calculi,simply because functions are harder to deﬁne than constructors. Forexample, returning to Expr in the above example, we may want toadd imperative features to the core language by extending the Exprdatatype.
data ExprS extends Expr = Setq String ExprS| Read | Write ExprS
Then, we want to somehow reuse for ExprS the eval function orig-inally deﬁned for Expr. We will explain the diﬃculty of this kind ofreuse more in detail later (Section 2). Generally, for polymorphicvariants to be useful in practical application domains, we wouldneed some mechanisms to reuse existing functions for new con-structors.
1.4The Plan of the Paper
In this paper, we will show how polymorphic variants can beencoded in Haskell (Section 2). The encoding needs an extensionof Haskell 98. The extension — multi-parameter type classes withfunctional dependencies [12] is, however, popular and availableat least in two popular Haskell implementations Hugs and GHC.(We also require that the monomorphism restriction is turned oﬀ.)This encoding is not diﬃcult to understand but at least tediousfor programmers to write by hand, and is practially unfeasible.Therefore, we will propose a type system that directly supportspolymorphic variants and records while avoiding the problem ofambiguity (Section 3). We will introduce a declaration form forpolymorphic variants as a special form of (parametric) type classdeclarations. We also introduce a declaration form for polymorphicrecords and a new instance declaration form that treats recordsand variants symmetrically. We will explain these new forms bytranslating them into plain Haskell codes. Then, we will showsome examples (Section ??), discuss relations to existing work
(Section 4), present future directions (Section 5) and summarizeour contribution (Section 6).
2.Encoding Polymorphic Variants in Haskell
In this section, we will explain how to encode polymorphic variantsin Haskell and how to reuse existing functions deﬁned for polymor-phic variants, solving the problem suggested in the Introduction.Then, we will make manifest the reason why the enconding is notused in practice, Still, the encoding itself explains the idea behindthe new declaration forms that we will introduce in the next section.
2.1Type Classes with Functional Dependencies
Haskell’s type class system is a very general and powerful systemfor overloading. However, Haskell’s type class system, as is deﬁnedin Haskell 98, cannot express polymorphic record and variant cal-culi, especially when we need parametric types such as List andTree.It is known, however, that the system of parametric type classes[1] — a generalization of Haskell’s type class system — can encodepolymorphic record and variant calculi. Type classes with func-tional dependencies [12] further generalize parametric type classes— parametric type classes are special cases where there is only oneindependent type parameter per class. Dependencies among typeparameters are represented by a vertical bar in a class declaration:
class Foo a b c | a b → c where ...
Here, a and b, which appear on the left-hand side of →, areindependent parameters, and c, which appears on the right-handside of →, is a parameter dependent on a and b. This means that,if we have two predicates Foo x y z and Foo x y w that sharethe independent parameters x and y in a single predicate set, twodependent parameters z and w must be uniﬁed.
2.2Encoding Polymorphic Variants
Polymorphic variants can be simply encoded as type classes wherethe sole independent parameter appears at the result type positionsof member functions.
class List s x | s → x wherecons :: x → s → snil:: s
Then, we can add constructors in subclasses:
class List s x ⇒ AppendList s x | s → xwhereunit:: x → sappend :: s → s → s
We also have to deﬁne what we can call “standard instance types”of type classes, the types of whose constructors exactly match theclass declarations
data T_List x =Cons_List x (T_List x) | Nil_List
data T_AppendList x =Cons_AppendList x (T_AppendList x)| Nil_AppendList| Unit_AppendList x| Append_AppendList (T_AppendList x)(T_AppendList x)
If we can use GADT (Generalized Algebraic Data Types)-styledeclarations, correspondence betweeen class declarations and datatype declarations will be much clearer.
data T_List :: * → *whereCons_List :: x → T_List x → T_List x
22006/6/10
Nil_List:: T_List x
data T_AppendList :: * → * whereCons_AppendList:: x → T_AppendList x → T_AppendList xNil_AppendList:: T_AppendList xUnit_AppendList:: x → T_AppendList xAppend_AppendList :: T_AppendList x→ T_AppendList x → T_AppendList x
And of course, we need (rather trivial) instance declarations aswell.
instance List (T_List x) x wherecons = Cons_Listnil= Nil_Listinstance List (T_AppendList x) x wherecons = Cons_AppendListnil= Nil_AppendListinstance AppendList (T_AppendList x) x whereunit= Unit_AppendListappend = Append_AppendList
We can encode functions that accept polymorphic variants usingconstructors in standard instance types. For example,
lengthL Nil_List= 0lengthL (Cons_List _ xs) = 1 + lengthL xs
sumA Nil_AppendList = 0sumA (Cons_AppendList x xs) = x + sumA xssumA (Unit_AppendList x)= xsumA (Append_AppendList xs ys) = sumA xs + sumA ys
Some functions (e.g. sumA) may have the case for append explic-itly and other functions (e.g. lengthL) may be without the casefor append. Then the constructors deﬁned in List can be used forboth kinds of functions as in lengthL (cons 1 nil) and sumA(cons 2 nil). This is what polymorphic variant calculi exactlymean.
2.3Reusing Functions
In order to reuse functions deﬁned for List in its subclass, one maybe temped to deﬁne a new function as follows:
lengthA (Append_AppendList xs ys) =lengthA xs + lengthA yslengthA (Unit_AppendList x) = 1-- other constructorslengthA (Cons_AppendList z zs) =lengthL (Cons_List z zs)lengthA Nil_AppendList = lengthL Nil_List
Unfortunately, this does not type check since zs above may containappend’s as subcomponents of zs (e.g., cons 1 (append . . .. . . )) and since lengthL is deﬁned recursively.Using a coercion such as:
coerce_AppendList_List:: T_AppendList x → T_List xcoerce_AppendList_List(Append_AppendList Nil_AppendList ys) =coerce_AppendList_List yscoerce_AppendList_List (Append_AppendList xs ys) =Cons (hdA xs) (coerce_AppendList_List(Append_AppendList (tlA xs) ys))
lengthA xs = lengthL (coerce_AppendList_List xs)
-- we omit deﬁnitions for these functionshdA :: T_AppendList x → xtlA :: T_AppendList x → x
works for length, however, is in general, not a good idea. Itcoerces deeply, that is, it entirely maps all the subcomponentsof type T_AppendList to T_List and loses information. How-ever, in general, a function may want the subcomponents of typeT_AppendList to maintain their type. For example,
tlA xs = tlL (coerce_ApeendList_List xs)
is not a good deﬁnition since its type is
T_AppendList x → T_List x
instead of
T_AppendList x → T_AppendList x.
Thus, it is not easy to reuse functions for List in its subclasses.This seems to be the very reason why such extensible algebraicdatatypes are not popular — it appears to be no use to extend theexisting type, instead, we would rather rewrite the existing one as:
data List x = Nil | Cons x (List x)| Append (List x) (List x)| Unit x
and rewrite all the existing functions at the same time, losing muchmodularity. Functions that must be redeﬁned may be scattered inthe source program. Or even worse, no source ﬁle may be availablewhen functions are deﬁned in libraries.
2.4Open Recursion
Objective Caml has polymorphic variants since version 3.0. As forthe problem presented above, Garrigue [5] proposes using open re-cursion. It is not possible to completely rephrase O’Caml programsin Haskell. Therefore, we show his solution in pseudo Haskellcodes, which are not actually typable in Haskell. (Of course, withsimple modiﬁcation, we can make it typable in Haskell.)The idea is that we add an additional parameter to recursivefunctions that abstracts recursive invocation.
lengthL_aux le_rec Nil = 0lengthL_aux le_rec (Cons _ xs) = le_rec xs
Here, the argument le_rec abstracts recursive invocation.Then, it is possible to reuse functions when a polymorphic vari-ant is extended,
lengthA_aux le_rec (Append xs ys) =le_rec xs + le_rec yslengthA_aux le_rec (Unit x) = 1lengthA_aux le_rec Nil = lengthL_aux le_rec Nil_lengthA_aux le_rec (Cons x xs) =lengthL_aux le_rec (Cons x xs)
by simply “tying the knot” as follows.
lengthL = lengthL_aux lengthLlengthA = lengthA_aux lengthA
Using this technique, we can reuse existing functions deﬁned forless constructors.
2.5Type Classes for Operations
However, in this technique, we must always provide a higher orderfunction which abstracts recursive function invocation, wheneverwe deﬁne a recursive function for a variant which is to be extended.Fortunately, the system of type classes in Haskell can hide suchhigher order functions and administrative work from programmers.
32006/6/10
Therefore, in Haskell, we can deﬁne length as a member functionof a type class.
class Length a wherelength :: a → Int
instance Length (T_List x) wherelength Nil_List= length_Nillength (Cons_List x xs) = length_Cons x xs
length_Nil = 0length_Cons x xs = 1 + length xs
instance Length (T_AppendList x) wherelength Nil_AppendList= length_Nillength (Cons_AppendList x xs) =length_Cons x xslength (Unit_AppendList x)= length_Unit xlength (Append_AppendList xs ys) =length_Append xs ys
length_Unit x = 1length_Append xs ys = length xs + length ys
We do not have to write codes that explicitly take ane xtra argu-ment.However, still, a problem remains: if we write an expressionsuch as:
length (cons (1::Int) (cons 2 nil))
the type checker reports that it has an ambiguous type.
(Length a, List a Int) => Int
That is, cons (1::Int) (cons 2 nil) has type List a Int=> a and length has type Length a => Int. We cannot deter-mine the type variable a.For example, Hugs (started with command line option -98)reports the followng message.
ERROR "XX.hs":xx - Unresolved top-level overloading*** Binding: xxxx*** Outstanding context : (Length b, List b Int)
In general, “Ambiguity” means that we have a type π ⇒ τ (π is aset of predicates and τ is a type in a narrow sense) where some freevariables in π do not appear freely in τ (i.e. FV(π) ⊈ FV(τ) whereFV stands for “free variables” as usual.) Then, programmers haveto provide type annotations explicitly in order to disambiguate themeaning of the program. We can instantiate the type variable a to aconcrete type, in this case, T List Int. Therefore, we can insert atype annotation as follows:
length (cons 1 (cons 2 nil) :: T_List Int)
Or, when the type of the parameters is not completely known, wewill have to write a little trickier code.
asList :: T_List x → T_List xasList x = x
foo :: x → x → Intfoo x y = length (asList (cons x (cons y nil)))
2.6Summary of Encoding
Now, we have ﬁnished an encoding of polymorphic variants inHaskell (+ type class with functional dependencies). It has somecharacteristics.
• We represent constructors of polymorphics variants as memberfunctions of type classes.
• We also deﬁne functions that accepts polymorphic variants asmember functions of type classes. This is necessary in order tomake such functions reusable when variants are extended.
However, since the encoding uses type classes doubly — bothfor constructors and functions (operations), apparently, there aretwo major problems.
• It is tedious for programmers to write such mimic codes byhand.• In general, it is not easy to add exact type annotations to all thenecessary places in order to disambiguate type variables.
Haskell programmers instinctively avoid ambiguous types. This ex-plains why this encoding mechanism has not been popular so far.However, in this case, ambiguity is not a sign of a pathologicalcode. In fact, if we happen to instantiate the ambiguous type vari-able to another candidate type in the above example,
length (cons 1 (cons 2 nil) :: T_AppendList Int)
the meaning remains identical since the both codes use essentiallythe same branches for length.Therefore, if we can leave the process of encoding to the com-piler, we can use polymorphic variants more readily, which is thetopic of the next section.
3.Variant and Record Declarations
We would like to design a type system and a set of declarationforms that directly supports polymorphic variants and has the sameeﬀect as the encoding explained in the previous section.More speciﬁcally, in this section, we will introduce class dec-laration forms for polymorphic variants (constructors) as well asfor methods (operations). (In order to guarantee that disambigua-tion of type variables does not aﬀect meanings of programs, wemust distinguish classes for methods from ordinary Haskell typeclasses.) We will also introduce instance relations between variantsand methods. Then, we will explain how to translate these new dec-laration forms into plain Haskell code.The new system has to do the following tasks:
• to deﬁne “standard instance types” for variants, and• to declare instance relations between “standard instance types”and related classes.
Programmers do not have to know names of standard instance typesand their constructors, they are “behind the scene” — they are allused completely internally by the compiler and programmers neveruse them explicitly in their programs.The type system also has to do the following:
• to insert type annotations when ambiguous types concerningvariant types appear.
Among them, the last one is non-trivial and we introduce a slightmodiﬁcation of the type inference algorithm for this purpose.
3.1Variant Declarations
We introduce a new class declaration form in order to deﬁne poly-morphic variants. The declaration form for polymorphic variants isalmost the same as that of parametric type classes except that thekeyword variant is used. (In the following, we use the syntax forparametric type classes: where we write the sole independent pa-rameter on the left-hand side of the symbol ∈, for we do not needthe full power of type classes with functional dependencies and thenotation of the former is a little more compact.)
variant π ⇒ α ∈ VariantName β whereConstr1 :: τ11→ · · · → τn11→ α
42006/6/10
. . .Constrm :: τ1m → · · · → τnmm → α
This introduces new symbols Constr1, . . . , Constrm. (We willuse identiﬁers beginning with capital letters for variants.) The re-striction for variant declarations is:
• The independent variable α must appear as the type of the returnvalue of functions. That is, functions must have types of theform · · · → α. (It is possible to have a constructor with noargument — like Nil in the next example.)
The context π speciﬁes superclasses as in class declarations inthe current Haskell. Of course, super classes must be also variantclasses. However, multiple inheritance is allowed.Variant declarations are straightforwardly translated as typeclass declarations. That is, a declaration:
variant α ∈ VariantName β where . . .
becomes a type class declaration:
class VariantName α β | α → β where . . .
where the type variable on the left-hand side of ∈ becomes the soleindependent parameter.For example, the type of lists can be deﬁned as:
variant xs ∈ List x whereNil:: xsCons :: x → xs → xs
The diﬀerence from ordinary data declarations is that we canadd new constructors later:
variant xs ∈ List x ⇒ xs ∈ List2 x whereCons2 :: x → x → xs → xs
variant xs ∈ List x ⇒ xs ∈ AppendList x whereUnit:: x → xsAppend :: xs → xs → xs
(Traditional data declarations can be considered as “ﬁnal” variantdeclarations which cannot have subclasses.) In this example, wecan think of Cons2 as a “cdr-coded” list constructor (with onlytwo elements, — of course, you can add as many elements as youwish). The variant declarations for List and AppendList are ex-actly translated into the type class declarations for the same namesin the previous section.Alternatively, it would be possible to adopt a syntax similar todata declarations.
variant List x = Nil | Cons x (List x)
However, recursive constructors such as Cons has arguments whosetype contains the “self” type — the type of the return value. Theirtypes must change when the variant type is extended. Here, weprefer to use a class-style syntax which makes this fact explicit bya type parameter (i.e. xs). (Another reason why we do not adopt adata-style syntax is a vague conjecture that variants will be furtheruseful if they are combined with GADT (Generalized AlgebraicData Type)’s.)Though we introduce variants as a special case of type classes,there is no need to declare datatypes (other than the *standard*instance types) as instances of variant classes.
• A variant class has no instances (other than its *standard* in-stance type and the *standard* instance types of its subclasses).
3.2Record Declarations
We also introduce a new declaration form called record declarationsin order to deﬁne functions (methods) that operate on variants.
This is because if we did not treat record classes separately fromordinary Haskell classes, the ambiguity problem would remain —that is, the meaning of an expression would depend on the typewhich an ambiguous type variable is instantiated to. On the otherhand, if we separate record classes from ordinary type classes,when an ambiguous type variable only concerns variant class andrecord class predicates, the meaning does not depend on the type itis instantiated to.In “A Second Look at Overloading” [19], Odersky, Wadlerand Wehr propose System O and solve the problem of ambiguityof type classes by putting a simple restriction on the types ofsymbols that can be overloaded. System O requires that overloadedsymbols should be functions and that the type of the ﬁrst argumentshould determine the actual implementation. (That is, overloadedfunctions must have type α → · · · where α is the placeholdervariable of the class.) System O can encode polymorphic recordcalculi and more — it can, so to speak, add new “methods” or“ﬁelds” to existing datatypes.We impose exactly the same restriction for method declarationsin record classes. Moreover, in the sense that variant declarationshave a symmetric restriction that overloaded symbols must havetype · · · → α where α is the independent parameter, this paperproposes a system that can be considered as a symmetric extensionof System O.We use the keyword record instead of class to clarify thateach overloaded operator obeys the System O restriction. We usethe word record, because it can be seen as deﬁnition of selectors(methods) for records.
record π ⇒ α ∈ RecordName β wheremethod1 :: α → τ1. . .methodm :: α → τm
This introduces new symbols method1, . . . , methodm. Here, α isthe independent type variable and β is a sequence of type param-eters dependent on α. The context π speciﬁes superclasses in thesame way as in class declarations in the current Haskell. Its mean-ing is the same as that of parametric type class declaration exceptfor the restriction on the form of types:
• The independent variable α must appear as the type of the ﬁrstargument of each function. (Functions must have types of theform α → · · · .)
Therefore, a declaration:
record α ∈ RecordName β where . . .
becomes a type class declaration:
class RecordName α β | α → β where . . .
where the type variable on the left-hand side of ∈ becomes the soleindependent parameter.For example, a declaration:
record a ∈ Length wherelength :: a → Int
is exactly translated into the type class declaration for the samename in the previous section.**************************************************
3.3Instance Declarations
So far, we can consider record and variant declarations as spe-cial cases of class declarations in the traditional Haskell. Instancedeclarations are, however, diﬀerent from the traditional ones.
52006/6/10
In our system, variant classes cannot have instances in the usualsense. Instead, we declare a variant class (v) as an instance of arecord class (r). It must have the form:
instance π ⇒ v τ ∋ υ ∈ r σ wheremethodm (Constrn p1 . . .pkn) = em. . .
Here, υ between “∋” and “∈” intuitively stands for the “self type”(the type of the ﬁrst argument of methodm) and may appear in π.In order to keep the typing rule for instance declarations simple,
• we restrict constructors of polymorphic variants only appearas the toplevel constructor of the ﬁrst argument in methoddeﬁnitions in instance declarations.
This is probably the simplest way to guarantee that methods in therecord class accepts all the constructors in the variant class. If weallowed polymorphic variants to appear in other places in patterns,we would need more elaborate typing rules for patterns to guaranteethat a certain method accepts all the variants in a certain set ofvariant classes. Moreover,
• we do not allow constructors of polymorphic variants appearoutside of instance declarations.
Note that when v is a subclass of another class, we only providecases for newly added constructors in v. Therefore, there is onlyone instance declaration for a speciﬁc method/Constr pair.
instance List x ∋ xs ∈ Length wherelength Nil= 0length (Cons x xs) = 1 + length xs
instance List2 x ∋ xs ∈ Length wherelength (Cons2 x y xs) =length (Cons x (Cons y xs))
instance AppendList x ∋ xs ∈ Length wherelength (Unit x) = 1length (Append xs ys) = length xs + length ys
Then, since the semantics of methodm does not depend ontyping, no ambiguity will arise. In order for this to work, whenwe check the type of methodm in the above instance declaration,we must take into account that methodm may be added casesfor new constructors in subclasses of v later and therefore, thecurrent method deﬁnition for Constrn might be later used withcases for new constructors. Then, we must make sure that the typeof the method is not overly restricted so that it does not preventlater extensions. Therefore, the type checking rule for the instancedeclaration must ensure that:
• If the type of methodm and Constrn are declared in variant andrecord declarations respectively as:
variant α ∈ v β whereConstrn :: κ1 → · · · → κkn → α
record α ∈ r γ wheremethodm :: α → µm
the type of methodm in the above instance declaration shouldbe as general as:
ρ ⇒ υ → µm[σ/γ]
where we assume the type of Constrn to be
κ1[τ/β, υ/α] → · · · → κkn[τ/β, υ/α] → υ
and ρ must be implied by π ∪ { υ ∈ v τ, υ ∈ r σ } and υ standsfor the “self type”.
Moreover, the instance context π is subject to the same restrictionas the traditional type classes: π must imply the contexts of all thesuperclass instances of r and v [21, page 47].
3.4Type Inference
Basically, the core part of the type inference algorithm does notneed to be changed and remains the same as the one described in[9]. We have to, however, change the behavior of “context reduc-tion” since the form of instance relations has changed. Then, whatshould the type checker do for a type constraint set that containsboth record and variant constraints?Intuitively, it ﬁnds ambiguous types, checks whether we can in-stantiate the ambiguous type variable to a certain standard instancetype, and then actually substitutes the ambiguous type variable tothe standard instance type of the relevant variant classes.The context reduction process of Haskell can be regarded asa special case of simpliﬁcation in the terminology of Jones [10].In our system, the corresponding process should be regarded as acombination of simpliﬁcation and improvement since it involves atype substitution. We would formalize the process as a functionnamed impr. It returns a pair of type substitution and a simpliﬁedtype constraint set. Two auxiliary functions check and ﬁnd are usedin the deﬁnition of impr.
impr(P)=let V = all variant class constraints in PR = all record class constraints in PVR = { (v σ, α, r τ) | (α ∈ v σ) ∈ V, (α ∈ r τ) ∈ R }inif ∀ (v σ, α, r τ) ∈ VR. check(v σ, α, r τ, P)then (idSubst, P)else let (v σ, α, r τ) be an arbitrary pairs.t.¬check(v σ, α, r τ, P)
(Q, v γ, ζ, r δ) = ﬁnd(v, r)
S = mgu((γ, ζ, δ), (σ, α, τ))(S ′, P′) = impr(S (P ∪ Q)) in(S ′ ◦ S, P′)
check(v σ, α, r τ, P)=let (Q, v γ, ζ, r δ) = ﬁnd(v, r) inif there is a substitution Ss.t. S (γ, ζ, δ) = (σ, α, τ) and S π ∈ Pthen True else False
ﬁnd(v, r)=if there is an instance declaration:
instance Q ⇒ v γ ∋ ζ ∈ r δ where . . .
then (Q, v γ, ζ, r δ)else failure
We assume that the standard improvement process for polymor-phic type classes [10, § 3.1] (namely, if both α ∈ c τ and α ∈ c σare in P, the type parameters τ and σ must be uniﬁed) is performedprior to our own simpliﬁcation and improvement.Note that, unlike context reduction in Haskell, the type checkerusually do not discard any type constraints since other type con-straints may be added later which may interact with them. The sizeof the type constraint set gets larger during recursive calls of impr.The impr function always terminates since it does not introducenew type expressions and the number of record and variant classesis limited.
62006/6/10
The ﬁrst element of the result of impr is a type substitutionwhich is applied to the type and the type environment. The secondelement of the result replaces the type constraint set. Using thenotation of [10], it is written as:
Q | TA ⊢W E : ν(T ′, P) = impr(Q)
P | T ′TA ⊢W E : T ′νIt is not necessary to precisely specify when this simpliﬁcation andimprovement process is invoked. It must be done, however, at leastbefore the type is presented to human and before the disambigua-tion process explained in the next paragraph takes place.When α is an ambiguous type variable in P ⇒ τ, we substituteα with the standard instance type of a set of the variant constraintsgiven to α. Then, all the type constraints of the form “α ∈ . . . ”can be safely discarded from P. At the same time, the type checkerinserts a type annotation in the source program. (Ambiguous typescan arise mainly after checking function applications.)We have a prototype implementation of the proposed type in-ference algorithm by extending the engine of “Typing Haskell inHaskell” [11]. Most part of modiﬁcation is necessary to incor-porate functional dependencies. Therefore, the only essential en-hancement in our implementation is the impr function presentedabove.
4.Related Work
We mentioned some related work already in the Introduction. Inthis section, we will refer to some others.In [15], in order to construct modular interpreters, Liang, Hudakand Jones propose using a datatype OR that represents the disjointunion of two types, and a kind of subtyping relation:
data OR a b = L a | R b
class SubType sub sup whereinj :: sub → supprj :: sup → Maybe sub
An apparent drawback of their approach is ineﬃciency of data rep-resentation, since OR tend to be deeply nested. Here is an exampletaken from their paper.
type Term =OR (OR TermA (OR TermB (OR TermF(OR TermL TermR))))(OR TermN (OR TermC (OR TermP TermT)))
More compact representation is desirable.The type system of O’Haskell [18] has the notion of extensi-ble datatypes. Unlike our system, it is based not on polymorphicrecord/variant calculi but on subtyping. Though superﬁcially, theresults look alike, their internal mechanisms are quite diﬀerent. Adrawback of such a subtyping approach is loss of information whenwe create heterogeneous collections.Haskell++ [7] also supports a form of code reuse when wedeﬁne a new datatype similar to an existing datatype. Withoutpolymorphic variants, we have to represent heterogeneous listsusing existential types [14], which also leads to loss of information.The type system of Mondrian [16] allows both code reuse andheterogeneous lists in compensation for loss of some type safetyproperty. This means that “message not understood” errors arisenot in compile time but in run time.HList [13] is a quite diﬀerent approach to heterogeneous col-lections. Though it seems to concern much broader area thanours, as for heterogeneous collections, our approach seems morelightweight as we do not need type-level programming.In “Extensible Algebraic Datatypes with Defaults,” Zenger andOdersky [23] also tackle the problem of code reuse. Though it is
presented as a new design pattern for Java, the underlying ideathat newly added constructors can select a case branch for existingconstructors seems to overlap with ours. In their system, the onlypossible existing case they can select is the implicit default case.Though it may be possible to extend their proposal to select casesother than the default case, it is likely that it would become toocomplex to write by hand.Millstein, Bleckner and Chambers [17] also proposes a systemin which both functions and datatypes are extensible. Though itcan handle binary methods (such as equality and set union) moreelegantly than ours, it does not deal with type inference.
5.Future Work
5.1Binary Methods
In our system, it is possible to deﬁne binary methods, though it maylook awkward. Binary methods are methods which take anotherargument of the same variant class.
record a ∈ Eq where(==), (/=) :: a → a → Bool
The syntactic restriction imposed on the instance declarations al-lows us to avoid the problem caused by “binary methods.”According to the limitation introduced in § 3.3, we do not allowan instance declaration such as:
instance a ∈ Eq ⇒ List a ∋ x ∈ Eq whereCons a as == Cons b bs = a==b && as==bsNil== Nil= TrueCons _ _== Nil= FalseNil== Cons _ _= False
because it uses polymorphic variants in the pattern for the secondparameter of the method. If we accepted this instance declaration,it would be possible to declare another instance such as:
variant a ∈ Foo whereFoo :: Int → a
instance Foo ∋ x ∈ Eq whereFoo n == Foo m = n == m
Nothing prevents a predicate set such as (a ∈ Foo, a ∈ ListInt, a ∈ Eq) and as a result, an expression such as “Foo 1 ==Cons 1 Nil” would become typable but would cause a runtimeerror.Then, how should we deﬁne equalities for List (and List2)?We can circumvent this diﬃculty if we introduce an auxiliary class:
record x ∈ EqList a whereeqCons :: x → (a, x) → BooleqNil:: x → Bool
instance (a ∈ Eq, x ∈ Eq) ⇒List a ∋ x ∈ EqList a whereeqCons (Cons x xs) (y, ys) = x==y && xs==yseqCons Nil(_, _)= FalseeqNil(Cons _ _)= FalseeqNilNil= True
instance x ∈ EqList a ⇒ List a ∋ x ∈ Eq where(Cons x xs) == ys = eqCons ys (x, xs)Nil== ys = eqNilys
This is a well-known technique to deal with multimethods [8]. Itbecomes possible to declare subclasses of List as an instance ofEqList later.In practice, however, this is awkward and it would be necessaryto automatically generate this kind of tedious instance declarations.
72006/6/10
5.2Default Deﬁnitions
In practice, many polymorphic variants would have similar behav-iors for most method deﬁnitions. For example, as for Cons2 andAppend, we will deﬁne most methods as follows.
foo (Cons2 x y zs) = foo (Cons x (Cons y zs))foo (Append xs ys) =foo (if isNull xs then yselse Cons (hd xs) (Append (tl xs) ys))
On the other hand, the current Haskell permits classes to havedeﬁnitions of “default” methods.
class a ∈ Eq where(==), (/=) :: a → a → Boolx /= y = not (x == y)
Then, it would be possible to think of a similar mechanismfor variants where the method deﬁnitions for a constructor C areautomatically generated from a default deﬁnition.We only have to write an empty instance declaration to get amethod for Cons2. For example,
instance Cons2 x ∋ a ∈ Length where {}
Now, we can pass e :: List2 x to, for example, length ::xs ∈ Length ⇒ xs → Int. The constructor Cons2 is convertedto two Cons’s as is deﬁned by the default declaration. Of course, ifwe do not declare List2 as an instance of Length, the expressionlength (Cons2 1 2 Nil) is untypable.We must investigate what kind of default mechanism is easy touse and intelligible to users. There are some questions to be an-swered. For example, if both the method and the variant involvedin an instance declaration have default deﬁnitions, which has pri-ority? What typing rule should apply to default deﬁnitions? Forexample, the default deﬁnition for Append has the constraint thatthree methods isNull, hd and tl must be deﬁned for the type inquestion. What kind of type constraints should be allowed?
6.Conclusion
In this paper, we have explained how we can encode polymorphicvariants in Haskell’s type classes. Then, we have proposed a typesystem for polymorphic records and variants for Haskell. We haveintroduced:
1. a declaration form for polymorphic variants as a special case ofparametric type classes,2. a new instance declaration form between a “record” class and a“variant” class and rules corresponding to “context reduction”in the traditional Haskell, which can be explained as “simpliﬁ-cation” and “improvement” in the terminology of Jones [10].
Moreover, the meanings of programs can be given independently oftypes and we need not worry about ambiguous type errors. Insteadof avoiding ambiguous types altogether, the type system makes useof ambiguities even aﬃrmatively.The proposed type system can produce vanilla Haskell (Haskell98 + type classes with functional dependencies) codes as a resultof type inference. Therefore, the type system can behave as apreprocessor, and we can give the meanings of programs in theextended type system using translation to plain Haskell.
Acknowledgments
The author is grateful to Jacques Garrigue for valuable commentson previous drafts of this paper. Comments from anonymous refer-ees on earlier versions of this paper were also helpful to simplifyand to improve both the idea and the presentation.
An preliminary version of this paper is presented at APLAS’02(The Third Asian Workshop on Programming Languages and Sys-tems) whose proceedings are unpublished. The author is also grate-ful to the attendance of the workshop for helpful comments.
References
[1] K. Chen, P. Hudak, and M. Odersky. Parametric type classes. In ACMConf. on LISP and Functional Programming, June 1992.[2] R. B. Findler and M. Flatt. Modular object-oriented programmingwith units and mixins. In Proceedings of the 1998 ACM SIGPLANInternational Conference on Functional Programming (ICFP ’98),1998.[3] E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns— Elements of Reusable Object-Oriented Software. Addison-Wesley,1995.[4] J. Garrigue.Programming with polymorphic variants.In MLWorkshop, Sept. 1998.[5] J. Garrigue. Code reuse through polymorphic variants. In FOSE2000, Nov. 2000.[6] B. R. Gaster and M. P. Jones.A polymorphic type system forextensible records and variants. Technical Report Technical ReportNOTTCS-TR-96-3, Computer Science, University of Nottingham,Nov. 1996.[7] J. Hughes and J. Sparud. Haskell++: An object-oriented extension ofHaskell. In Haskell Workshop 1995, 1995.[8] D. H. H. Ingalls.A simple technique for handling multiplepolymorphism.In Conference proceedings on Object-orientedprogramming systems, languages and applications (OOPSLA) 1986,pages 347–349, 1986.[9] M. P. Jones. Qualiﬁed Types: Theory and Practice. PhD thesis,Programming Research Group, Oxford University ComputingLaboratory, July 1992.[10] M. P. Jones. Simplifying and improving qualiﬁed types. ReserchReport YALEU/DCS/RR-1040, Yale University, June 1994.[11] M. P. Jones. Typing haskell in haskell. In Proceedings of the 1999Haskell Workshop, pages 9–22, Oct. 1999.[12] M. P. Jones.Type classes with functional dependencies.InProceedings of the 9th European Symposium on Programming, Mar.2000. LNCS 1782.[13] O. Kiselyov, R. L¨ammel, and K. Schupke. Strongly typed heteroge-neous collections. In Proc. of the ACM SIGPLAN Haskell Workshop2004, pages 96–107, Sept. 2004.[14] K. L¨aufer. Type classes with existential types. Journal of FunctionalProgramming, 6(3):485–517, May 1996.[15] S. Liang, P. Hudak, and M. Jones.Monad transformers andmodular interpreters.In Conference Record of POPL’95: 22ndACM SIGPLAN-SIGACT Symposium on Principles of ProgrammingLanguages, pages 333–343, Jan. 1995.[16] E. Meijer and K. Claessen.The design and implementation ofMondrian. In Proceedings of Haskell Workshop 1997, 1997.[17] T. Millstein, C. Bleckner, and C. Chambers. Modular typecheckingfor hierarchically extensible datatypes and functions.In Proc.the 2002 ACM SIGPLAN International Conference on FunctionalProgramming, pages 110–122, Oct. 2002.[18] J. Nordlander.Polymorphic subtyping in O’Haskell.In Proc.the APPSEm Workshop on Subtyping and Dependent Types inProgramming, 2000. Ponte de Lima, Portugal.[19] M. Odersky, P. Wadler, and M. Wehr. A second look at overloading.In Proc. ACM Conf. on Functional Programming and ComputerArchitecture, pages 135–146, June 1995.[20] A. Ohori. A polymorphic record calculus and its compilation. ACMTransactions on Programming Languages and Systems, 17(6):844–895, Nov. 1995.[21] S. Peyton Jones, J. Hughes, et al. Haskell 98: A Non-strict, PurelyFunctional Language, Feb. 1999. http://www.haskell.org/onlinereport/.
82006/6/10
[22] D. R´emy. Typechecking records and variants in a natural extension ofML. In Annual ACM Symp. on Principles of Prog. Languages, pages77–88, January 1989.[23] M. Zenger and M. Odersky. Extensible algebraic datatypes withdefaults.In Proceedings of the International Conference onFunctional Programming, September 2001.
92006/6/10