The inverter itself is generic: it is a type-class function, that is, a type-class parameterized by the type-class to `invert'. The inverter is a simple higher-order for-loop on types. There has been a proposal on Haskell' to give equal rights to types and classes. In Haskell98+multi-parameter type classes, classes are already first-class, for all practical purposes. We can easily define (potentially, higher-order) type functions on type classes.
It becomes relatively straightforward then to implement RSA in types. That prompted Graham Klyne to remark on Haskell Cafe ``Methinks this gives a whole new meaning to "type security"''.
The article below introduces a subset of Haskell (called
Haskell1) with only one, pre-defined typeclass C
with
only one method ac
. One can add more instances
to C
but cannot define any more typeclasses or any more
methods. Despite the restriction, we implement overloaded numerical
functions, show
and, minBound
. We define
monads and their extension, restricted monads, as well as monad
transformers, e.g., MonadError
, demonstrating that
Haskell1 supports some functional dependencies.
To represent the rest of functional dependencies, we
introduce Haskell1' as an extension of Haskell1 with the pre-defined
constraint TypeCast. That constraint is not user-extensible and can be regarded
built-in. In fact, it is already the built-in constraint t1 ~ t2
since GHC 6.12. We implement in Haskell1' the motivating example from the
paper `Associated Types with Class' by Chakravarty, Keller, Peyton
Jones and Marlow (POPL2005). Finally we introduce the analogue of
Haskell98 classes -- method bundles -- and use them for defining
bounded existentials.
Haskell1 is not a new language and requires no new compilers. It is merely a subset of Haskell; the `removal' of typeclass declarations is a matter of discipline rather than that of syntax.
Gerrit van den Geest has kindly pointed out another re-design
of Haskell type classes: System O of Odersky, Wadler, and Wehr. System
O however imposes the restriction that each function overloaded over
the type a
must have the type of the form a -> t
, with a
not free in t
. Therefore, System O cannot express, for example,
fromInteger
and minBound
. Haskell1 has no such restrictions and can
express any overloaded function of Haskell. Restricting Haskell to
only one particularly chosen typeclass is no restriction at all.
Class1.hs [7K]
Expressing Haskell98 typeclass idioms in Haskell1
Class2.hs [10K]
Haskell1' and its expressivity
In addition to the single, pre-defined class C
, we assume TypeCast.
The latter is not user-extensible and may be regarded as a pre-defined
constraint. To define TypeCast however, we need the undecidable instances
extension. Nothing else requires this extension; furthermore, TypeCast is
closed and non-recursive and so is certainly decidable.
We show a method to describe classes of types in a concise way, using unions, class differences and unrestricted comprehension. These classes of types may be either closed or open (extensible). After that set up, we can write arbitrarily many functions overloaded over these type classes. An instance of our function for a specific type class may use polymorphic functions to generically process all members of that type class. Our functions are hence second-order polymorphic.
poly2.hs [9K]
The complete Haskell source code
is-of-class.hs [4K]
Small self-containing example of classifying data based on their types
This self-contained code defines the function is_of_class
to
statically check if an object of the type x
is a member of the
class c
. A class of types is defined by enumeration, set-union,
set-difference, and unrestricted comprehension.
The code was originally posted as Re: Trying to avoid duplicate instances on the Haskell-Cafe mailing list Tue, 13 May 2008 23:04:29 -0700 (PDT)
print
to be equivalent to
putStrLn . show
when applied to showable expressions,
whose types are the members of the class Show
. For other
types, the operation print
should do something
different (e.g., print that no show function is available, or, for
Typeable expressions, write their type instead).The naive approach clearly does not work
instance Show a => Print a where print x = putStrLn (show x) instance Print a where print x = putStrLn "No show method"because the two instances have the identical heads
Print a
and so considered duplicates by the type-checker. The WikiPage
below describes the working solution, relying on multi-parameter type
classes with functional dependencies and the type level predicate
describing the membership in the class Show. The trick is to re-write
a constraint (C a)
which succeeds of fails, into a
predicate constraint (C' a flag)
, which always succeeds,
but once discharged, unifies flag
with a type-level
Boolean HTrue
or HFalse
.Joint work with Simon Peyton-Jones.
Type improvement constraint, local functional dependencies, and a type-level typecase
The method for defining type-level predicates
Dynamic dispatch on a class of a type
A more `dynamic' solution
Type-class overloaded functions: second-order typeclass programming with backtracking
An example of building classes of types and defining their membership predicate
IsInstanceOf
. The problem was originally posed by Hal Daume III,
who wrote on the Haskell mailing list:i'm hoping to be able to simulate a sort of dynamic dispatch based on class instances. basically a function which takes a value and depending on what classes it is an instance of, does something. I've been trying for a while to simulate something along the lines of:class Foo a where { foo :: a -> Bool } class Bar a where { bar :: a -> Bool } foo x | typeOf x `instanceOf` Foo = Just (foo x) | typeOf x `instanceOf` Bar = Just (bar x) | otherwise = Nothing
The following code shows how to implement a dynamic dispatch on a type class context. No unsafe operations are used. The test at the end demonstrates that we can indeed simulate Hal's desired example.
Hal Daume III: simulating dynamic dispatch. The message with the statement of the problem, posted on the Haskell mailing list on Mar 20, 2003.
< http://www.haskell.org/pipermail/haskell/2003-March/011518.html >
Choosing a type-class instance based on the context
An alternative: a static dispatch on a class of a type
UndecidableInstances
extension
is on. The unconformant instances are admitted and cause problems,
but at a later time and place and accompanied with even harder to
understand error messages.Functional dependencies are quite well understood, see the works by M. P. Jones and M. Sulzmann. According to Mark P. Jones, they are inspired and quite akin to functional dependencies in relational databases. In a class declaration
class C a b | a -> b where cm :: a -> bthe functional dependency
a->b
asserts the following implication(*) C a1 b1, C a2 b2, a1 ~ a1 ===> b1 ~ b2where
~
denotes type equality. We view the type-class as defining a
predicate on types: C t1 t2
holds for types t1
and t2
if there
is an instance of C
that matches C t1 t2
, that is, will be
selected for t1
and t2
. On one hand, the implication (*) lets us
derive the proof of type equality, to be used for improving
other types and resolving further constraints. For example, if we enter the
following instance and a definitioninstance C Bool Int where ... f x = cm (not x)GHC infers for
f
the type Bool -> Int
. Without the functional
dependency, the inferred type is polymorphic: C Bool b => Bool ->
b
. If the context in which f
is used does not constrain f
's result
type, the user will have to write a type annotation to help the
compiler select the instance for C
. Since our instance tells the
compiler that C Bool Int
holds, the implication (*) says C Bool b ===> b ~ Int
. The constraint C Bool b
can hence be discharged from the type of f
and b
improved to Int
.
A functional dependency is also a restriction on the set of
instances. If we enter instances of C
such that the
implication (*) is violated, the compiler should
reject the program. Sometimes, the error message makes it hard to
understand what exactly is wrong with the instances. The simple Prolog
code below is intended to help, by printing a counter-example of the
violation of the functional dependency. The code works with and without
overlapping instances.
The program is a simple model checker for implications like (*).
Our first example has one type class and two instances
class C a b | a -> b instance C Bool Int instance C [a] [b]Each instance is encoded as a Prolog clause:
c(i1,bool,int). c(i2,[_A],[_B]).
In Haskell, lower-case type identifiers are variables and upper-case
ones are type constants. In Prolog, it's the other way around.
The first argument of c
identifies the instance.
Underscored variables are singleton variables (if we omit the
underscores, we get a warning from the interpreter).
?- G = (c(_,X,Y), c(_,X,Y1)), G, Y \== Y1, print('counterexample: '), instantiate(G), print(G), nl.we search for types
X
, Y
and Y1
such that c(_,X,Y)
and
c(_,X,Y1)
both hold and Y
is different from Y1
. If the search
succeeds, we print out the found types. (Actually, we print out
a grounding of the found types, which makes the print-out nicer.)
The above program does find a counterexample:
c(i2, [t2], [t3]), c(i2, [t2], [t4])
.
That is, one can select an instance for C [t2] [t3]
and for
C [t2] [t4]
, where t2
, t3
, t4
are some distinct types;
in particular t3
is different from t4
. Since the implication
(*) is violated, the program must be rejected.
The Prolog code used syntactic disequality \==
, which is defined
as the negation of ==
. The ordinary Prolog equality Term1 = Term2
holds if there exists a substitution for free variables in Term1
and Term2
that makes the terms identical. This equality is
decided by unification. The syntactic equality Term1 == Term2
holds
if the terms are identical for any substitution.
If X
and Y
are two free variables, then X = Y
holds (making
these variables shared) but X == Y
fails. Correspondingly, X \== Y
succeeds (and X \== X
fails).
Our second example has overlapping instances:
class C a b | a -> b instance C Bool Int instance C a bencoded as
c(i1,bool,int). c(i2,_A,_B).The same Prolog query produces the counter-example:
c(i1, bool, int), c(i2, bool, t1)
. That is, C Bool Int
can be
resolved (to the first instance) and C Bool t1
with t1
different
from Int
can also be resolved, to the second instance. The program should
be rejected.A violation of a functional dependency is usually harder to see. Here is a real example, posted on the Haskell mailing list by Wolfgang Jeltsch in Aug 2003.
class C a b c | a b -> c where ... instance C a b c => C a (x,y,b) c where ... instance C a (a,c,b) c where ...Its encoding in Prolog, the model checking query and the found counter-example are as follows
c(c2, A,tup(A,C,_B), C). c(c1(I),A,tup(_X,_Y,B),C) :- c(I,A,B,C). ?- G = (c(_,X,Y,Z), c(_,X,Y,Z1)), G, Z \== Z1, print('counterexample: '), instantiate(G), print(G), nl. %% counterexample: c(c2, t11, tup(t11, t12, tup(t11, t13, t14)), t12), %% c(c1(c2), t11, tup(t11, t12, tup(t11, t13, t14)), t13)
We have described how to check if the instances of a type class with a functional dependency conform to the dependency. The method is model checking of the implication represented by the functional dependency. If the check fails, it produces a counter-example of a concrete selection of violating instances.
Peter J. Stuckey and Martin Sulzmann: The theory of overloading.
TOPLAS, 2005, v27, N6, 1216-1269
Mark P. Jones, Iavor S. Diatchki: Language and Program Design for Functional Dependencies.
Haskell Symposium 2008
< http://web.cecs.pdx.edu/~mpj/pubs/fundeps-design.html >
Iavor S. Diatchki: TypeFamilies vs. FunctionalDependencies & type-level recursion
Message posted on the Haskell' list on Wed, 15 Jun 2011 10:10:14 -0700.
The message explains the GHC bug of failing to validate instances with
respect to functional dependency, occurring when
UndecidableInstances
is on. Iavor suggests a fix.
The conditions are quite constrictive, and GHC offers a way to
lift them, with the LANGUAGE
pragma UndecidableInstances
.
The pragma is shunned however. There are good reasons for that
attitude: if we lift the conditions, we can write instances that
send the type checker into infinite loop (albeit only potentially:
the termination is insured by the recursion depth limit, set by
the flag -fcontext-stack
). Section 7.6.3.2.
``Undecidable instances'' describes two such (quite subtle) cases.
It is also true that Paterson and Coverage Conditions are
sufficient but by no means necessary to ensure the decidability of type
normalization. There are patently total type functions
rejected by the Conditions. This article shows a simple
example, and argues for more acceptance towards
UndecidableInstances
. The extension is not always bad,
and should not be automatically frowned upon.
Our example is simple indeed:
{-# LANGUAGE TypeFamilies #-} type family I x :: * type instance I x = x type family B x :: * type instance B x = I xThe code is not accepted by GHC 6.8.3 and GHC 6.10.4. The compiler complains:
Application is no smaller than the instance head in the type family application: I x (Use -fallow-undecidable-instances to permit this) In the type synonym instance declaration for `B'Yet there cannot possibly be any diverging reduction sequence here! The type family
I
is the identity, and the type
family B
is its alias. There is no recursion. The fact
that type families are open is not relevant: type families in our code
are effectively closed, because one cannot define any more instance
for I
and B
(or risk overlap, which is rightfully not supported
for type families).
GHC complains because it checks termination
instance-by-instance. To see the termination in the above type
program, we should consider the instances I
and B
together.
Then we will see that I
does not refer to B
, so there are no
loops. This global termination check -- for a set of instances --
is beyond the abilities of GHC. One may argue that this is the
right decision: after all, GHCi is not a full-blown theorem prover.
Thus there are patently decidable type programs that require
UndecidableInstances
. That extension should not be categorically
stigmatized.
In conclusion, UndecidableInstances
is not a dangerous flag. It will
never cause the type-checker to accept a program that `goes wrong.'
The only bad consequence of using the flag is type checker's might be
telling us that it cannot decide if our program is well-typed, given
the context-stack--depth limit. We may ask the type-checker to try a
bit harder (with a larger depth limit), or look through our program
and find the problem.
UndecidableInstances
are quite like the primitive
recursion criterion: all primitive recursive functions surely
terminate; non-primitive recursive functions generally don't. Still
there are many classes of non-primitive recursive functions that are
total. To see their totality, one has to use more complex criteria.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML