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.
No doubt local instances are sorely missed. However, there are several different ways of adding them to Haskell -- each with is its own semantics, each with its own problems, which may seem to outweigh the benefits. This article illustrates the problems on simple examples.
Let us assume Haskell with local instances, defined by the let instance form. Consider the following function:
f1 :: Int -> String
f1 x =
let instance Show Int where show _ = "one"
in show x
whose type has no Show constraint: show is being applied to x::Int
and there is the matching Show instance in scope. Thus f1 1
should evaluate to "one". In the next example, however, f2 :: Show a => a -> String
f2 x =
let instance Show Int where show _ = "one"
in show x
the variable x is polymorphic and the overloading of show cannot
be resolved, hence the Show constraint in the function's type.
What should f2 (1::Int) return?
One may argue that a function should close over, or capture, local
instances just as it closes over local variables. If captured
instances are not reflected in the type of the function, however,
there is an unpleasant consequence: parametricity breaks and free
theorems are invalidated. To illustrate, consider the following
variation of f2:
f3 :: Show a => a -> String
f3 x =
let instance Show Int
where show x = if x == 0 then "zero" else "nonzero"
in show x
Its type says that f3 handles its argument solely through the
caller-provided show implementations, that is, Show instances
that are in scope of its invocation. Therefore, in the following
program with the single Show instance, instance Show Int where show _ = "const"
f3_Int :: Int -> String
f3_Int x = f3 x
f3_Int should be a constant function -- as the consequence of a free
theorem. With our implementation of f3, f3_Int 0 and f3_Int 1
give, however, different results. To preserve parametricity, the closed
instances must somehow appear in the function's signature -- preferably
in a way that preserves principle types and hence the type inference.
This complicates the type system.
In the opposite approach, local instances are not closed over --
rather, they behave like dynamically-bound variables. We would then
expect f2 (1::Int) to return "1". This approach is also reasonable,
and also problematic. GHC, seeing our call in which the polymorphic f2 is applied to an Int argument, may decide to specialize f2 to
that type. Such specializations, which eliminate indirect type-class
method calls, are crucial for good performance, and GHC indeed
does them. In our case, the compiler will generate a specialized
version of f2:
f2_Int :: Int -> String
f2_Int x =
let instance Show Int where show _ = "one"
in show x
It looks just like the f1 we started with, which, when applied to 1 returned "one". The specialization thus changed the function's
behavior. Without local instances, specialization was easy to
understand: GHC may, at will, create a copy of a polymorphic function,
instantiate it at a specific type, and replace calls to the
polymorphic function at that type with the calls to the specialized
version. Users, or tools, can perform such a procedure ourselves when
optimizing or refactoring code. With unclosed local instances,
specialization changes the program behavior.
To complicate the matters further, what should f4 (1::Int) return
for the following f4?
f4 :: Show a => a -> String
f4 x =
let instance Show Int where show _ = "two"
in f2 x
Stefan Kaes, the person who introduced ``parametric overloading'' (type classes, in modern term) chose the ``closure semantics''. In his system all instances are local. Duggan and J. Ophel (2002) have perhaps the most comprehensive treatment of local instances. Their proposal supports both closure and non-closure semantics, distinguishing them by so-called open and closed kinds. They do complicate the type system.
Yet another approach, advocated in ``Implicit Configurations'' (HW 2004), restricts local instances so that the problems we have seen do not arise. The restriction outlaws all the examples shown so far. Users are only allowed to define something like the following
data Any = forall s. Any s -- existential
any = Any ()
fq :: (forall a. Show a => a -> String) -> String
fq k = case any of
Any (some::s) ->
let instance Show (s,Int) where ...
in k (some,10)
That is, a local instance must contain an ``opaque'' type like the s above. Informally, only those local instances are permitted that
cannot possibly overlap with any other instance in scope. Is this
restriction too severe? Only experience can tell.In conclusion, the problem of local instances at present is the engineering problem, to be resolved by the empirical evaluation of the trade-offs of various proposals. Incidentally, the ``Implicit Configurations'' paper pointed out a way to emulate the proposed local instances within Haskell of 2004 -- so that one can experiment and accumulate the experience.
I thank Gesh @gesh.uni.cx and Jun Inoue for insightful discussions.
Implicit configurations -- or, type classes reflect the values of types
This paper described all proposed approaches to the configuration problem, including implicit parameters, global variables, the Reader monad, and local instances.
Philip L. Wadler and Stephen Blott: How to Make Ad-Hoc Polymorphism Less Ad Hoc
Proc. POPL 1989, pp. 60-76.
The pioneering work of Stefan Kaes
The parametric overloading system introduced in Kaes' paper was built around local instances, and even local type classes.
Atze Dijkstra, Gerrit van den Geest, Bastiaan Heeren, S. Doaitse Swierstra: Modelling Scoped Instances with Constraint Handling Rules
Technical Report, Utrecht University, 2007
The paper discusses in great detail the problems posed by local instances. It proposes an interesting solution, which lets the programmer specify the instance resolution heuristics.
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 definition instance 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 b
encoded 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 set of instances that violate the dependency.
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 x
The 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-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML