{-# OPTIONS -fglasgow-exts #-} module Main () where import HSXML_ext main = runEHTMLRender . toHTML $ content content = standard_page HeadAttrs { ha_title = "Type improvement constraint", ha_longtitle = "Type improvement constraint, local functional \ \dependencies, and a type-level typecase", ha_description = "Type improvement (TypeCast) -- its origins and \ \applications to intentional type analysis", ha_DateRevision = (1,January,2007), ha_DateCreation = (28,July,2006), ha_keywords = ["Type improvement", "functional dependencies", "type equality", "type analysis", "type class", "not-a-function", "Haskell"], ha_links = HLinks { links_start = FileURL "index.html", links_contents = FileURL "types.html", links_prev = FileURL "number-parameterized-types.html", links_next = FileURL "generics.html", links_top = FileURL "../README.html", links_home = URL "http://pobox.com/~oleg/ftp/" } } (tdiv [p "The type improvement constraint" [[code "TypeCast tau1 tau2"]] "holds if the type" [[code "tau1"]] "is equal to" [[code "tau2"]] "-- or can be equal if some type variables in these types are suitably" "instantiated. Unlike a similar constraint" [[code "TypeEq tau1 tau2 HTrue"]] comma [[code "TypeCast"]] "does instantiate type variables in" [[code "tau1"]] "and" [[code "tau2"]] dot] [p "The type class" [[code "TypeCast"]] "has been introduced in HList" "and is described in Section 9 and specifically Appendix D of" "the full HList paper" br [[urlref (URL "http://homepages.cwi.nl/~ralf/HList/paper.pdf")]]] [p "The" [[code "TypeCast"]] "constraint is connected with `boxy types'" "and is directly related to type equality coercions:" br "Martin Sulzmann, Manuel Chakravarty, and Simon Peyton Jones," "``System F with Type Equality Coercions''" br [[urlref (URL "http://research.microsoft.com/%7Esimonpj/papers/ext-f")]]] [p "The type improvement constraint can express local," "per instance rather than class-wide, functional dependencies." "The" [[code "TypeCast"]] "constraint is especially useful for" "type-level type introspection: type-level" [[em "type-case"]] dot "The following messages show many examples."] [ul [li [[item'ref is'function'type]]] [li [[item'ref deepest'functor]]] [li [[item'ref deep'join]]] [li [[item'ref local'fd]]] [li [[item'ref resolve'ambiguity]]] [li [[item'ref solve'read'show]] br nbsp] [li [[aref (FileURLA "types.html" "keyword-args") "Genuine keyword arguments"]]] [li [[aref (FileURLA "../Scheme/xml.html" "typed-SXML") "Typed SXML"]] nosp ", an extensive example of local functional dependencies"] ] [hr] [is'function'type] [deepest'functor] [deep'join] [local'fd] [resolve'ambiguity] [solve'read'show] ) {- Some notes on type equality. TypeEq constraint: |TypeEq a b c| where c is functionally dependent on |a| and |b|. If the types |a| and |b| are the same, |c| is inferred to be |HTrue|; if the types |a| and |b| are different, |c| is inferred to be |HFalse|. HTrue and HFalse are some distinguished singular types. The constraint is partial; it is total if both |a| and |b| are ground types. The predicate may be able to decide equality or disequality for some unground types. TypeEqTotal a b c: the same as TypeEq but it is a total predicate. It works for ground and unground types. A type variable |tau| is equal only to itself and nothing else. That is, TypeEqTotal decides the universal equality: two types are decided equal if they are equal in every possible interpretation, i.e., assignment of types to type variables. TypeCast a b: This constraint does instantiate type variables in |b|. The constraint holds if the type |b| is equal to |a|, or can be equal if some type variables in |b| are suitably instantiated. That is, TypeCast a b holds if there is a possible interpretation where |a| and |b| are equal. The current Haskell with extensions gives us all these predicates. Alas, we don't have |TypeCast a b c|, which can tell either HTrue or HFalse. Therefore, we still need overlapping instances -- which, in effect, emulate the latter. If the latter is given us, then the three predicates remove the need for overlapping and incoherent instances whatsoever. If I could wish, I'd rather have TypeEq, TypeEqTotal and TypeCast predicate as built-in constraints -- and no overlapping instances extension. These predicates are already present implicitly in the typechecker anyway. Type dis-equality can be done even in Haskell98, albeit in an ugly way. A nicer way requires multi-parameter type classes and functional dependencies. A really nice way requires overlapping instances. We can assert that the function foo applies to the values of distinct types: foo:: TypeEq a b HFalse -> a -> b -> String foo _ _ = "Foo" For any use of |foo|, the typechecker will see if the types a and b are ground, and if so, if they are disequivalent. If they are, the constraint is discharged. If the types |a| and |b| are unground, there may still be a way to see their difference, e.g., |Maybe e| and |[b]|. If this is the case, the constraint is again discharged. If the types |a| and |b| are not ground enough to see their disequality, the constraint float upwards, to the enclosing expression, etc. Eventually type variables get instantiated enough so that the constraint can be checked. Or, we encounter the context (explicit quantification, top-level definition with monomorphic restriction, 'main') that forces all constraints. If the constraint remains unsatisfied at that point, an error is reported. The user must sufficiently instantiate the types. I think this is a reasonable behavior, and it works already. All our OOHaskell is based on it (to check that the set of types of labels in any `object' is indeed a set). This also solves the problem that Francois Pottier mentioned at the beginning of his ICFP'05 talk, as the motivation for GADT and his local type inference. Typeclasses give us nicely behaving disequality, which can be inferred and propagated. This [TypeEqTotal a b c] plays well with existenstials: the equality decided by TypeEqTotal is the identity, which is the weakest and so works for either universally or existentially quantified variables. One of the examples in types.html#de-typechecker, Section: * Equality predicate of type schemas TypeUni x y bool: like TypeCast but reporting failure as HFalse. The combination of TypeCast and TypeEq. foo:: TypeUni x y b1, TypeUni x () b2, TypeUni y Bool b3 => x -> y -> (b1,b2,b3) If we resolve the constraints as they are written, we infer the result of the function as (HTrue,HTrue,HFalse). If we resolve the constraints in the reverse order, we get (HFalse,HTrue,HTrue). -} is'function'type = as_block $ description'unit "is-function-type" (title "How to write an instance for " [[em "not"]] nosp "-a-function") [dbody [p "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"] [blockcode "class Vspace a v | v -> a" "instance Vspace a a" "instance (Vspace a v) => Vspace a (c->v)" ] [p "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" [[code "c->v"]] nosp ": the first instance may be" "specialized to" [[code "instance Vspace (c->v) (c->v)"]] comma "which," "together with the second instance, clearly contradicts the functional" "dependency:" [[code "c->v"]] "does not uniquely determine the first" "parameter of the typeclass."] [p "The following message shows how to solve the problem in the" "general way: that is, how to modify the instance" [[code "Vspace a a"]] "so that it applies only when the type" [[code "a"]] "is" [[em "not"]] "a functional type. The solution is a class" [[code "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" [[code "HTrue"]] "if and" [[em "only if"]] "the first parameter is an arrow" "type," [[code "x->y"]] "for some" [[code "x"]] "and" [[code "y"]] dot "The second parameter of" [[code "IsFunction"]] "is inferred to be" "of the type" [[code "HFalse"]] "in any other case."] [p "Although the implementation of" [[code "IsFunction"]] "needs" "overlapping instances, using it does not."] ] [version "1.2, Mar 27, 2005"] [references [tp [[file'ref "isFunction.lhs"]] "The literate Haskell code with explanations and the examples" br "The code was originally posted as " [[html_cite "Problem with fundeps."]] "on the Haskell-Cafe mailing list on Mon, 3 Jan 2005 22:33:45 -0800"] ] deep'join = as_block $ description'unit "deep-join" (title "Deep monadic join") [dbody [p "The regular" [[code "join"]] "function, defined in" [[code "Control.Monad"]] comma "has the signature"] [blockcode "join :: Monad m => m (m a) -> m a"] [tp "Paolo Martini (in his message on Apr 26, 2006) posed the" "problem of a deep join function:"] [blockcode "deep'join :: Monad m => m (m (m (... a ...))) -> m a"] [tp "The last" [[code "m"]] " cannot be generally removed because" "some monads, for example" [[code "IO"]] comma "do not provide any" "function of the type" [[code "m a -> a"]] dot] [p "One may say that" [[code "deep'join"]] "is a `folded' join." "For the List monad, deep join is list flattening."] ] [version "1.1, Apr 30, 2006"] [references [tp [[file'ref "deep-monadic-join.hs"]] "The implementation of the deep join function, and a few tests" ] ] deepest'functor = as_block $ description'unit "deepest-functor" (title "Deepest functor:" [[code "fmap"]] "over arbitrarily nested collections") [dbody [p "The following generic code performs" [[code "fmap"]] "over arbitrarily deeply nested `collections':" "lists of" [[code "maybe"]] nosp "s of maps of IOs, etc." "The code works for any" [[code "fmap"]] nosp "pable thing:" "any Functor and any combination of Functors."] [blockcode "test1 = f_map (+1) [[[1::Int,2,3]]]" "test4 = f_map not (print \"here\" >>" " return (Just (Just [Just [True], Nothing])))" " >>= print"] [p "Here" [[code "test4"]] comma "when executed, yields" [[code "Just (Just [Just [False],Nothing])"]] "as the result. We indeed can affect items" "(e.g., booleans) buried deeply in complex structures, such as" [[code "IO (Maybe (Maybe [Maybe [Bool]]))"]] dot "This feature puts the deepest functor in the category of" "SYB-like generic programming."] ] [version "1.1, Mar 14, 2006"] [references [tp [[file'ref "deepest-functor.lhs"]] "The literate Haskell code with explanations and examples" br "The code was originally posted as " [[html_cite "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"] ] local'fd = let [cCaa,cCab,a,b] = map (\x -> [[code x]]) ["C a a","C a b","a","b"] in as_block $ description'unit "local-fd" (title "Local functional dependency") [dbody [p "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"] [blockcode "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])"] [tp "The problem is that the test expression fails to typecheck." "The inferred type for the right-hand side of the test expression is"] [blockcode "(Num a, Num b, Product a (Vec b) c) => c"] [tp "Alas, the constraint" [[code "Product"]] "cannot be resolved" "because there is no instance" [[code "Product a (Vec b) c"]] dot "The existing instance is less general, for the case" a "and" b "are the same. We can make" [[code "test"]] "to typecheck by adding" "to it various type annotations."] [p "Alternatively, rather than annotating every expression involving" [[code "<*>"]] comma "we `annotate' the instance as follows." "The original, annotation-free definition of" [[code "test"]] "typechecks then."] [blockcode "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"] [p "Thus, given the instance" cCaa "and the constraint" cCab comma "we see failure:" cCaa "does not match" cCab dot "Without functional dependencies, instance selection may instantiate" "type variables in the instance head, but not those in the constraint." "The re-written instance" [[code "TypeCast a b => C a b"]] comma "effectively describes the same set of types. Now, however," cCab "matches that instance -- and," [[em "then"]] "the TypeCast constraint forces" a "and" b "to be the same. These" [[em "local"]] comma "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 "1.3, Oct 29, 2006"] [references [tp [[file'ref "local-func-dependency.lhs"]] "The literate Haskell code with explanations and an example" br "The code was originally posted as " [[html_cite "Local Fundeps [was: Fundeps: I feel dumb]"]] " on the Haskell-Cafe mailing list on Thu, 13 Apr 2006 19:56:17 -0700"] [p [[file'ref "local-dep-problem.txt"]] "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." br "The message was originally posted as " [[html_cite "Re: Fundeps: I feel dumb"]] " on the Haskell-Cafe mailing list on Thu, 13 Apr 2006 03:27:03 -0000"] [p "Another example: the implementation of monadic" [[code "sequence"]] "for HLists, i.e., converting" [[code "HList (m a_i)"]] "into" [[code "m (HList a_i)"]] dot "In the argument list of monadic values" [[code "m a_i"]] "the types" [[code "a_i"]] "may differ, yet the monad" [[code "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" [[em "computed"]] "from the argument type." br [[urlref (URL "http://darcs.haskell.org/HList/HSequence.hs")]]] [p "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" [[code "a->(Integer,a)"]] "to be members of the Num class." br [[urlref (URL "http://thread.gmane.org/gmane.comp.lang.haskell.cafe/16129/focus=16129") ]]] ] resolve'ambiguity = as_block $ description'unit "ambiguity-resolution" (title "Resolving overloading ambiguity") [dbody [p "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:"] [blockcode "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)"] [tp "The first instance is the base case. The second instance tells us" "how to get" [[code "nest :: TransL f a -> g a"]] "from just" [[code "nest :: f a -> g a"]] dot "Similarly, the third instance." "Now, the problem is of applying" [[code "nest"]] "to a value of the type" [[code "TransL IdL a"]] "and expecting" [[code "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" [[code "TypeCast"]] "helps us to precisely specify the order of instance selection," "so to remove any ambiguity."] ] [version "1.1, Jul 11, 2006"] [references [tp [[file'ref "instance-ambiguity-resolution.lhs"]] "The literate Haskell code with explanations and examples" br "The code was originally posted as " [[html_cite "Re: technique to allow innocuous ambiguity in \ \instance declarations?"]] "on the Haskell-Cafe mailing list on Tue, 11 Jul 2006 22:35:31 -0700"] ] solve'read'show = as_block $ description'unit "solving-read-show" (title "Solving the" [[code "show . read"]] "problem") [dbody [p "Niklas Broberg described the problem of constructing different" "realizations of XML documents from data of different types." "We wish to write" [[code "p (p \"foo\")"]] "and specify the desired type of the XML document, like"] [blockcode "(p (p \"foo\")) :: XMLTree" "(p (p \"foo\")) :: IO () -- for writing out the XML document"] [p "The function" fnp "obviously has to be overloaded with the type" [[code "p :: a -> xml"]] dot "However," [[code "p (p \"foo\")"]] "exhibits the" [[code "show . read"]] "problem. What should be the result type" "of the inner invocation of" fnp nosp "?" "Functional dependencies help resolve the ambiguity; alas, we can't" "assert any dependency here. We should be able to use" [[code "String"]] nosp "s" "with XML documents of different types," "so we cannot say that the argument of" fnp "determines the result." "Also, XML documents of the same type can be created from children" "of different types."] [p "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 "1.1, Aug 14, 2006"] [references [tp [[file'ref "solve-read-show.lhs"]] "The literate Haskell code" br "It was originally posted as " [[html_cite "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"] [p "Niklas Broberg's follow-up:" br [[urlref (URL "http://www.haskell.org/pipermail/haskell-cafe/2006-August/017392.html")]] br "He confirms the statement of the problem and describes his solution," "based on the explanation in the article above."] ] where fnp = [[code "p"]] dot = [[tspan nosp "."]] comma = [[tspan nosp ","]] -- LocalWords: TypeCast HList HFalse HTrue file'ref blockcode