previous   next   up   top

Type improvement constraint, local functional dependencies, and a type-level typecase

 

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.


 

How to write an instance for not-a-function

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.

Version
The current version is 1.2, Mar 27, 2005.
References
isFunction.lhs [5K]
The literate Haskell code with explanations and the examples
The code was originally posted as Problem with fundeps. on the Haskell-Cafe mailing list on Mon, 3 Jan 2005 22:33:45 -0800

 

Deepest functor: fmap over 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

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.

Version
The current version is 1.1, Mar 14, 2006.
References
deepest-functor.lhs [3K]
The literate Haskell code with explanations and examples
The code was originally posted as Deepest functor [was: fmap for lists of lists of lists of ...] on the Haskell-Cafe mailing list on Tue, 14 Mar 2006 22:27:53 -0800

 

Deep monadic join

The regular join function, defined in Control.Monad , has the signature

     join :: Monad m => m (m a) -> m a
Paolo 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 a
The 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.

Version
The current version is 1.1, Apr 30, 2006.
References
deep-monadic-join.hs [3K]
The implementation of the deep join function, and a few tests

 

Local functional dependency

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) => c
Alas, 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.

Version
The current version is 1.3, Oct 29, 2006.
References
local-func-dependency.lhs [5K]
The literate Haskell code with explanations and an example
The code was originally posted as Local Fundeps [was: Fundeps: I feel dumb] on the Haskell-Cafe mailing list on Thu, 13 Apr 2006 19:56:17 -0700

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 >

 

Resolving overloading ambiguity

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.
Version
The current version is 1.1, Jul 11, 2006.
References
instance-ambiguity-resolution.lhs [4K]
The literate Haskell code with explanations and examples
The code was originally posted as Re: technique to allow innocuous ambiguity in instance declarations? on the Haskell-Cafe mailing list on Tue, 11 Jul 2006 22:35:31 -0700

 

Solving the show . read problem

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

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.

Version
The current version is 1.1, Aug 14, 2006.
References
solve-read-show.lhs [3K]
The literate Haskell code
It was originally posted as Local functional dependencies: solving show . read and XML generation problems on the Haskell-Cafe mailing list on Mon, 14 Aug 2006 16:00:35 -0000

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.



Last updated January 1, 2007

This site's top page is http://okmij.org/ftp/

oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML