From oleg-at-okmij.org Mon Jan  3 22:33:45 2005
cc: haskell-cafe@haskell.org
In-Reply-To: <courier.41D863C1.00005081@averell>
Subject: Problem with fundeps.
From: oleg-at-pobox.com
Message-ID: <20050104063345.D1ABFA930@Adric.metnet.navy.mil>
Date: Mon,  3 Jan 2005 22:33:45 -0800 (PST)
X-Comment: more general IsFunction, from de-typechecker


On Sun, 2 Jan 2005 karczma@info.unicaen.fr wrote:

] I tried to generalize one of my old
] packages for quantum *abstract* computations, where state vectors are
] defined as functional objects, whose codomain has some arithmetic.
] It is easy to see that you can define (f <+> g) = \x -> f x + g x
] etc. It should be possible to curry this further, so I defined
]
] class Vspace a v | v -> a
] where
]  (<+>) :: v -> v -> v
]  (*>)  :: a -> v -> v
]  -- etc.
] For a given set of vectors, the associated scalars are unique
]
] instance Vspace a a where
] (<+>) = (+)
] (*>)  = (*)
] -- etc.  No problem.
]
] instance (Vspace a v) => Vspace a (c->v) where
]  -- ...
]
] GHCi answers
]
]   Cannot unify the type-signature variable `v' with the type `c -> v'
]   When using functional dependencies to combine
]     Vspace a a, arising from the instance declaration at ./Qutils.hs:30
]     Vspace a (c -> v),
]       arising from the instance declaration at ./Qutils.hs:38


Marcin 'Qrczak' Kowalczyk commented:
]] In the instance Vspace a a the compiler doesn't know that "a" is
]] supposed to be a scalar only. It matches vector types (functions) too.
]]
]] And adding a context won't help. An instance of the form
]]   instance Ctx a => Cls (T a)
]] means "T a can always be used as an instance of Cls, and such usage
]] will yield a further requirement of Ctx a which must be fulfilled"
]] rather than "T a can be used as an instance of Cls as long as Ctx a
]] holds". In particular it will overlap with any other instance whose
]] head can be unified with Cls (T a). Instance overlapping doesn't take
]] instance contexts into account, only instance heads.

Henning Thielemann noted
  http://www.haskell.org/pipermail/haskell-cafe/2005-January/008227.html
that the same problem occurs in the new Haskell numeric prelude.

This problem has been solved in the general way. Please refer to the
message on keyword arguments:
	http://www.haskell.org/pipermail/haskell/2004-August/014416.html

Functional dependencies _are_ kept. Here's one of the tests

test4 = ((\x y -> x <+> y) <+> (\x y -> ((2 *> x) <+> (3 *> y))))
	(1::Int) (2::Int)

it typechecks and computes. Perhaps this solution also solves the
problems in the numericprelude. The compiler is GHCi 6.2.1 and
GHCi 6.4.

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
> 
> module Q where
> 
> class Vspace a v | v -> a
>     where
>     (<+>) :: v -> v -> v
>     (*>)  :: a -> v -> v
> 
> 
> instance (IsFunction v f, Vspace' f a v) => Vspace a v
>   where
>   (<+>) = doplus (undefined::f)
>   (*>)  = dostar (undefined::f)
> 
> class Vspace' f a v | f v -> a
>     where
>     doplus :: f -> v -> v -> v
>     dostar :: f -> a -> v -> v
> 
> instance Num a => Vspace' HFalse a a where
>  doplus _ = (+)
>  dostar _  = (*)
>  -- etc.  No problem.
> 
> instance (IsFunction v f, Vspace' f a v, Vspace a v) 
>     => Vspace' HTrue a (c->v) where
>  doplus _ f g = \x -> f x <+> g x
>  dostar _ a f x = a *> (f x)
> 
> 
> test1 = (1::Int) <+> 2
> test2 = ((\x -> x <+> (10::Int)) <+> (\x -> x <+> (10::Int))) 1
> test3 = ((\x y -> x <+> y) <+> (\x y -> (x <+> y) <+> x)) (1::Int) (2::Int)
> 
> test4 = ((\x y -> x <+> y) <+> (\x y -> ((2 *> x) <+> (3 *> y))))
> 	(1::Int) (2::Int)
> 
> 
> 
> data HTrue
> data HFalse
> 
> class IsFunction a b | a -> b
> instance TypeCast f HTrue => IsFunction (x->y) f
> instance TypeCast f HFalse => IsFunction a f
> 
> -- literally lifted from the HList library
> class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
> class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
> class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
> instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
> instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
> instance TypeCast'' () a a where typeCast'' _ x  = x