Re: [Haskell-cafe] Type arithmetic with ATs/TFs

On Fri, Feb 12, 2010 at 2:10 PM, Edward Kmett wrote:

On Fri, Feb 12, 2010 at 2:11 PM, Andrew Coppin 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...

s/GADT/Fundep/g ?

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/...

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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe