Почему мы не можем определить замкнутые семейства данных?

Все следующие работы:

{-# 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!

... но это не так (по 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
   |                   ^^^^^

Неужели никто не потрудился реализовать это, или есть ли какая-то особая причина, по которой было бы нецелесообразно закрывать семейства данных? У меня есть семейство данных, где я бы предпочел сохранить инъективность, но также и возможность сделать непересекающийся экземпляр catch-all. Прямо сейчас, единственный способ, которым я вижу эту работу, - это

newtype CDF' a = CDF' (CTF a)

Ответы

Ответ 1

(Здесь я только догадываюсь, но хочу поделиться этой мыслью.)

Предположим, что мы можем написать

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

Теперь, каков тип конструкторов значений, вызванных этим определением? У меня возникло бы желание сказать:

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

... но последнее кажется очень неправильным, так как мы получили бы

CDFOther @ Int :: Double -> CDF Int

который должен быть запрещен, поскольку в замкнутом семействе данных можно было бы ожидать, что (не нижнее) значение CDF Int должно начинаться с конструктора CDFInt.

Возможно, подходящий тип

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

включая "ограничения неравенства", но для этого потребуется больше машинного оборудования для ввода текста, которое в настоящее время доступно в GHC. Я понятия не имею, было ли проверка типа/вывода оставалась разрешимой с таким расширением.

Напротив, типы семейств не содержат конструкторов значений, поэтому эта проблема там не возникает.