[Haskell-cafe] Type families and kind signatures

[Manuel M T Chakravarty]

Louis Wasserman:
> Mkay.  I get it now.  I was under the impression that, essentially,  
> a data family was precisely equivalent to a type family aliasing to  
> a separately declared datatype.

No, they are not equivalent.  You can see that as follows.  Assume,

   data family T a
   type family S a

Now, given `T a ~ T b', we know that `a ~ b'.  (We call this  
implication "decomposition".)

In contrast, given `S a ~ S b' we do *not* know whether `a ~ b'.  Why  
not?  Consider the instances

   type instance S Int     = Bool
   type instance S Float = Bool

Clearly, `S Int ~ S Float', but surely not `Int ~ Float'.  So,  
decomposition does not hold for type synonym families, but it does  
hold for data families.

This is actually, not really a property of type *families* alone.  It  
already distinguishes vanilla data types from vanilla type synonyms.   
We know, say, that if `Maybe a ~ Maybe b', then `a ~ b'.  However, given

   type Const a = Int

we have `Const Int ~ Const Float' (and still not `Int ~ Float').   
Definitions, such as that of `Const', are rarely used, which is why  
this issue doesn't come up much until you use type families.

> One more question: is there any way to get the low overhead of  
> newtypes for particular instances of a data family?  Is this  
> impossible?  That is, is there any way to do something like
>
> data family Foo a
> data instance Foo Int = Bar Int -- Bar is actually a newtype

You can use

   newtype instance Foo Int = MkFoo Int

So, the instances of a data family can be data or newtype instances.,  
and you can freely mix them.

Manuel


> On Thu, Apr 2, 2009 at 12:47 PM, David Menendez <dave at zednenem.com>  
> wrote:
> 2009/4/2 Louis Wasserman <wasserman.louis at gmail.com>:
> > Mkay.  One more quick thing -- the wiki demonstrates a place where  
> the
> > original attempt worked, with a data family instead. (That is,  
> replacing
> > 'type' with 'data' and adjusting the instance makes this program  
> compile
> > immediately.)
> > a) Is there a type-hackery reason this is different from data  
> families?
>
> It's not type hackery. Data families are different from type families,
> and the syntax for declaring instances of higher-kinded families is a
> consequence of those differences.
>
> An instance of a data family is a new type constructor, so you have to
> provide the additional arguments in order to declare the data
> constructors.
>
> data family Foo a :: * -> *
> data instance Foo Bool a = FB a a
> -- Foo Bool has kind * -> *, like [], so I could make it a Functor
>
> Instance of type families are always pre-existing type constructors.
>
> type family Bar a :: * -> *  -- Bar a must equal something of kind *  
> -> *
> type instance Bar () = Maybe
>
> > b) Is there a reason this isn't made a lot clearer in the  
> documentation?
> >  GHC's docs say that higher-order type families can be declared  
> with kind
> > signatures, but never gives any examples -- which would make it a  
> lot
> > clearer that the below program doesn't work.
>
> Here's a higher-kinded type family I've used.
>
> type family Sig t :: * -> *
>
> class (Traversable (Sig t)) => Recursive t where
>    roll :: Sig t t -> t
>    unroll :: t -> Sig t t
>
>
> The Traversable context wouldn't be valid if I had declared Sig t a ::
> *, because type families must always be fully applied.
>
>
> The difference is analogous to the difference between
>
> type M0 a = StateT Int IO a
> type M1   = StateT Int IO
>
> Since type synonyms (like type and data families) must always be fully
> applied, you can use M1 in places where you can't use M0, even though
> they're effectively the same thing.
>
> foo :: ErrorT String M1 a -- valid
> bar :: ErrorT String M0 a -- not valid
>
>
>
> --
> Dave Menendez <dave at zednenem.com>
> <http://www.eyrie.org/~zednenem/>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090403/041b2efe/attachment.htm