Question about typing

[Marcin 'Qrczak' Kowalczyk]

Sun, 8 Apr 2001 12:38:27 -0400, Dylan Thurston <dpt@math.harvard.edu> pisze:

> >     class Map c' a' c a | c' -> a', c -> a, c' a -> c, c a' -> c' where
> >         map :: (a' -> a) -> c' -> c
> > ...
> >     -- zipWith is similar to map, only more complicated:
> >     class ZipWith c1 a1 c2 a2 c a
> >         | c1 -> a1, c2 -> a2, c -> a,
> >           c1 a -> c, c a1 -> c1, c2 a -> c, c a2 -> c2
> >         where
> >         zipWith :: (a1 -> a2 -> a) -> c1 -> c2 -> c
> > ...
> 
> You raise many interesting question, but let me ask about one: why the
> specific choice of functional dependencies above?  Why is "c' a -> c"
> necessary for Map?

To make the type of "map f xs" determinable from types of f and xs.

The idea is that instances of map will be made only for "the same"
container applied to potentially different element types (where
the concept of "the same" is not formal, because c is the container
already applied to the element type).

If map could arbitrarily convert the shape of containers, there would
be more ambiguities. In particular "map f (map g xs)" would be always
ambiguous (nothing says what container to use for the intermediate
value).

Conversion is done similarly to fromIntegral: as composition of
functions which convert a container to and from a common universal
type: a list (which is a list of pairs in the case of dictionaries).

A perhaps unusual thing is that when the instance of a class like Map
is determined to be [a] a [b] b, then type variables a and b become
unconstrained. I'm not sure if it causes problems. Generally it seems
to be important which exactly type variables are constrained, e.g. for
resolving ambiguities and for the monomorphism restriction. The
bright side of this is that even though map is generally overloaded
over element types, it has an instance of the type equivalent to
Prelude's map: fully polymorphic wrt. element types.

> Why doesn't ZipWith include, e.g., "c1 a2 -> c2"?

When a is determined (it must be determined by other means anyway,
otherwise the instance is ambiguous, and c1 a2 -> c2 would not help
here), c1 a -> c, c a2 -> c2. So this dependency is implied by others.

I hope I haven't overlooked anything.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK