[Haskell-cafe] Type arithmetic with ATs/TFs

[Edward Kmett]

On Fri, Feb 12, 2010 at 2:11 PM, Andrew Coppin
<andrewcoppin at btinternet.com>wrote:

> OK, well in that case, I'm utterly puzzled as to why both forms exist in
> the first place. If TFs don't allow you to do anything that can't be done
> with ATs, why have them?
>
> My head hurts...


You can say anything you might say with type families using GADTs, but
you'll often be talking about stuff you don't care about. =)

sometimes you don't care what the Element type of a container is, just that
it is a container. Yet using GADTs you must always reference the content
type.

size :: Container' c e => c -> Int -- using Container' defined with GADTs

as opposed to

size :: Container c => c -> Int

That doesn't seem like a huge sacrifice at first, until you start
considering things like:

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Category-Cartesian-Closed.html

Instead of just being able to talk about a CCC based on the type used for
its homomorphisms, now I must constantly talk about the type used for its
product, and exponentials, and the identity of the product, even when I
don't care about those properties!

This ability to not talk about those extra types becomes useful when you
start defining data types.

Say you define a simple imperative growable hash data type, parameterized
over the monad type. You could do so with TFs fairly easily:

newtype Hash m k v = Hash (Ref m (Array Int (Ref m [(k,v)])))
empty :: MonadRef m => m (Hash m k v)
insert :: (Hashable k, MonadRef m) => k -> v -> Hash m k v -> m ()

But the GADT version leaks implementation-dependent details out to the data
type:

newtype Hash r k v = Hash (r (Array Int (r [(k,v)])))
empty :: MonadRef m r => m (Hash r k v)
insert :: (Hashable k, MonadRef m r) => k -> v -> Hash r k v -> m ()

This gets worse as you need more and more typeclass machinery.

On the other hand, GADTs are useful when you want to define multidirectional
mutual dependencies without repeating yourself. Each is a win in terms of
the amount of boilerplate you have to write in different circumstances.

class Foo a b c | a b -> c, b c -> a, c a -> b where
    foo :: a -> b -> c

would require 3 different class associate types, one for each fundep.

-Edward Kmett
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100212/bf1db310/attachment.html