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 tau1 and tau2 .
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 >
The 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.
fmap over arbitrarily nested collectionsshow . read problem
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 x and 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.
fmap over arbitrarily nested collectionsThe 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
Here 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.
The regular 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
m cannot 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
Product cannot be resolved because there is no instance Product a (Vec b) c . The existing instance is less general, for the case a and b are the same. We can make test to 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 a and 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.
local-dep-problem.txt [3K]
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 a from just nest :: f a -> g a . Similarly, the third instance. Now, the problem is of applying nest to a value of the type TransL IdL a and expecting TransR IdR a in 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 TypeCast helps us to precisely specify the order of instance selection, so to remove any ambiguity.show . read problemNiklas 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
The function 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-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML