[Haskell-cafe] Type arithmetic with ATs/TFs
lrpalmer at gmail.com
Fri Feb 12 18:11:43 EST 2010
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>
>> 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
> 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:
> 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
> 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
More information about the Haskell-Cafe