From oleg-at-okmij.org Mon Jan 3 22:33:45 2005
cc: haskell-cafe@haskell.org
In-Reply-To:
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