Why can't we define closed data families?

Question

All of the following work:

{-# LANGUAGE TypeFamilies #-}

type family TF a
type instance TF Int = String
type instance TF Bool = Char

data family DF a
data instance DF Int = DFInt String
data instance DF Bool = DFBool Char

type family CTF a where
  CTF Int = String
  CTF Bool = Char
  CTF a = Double     -- Overlap OK!

...but this doesn't (as of GHC-8.2):

data family CDF a where
  CDF Int = CDFInt String
  CDF Bool = CDFBool Char
  CDF a = CDFOther Double

wtmpf-file24527.hs:16:19: error: parse error on input ‘where’
   |
16 | data family CDF a where
   |                   ^^^^^

Is it just that nobody has bothered to implement this yet, or is there a particular reason why it wouldn't make sense for data families to be closed? I have a data family where I'd rather like to keep the injectivity, but also the opportunity to make a disjoint catch-all instance. Right now, the only way I see to make this work is

newtype CDF' a = CDF' (CTF a)

@DavidYoung Interesting. But I guess that if you used a GADT, inside a `CDF Int` you could find either a `String` or a `Double`. With a closed data family, only a `String` would be possible. — chi, Mar 22 '18 at 17:42
The evidence flows the other way in a GADT, and the runtime representation is quite different. — dfeuer, Mar 22 '18 at 17:55

score 12 · Answer 1 · edited Apr 17 '18 at 12:30

12

(Here I am only guessing, but I want to share this thought.)

Assume we can write

data family CDF a where
  CDF Int = CDFInt String
  CDF Bool = CDFBool Char
  CDF a = CDFOther Double

Now, what is the type of the value constructors induced by this definition? I would be tempted to say:

CDFInt   :: String -> CDF Int
CDFBool  :: Char   -> CDF Bool
CDFOther :: Double -> CDF a

... but the last one feels very wrong, since we would get

CDFOther @ Int :: Double -> CDF Int

which should be disallowed, since in a closed data family one would expect that a (non bottom) value of CDF Int must start with the CDFInt constructor.

Perhaps a proper type would be

CDFOther :: (a /~ Int, a /~ Bool) => Double -> CDF a

involving "inequality constraints", but this would require more typing machinery that currently available in GHC. I have no idea if type checking / inference would remain decidable with such extension.

By contrast, type families involve no value constructors, so this issue does not arise there.

edited Apr 17 '18 at 12:30

dfeuer

48,079
5
63
167

answered Mar 22 '18 at 18:46

chi

111,837
3
133
218

That sounds *very* likely. – dfeuer Mar 22 '18 at 19:00
This does make a great deal of sense. Still wonder whether this is the official reason. – leftaroundabout Mar 22 '18 at 19:45
1

Suppose you had a magical type family for every data family, instantiated here as `type family FamilyOf CDF a :: Nat where {FamilyOf CDF Int = 1; FamilyOf CDF Bool = 2; FamilyOf CDF = 3}`. Now you could give types to the data family constructors: `CDFInt :: FamilyOf CDF a ~ 1 => String -> CDF a`, `CDFBool :: FamilyOf CDF a ~ 2 => Char -> CDF a`, and `CDFOther :: FamilyOf CDF a ~ 3 => Double -> CDF a`. I don't know if this would run into some sort of trouble, but it smells like the right direction. – dfeuer Apr 17 '18 at 12:32
In my last comment, I meant "for every closed data family". – dfeuer Apr 17 '18 at 17:13

Why can't we define closed data families?

1 Answers1

Linked