Fundeps, instances and inference

[Scott Dillard]

Hi,

I've been fidgeting with a fixed-length list library, for things like 3d
vectors/points, rgba tuples, etc. The data type is

data a :. b = (:.) a b
  deriving (everything reasonable)

infixr :.

Nothing in that type specifies that for the partially instantiated type
t1:.t2:.t3, t1 and t2 should be equal. (Like Int:.Int:.() for a 2D integer
point.) But t1 and t2 will always will be equal, at least I want them to
always be equal, and everything useful I can think of needs them to be
equal.  (Note I won't actually store things in these data types. This is
just a way of defining operations. Packed arrays and vectors will be
converted to/from these types in a stream-fusioney kind of way. That's the
plan, at least.)

Anyway, I don't need to force them to be equal because all of the functions
for these list-like things come in the form of classes, and those classes
have fundeps, and the fundeps let me enforce type constraints.  The problem
I'm having is making these constraints work nicely with inference. I'm not
sure exactly whats going on, which is why I'm asking the list. For an
example, folding:

-- the fold function/class
class Fold a v | v -> a where
  fold  :: (a -> a -> a) -> v -> a
  foldl :: (b -> a -> b) -> b -> v -> b
  foldr :: (a -> b -> b) -> b -> v -> b

-- base case of the recursion, () is like []
instance Fold a (a:.()) where
  fold  f   (a:._) = a
  foldl f z (a:._) = f z a
  foldr f z (a:._) = f a z

-- inductive case. Pick one of the "instance" declarations below...
instance Fold a (a:.u) => Fold a (a:.a:.u) where -- I1
instance Fold a (a2:.u) => Fold a (a:.a2:.u) where -- I2
  fold  f   (a:.v) = f a (fold f v)
  foldl f z (a:.v) = f (foldl f z v) a
  foldr f z (a:.v) = f a (foldr f z v)


Now, both of those instance declarations work. The first one (I1) specifies
that all of the list elements should be the same type, "a". The second (I2)
doesn't say that right away, because one is 'a' and the other is 'a2.'
However the fundep (v->a) will force a and a2 to match, so from orbit the
two instances appear the same. In practice, I1 does not cause the type
checker to infer the type of list elements, while I2 does. So, in ghci, if
you do

foldr (:) [] (1:.2:.3:.())

With I1 you'll get an error like "no instance for Fold a (t :. t1 :. t2 :.
()).." But with I2, it will infer 1 2 and 3 to all be of type "Num a => a"
and will evaluate the expression to [1,2,3].

So the question is "Why?"  For simple things like fold, map, etc., I can
massage the instance declarations so that the type checker infers things for
me, but for more complicated recursions, I'm having trouble. (For example,
computing determinants by minor expansion. Not the most efficient way I
know, but if I can't figure that out there's no hope for Gaussian
elimination.) The functions work, its just the inference that isn't working.
I'm forced to annotate things, or at least ensure that the types of the
arguments can be inferred from someplace else.

Scott
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20080618/f21ff3a5/attachment.htm