The type improvement constraint
TypeCast tau1 tau2 holds if the type
tau1 is equal to
tau2 -- or can be equal if some type variables in these types are suitably instantiated. Unlike a similar constraint
TypeEq tau1 tau2 HTrue ,
TypeCast does instantiate type variables in
The type class
TypeCast has been introduced in HList and is described in Section 9 and specifically Appendix D of the full HList paper
< HList-ext.pdf >
TypeCast constraint is connected with `boxy types' and is directly related to type equality coercions:
Martin Sulzmann, Manuel Chakravarty, and Simon Peyton Jones, ``System F with Type Equality Coercions''
< http://research.microsoft.com/%7Esimonpj/papers/ext-f >
The type improvement constraint can express local, per instance rather than class-wide, functional dependencies. The
TypeCast constraint is especially useful for type-level type introspection: type-level type-case . The following messages show many examples.
fmapover arbitrarily nested collections
show . readproblem
There are occasions when one wishes to write a class instance for not a function. For example, Jerzy Karczmarczuk wanted to implement vectors as functional objects, and so he introduced
class Vspace a v | v -> a instance Vspace a a instance (Vspace a v) => Vspace a (c->v)
The functional dependency is required: the type of a vector uniquely determines the type of the scalar in the field. The first instance is supposed to handle scalars, and the second deals with true vectors. Alas, GHC does not accept the second instance, even with the -fallow-overlapping-instances flag: the instance violates the functional dependency. Indeed, the first instance will also match the the type
c->v: the first instance may be specialized to
instance Vspace (c->v) (c->v) , which, together with the second instance, clearly contradicts the functional dependency:
c->v does not uniquely determine the first parameter of the typeclass.
The following message shows how to solve the problem in the general way: that is, how to modify the instance
Vspace a a so that it applies only when the type
a is not a functional type. The solution is a class
IsFunction v f where the second parameter is uniquely determined by the first. To be precise, the second parameter is inferred to be of the type
HTrue if and only if the first parameter is an arrow type,
x->y for some
y . The second parameter of
IsFunction is inferred to be of the type
HFalse in any other case.
Although the implementation of
IsFunction needs overlapping instances, using it does not.
fmapover arbitrarily nested collections
The following generic code performs
fmap over arbitrarily deeply nested `collections': lists of
maybes of maps of IOs, etc. The code works for any
fmappable thing: any Functor and any combination of Functors.
test1 = f_map (+1) [[[1::Int,2,3]]] test4 = f_map not (print "here" >> return (Just (Just [Just [True], Nothing]))) >>= print
test4 , when executed, yields
Just (Just [Just [False],Nothing]) as the result. We indeed can affect items (e.g., booleans) buried deeply in complex structures, such as
IO (Maybe (Maybe [Maybe [Bool]])) . This feature puts the deepest functor in the category of SYB-like generic programming.
join function, defined in
Control.Monad , has the signature
join :: Monad m => m (m a) -> m aPaolo Martini (in his message on Apr 26, 2006) posed the problem of a deep join function:
deep'join :: Monad m => m (m (m (... a ...))) -> m aThe last
mcannot be generally removed because some monads, for example
IO, do not provide any function of the type
m a -> a.
One may say that
deep'join is a `folded' join. For the List monad, deep join is list flattening.
Local functional dependency is the one declared per instance rather than for the whole class. This article illustrates the usefulness of the feature, on a sample problem posed by Creighton Hogg. He defines the following generic multiplication code for vectors and scalars
data Vec a = Vec (Array Int a) Int class Product a b c | a b -> c where (<*>) :: a -> b -> c instance (Num a) => Product a (Vec a) (Vec a) where (<*>) num (Vec a s) = Vec (fmap (* num) a) s test = 10 <*> (vector 10 [0..9])The problem is that the test expression fails to typecheck. The inferred type for the right-hand side of the test expression is
(Num a, Num b, Product a (Vec b) c) => cAlas, the constraint
Productcannot be resolved because there is no instance
Product a (Vec b) c. The existing instance is less general, for the case
bare the same. We can make
testto typecheck by adding to it various type annotations.
Alternatively, rather than annotating every expression involving
<*> , we `annotate' the instance as follows. The original, annotation-free definition of
test typechecks then.
instance (Num a,Num b,TypeCast a b)=> Product a (Vec b) (Vec b) where (<*>) num (Vec a s) = Vec (fmap (* (typeCast num)) a) s
Thus, given the instance
C a a and the constraint
C a b , we see failure:
C a a does not match
C a b . Without functional dependencies, instance selection may instantiate type variables in the instance head, but not those in the constraint. The re-written instance
TypeCast a b => C a b , effectively describes the same set of types. Now, however,
C a b matches that instance -- and, then the TypeCast constraint forces
b to be the same. These local , per-instance functional dependencies notably improve the power of instance selection: from mere matching to some type improvement (towards the full unification). The net result is fewer type annotations required from the user.
More detailed explanation of the original problem and of the overloading resolution algorithm: First, the most general type of an expression is determined, and only later the matching (not unifying!) instance is selected.
The message was originally posted as Re: Fundeps: I feel dumb on the Haskell-Cafe mailing list on Thu, 13 Apr 2006 03:27:03 -0000
Another example: the implementation of monadic
sequence for HLists, i.e., converting
HList (m a_i) into
m (HList a_i) . In the argument list of monadic values
m a_i the types
a_i may differ, yet the monad
m must be the same for all elements. The local functional dependencies enforce this constraint, and remove the need to add type annotations to the result. The result type is computed from the argument type.
< HSequence.hs >
One more example: embedding Forth-like languages into Haskell. We wish then numeric literals act as stack transformers; and so we need the functions of the type
a->(Integer,a) to be members of the Num class.
< http://thread.gmane.org/gmane.comp.lang.haskell.cafe/16129/focus=16129 >
Nicolas Frisby posed a problem about controlling the order of instance selection, or, the application of type improvement rules. The problem is somewhat related to monad transformers. He described the following example of a type class with three instances:
class C f g where nest :: f a -> g a instance C IdL IdR instance C f g => C (TransL f) g instance C f g => C f (TransR g)The first instance is the base case. The second instance tells us how to get
nest :: TransL f a -> g afrom just
nest :: f a -> g a. Similarly, the third instance. Now, the problem is of applying
nestto a value of the type
TransL IdL aand expecting
TransR IdR ain the result. We can use the third instance first, followed by the second one. Or the other way around. Because of the ambiguity, however harmless in this case, the code fails to typecheck. The article shows how
TypeCasthelps us to precisely specify the order of instance selection, so to remove any ambiguity.
show . readproblem
Niklas Broberg described the problem of constructing different realizations of XML documents from data of different types. We wish to write
p (p "foo") and specify the desired type of the XML document, like
(p (p "foo")) :: XMLTree (p (p "foo")) :: IO () -- for writing out the XML document
p obviously has to be overloaded with the type
p :: a -> xml . However,
p (p "foo") exhibits the
show . read problem. What should be the result type of the inner invocation of
p? Functional dependencies help resolve the ambiguity; alas, we can't assert any dependency here. We should be able to use
Strings with XML documents of different types, so we cannot say that the argument of
p determines the result. Also, XML documents of the same type can be created from children of different types.
The article shows a solution that does not involve proxies or type annotations. We use a `syntactic hint' to tell the typechecker which intermediate type we want, and we assert local functional dependencies.
Niklas Broberg's follow-up:
< http://www.haskell.org/pipermail/haskell-cafe/2006-August/017392.html >
He confirms the statement of the problem and describes his solution, based on the explanation in the article above.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML