[Haskell] Re: class assosiated types, via GADTs or FDs

[oleg at pobox.com]

Manuel M T Chakravarty wrote:

> The functional dependency encoding prevents you from ever making the
> representation of your tries/maps (in the MapKey class example)
> abstract.  It does not only prevent you from declaring it as an abstract
> data type, but it actually forces users of a library built in this way
> to understand the representation types and manually encode them in their
> application code.  

It seems that problem can be easily solved in Haskell with the
existing tools. First of all, one has to mention partial signatures,
which are possible in Haskell to some extent (sufficient in our case)
  http://pobox.com/~oleg/ftp/Haskell/types.html#partial-sigs

But mainly, if we wish to hide some details of the representation, why
not to use tools that are built for that, such as applicative
functors? They are _easily_ implementable in Haskell, arguably
idiomatic, and free from the above drawbacks. The type system itself takes
care to properly hide the representation. The following messages
describe the realization of (generative and applicative and recursive)
functors in great detail:
  http://www.haskell.org/pipermail/haskell/2004-August/014463.html
  http://www.haskell.org/pipermail/haskell/2004-September/014515.html

Here's a simple example tailored to Manuel M T Chakravarty's sample
code. First, the illustration of the problem:

> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-undecidable-instances  #-}
> module MK where
>
> class MapKey k fm | k -> fm where
>     lookp :: k -> fm v -> Maybe v
>     empty :: k -> fm v
>       -- NB: The original signature of empty doesn't mention k, which
>       --     is already problematic, but you can fix this by
>       --     adding it as a dummy argument to fm.
>
> data BoolMap v = Integer
> instance MapKey Bool BoolMap
>
> newtype AnyMap k v = AM [(k,v)]
> instance MapKey Char (AnyMap Char) where
>     lookp k (AM m) = lookup k m
>     empty _ = AM []
> test1 = lookp True undefined

Indeed, the type of lookp is 
  *MK> :t lookp
  lookp :: forall k fm v. (MapKey k fm) => k -> fm v -> Maybe v

If we want to specialize it for Bool keys, we indeed can't write
  lookpBool :: forall fm v. (MapKey Bool fm) => Bool -> fm v -> Maybe v

but we perfectly well can write
> lookpBool k m = lookp (k::Bool) m

One can object that although we don't have to know how the Map of Bool
keys is realized, we can actually see that, from the type of
lookpBool. We have to hide that. But the type system already lets us
do that.

Let us look again at the type
  lookp :: forall k fm v. (MapKey k fm) => k -> fm v -> Maybe v

The problem is the presence of `fm'. A few algebraic transformations
on that expression give us
         forall k v. k -> (exists fm. (MapKey k fm) => fm v) -> Maybe v

which is easily realizable in Haskell.

> data Map' k v = forall fm. MapKey k fm => Map' (fm v)
>
> class MapKey' k where
>     lookp' :: k -> Map' k v -> Maybe v
>     lookp' k (Map' m) = lookp k m
>     empty' :: Map' k v

One and only instance of MapKey' we will ever need:

> instance MapKey k fm => MapKey' k where
>     empty' = Map' (empty (undefined::k))

First we note that the signature of empty' _does_ mention the type of
keys in essential manner -- but does not leak the representation of
the map.

We also note that type of lookp':
	*MK> :t lookp'
	lookp' :: forall k v. (MapKey' k) => k -> Map' k v -> Maybe v

Now, the representation of the map is perfectly hidden.

We can now write:

> test2 = let m = empty' in lookp' 'a' m
> test3 = let m = empty' in lookp' True m

No unneeded signatures -- and the ``library'' automatically adjusts
the representation of maps based on the type of the key --
which seems to have been the main motivation for the associated types.