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@zednenem.com> wrote:
2009/4/2 Louis Wasserman <wasserman.louis@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@zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe