On Fri, Feb 12, 2010 at 2:10 PM, Edward Kmett <[email protected]> wrote: > On Fri, Feb 12, 2010 at 2:11 PM, Andrew Coppin <[email protected]> > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
