[Haskell-cafe] Type arithmetic with ATs/TFs

[Luke Palmer]

On Fri, Feb 12, 2010 at 2:10 PM, Edward Kmett <ekmett at gmail.com> wrote:
> 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...
>

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