Pattern match on a data family in Haskell

Question

I have wrapped up whole data family in a single existential:

data Type = Numeric | Boolean 

data family Operator (t :: Type)
data instance Operator 'Numeric = Add | Sub
data instance Operator 'Boolean = And | Or

data AnyOp where
  AnyOp :: Operator t -> AnyOp

Now I would like to do some pattern matching on it

pp :: AnyOp -> String
pp op = case op of
  AnyOp Add -> "+"
  AnyOp Sub -> "-"
  AnyOp And -> "&"
  AnyOp Or  -> "|"

But the typechecker yells at me because

      ‘t’ is a rigid type variable bound by
        a pattern with constructor:
          AnyOp :: forall (t :: TType). Operator t -> AnyOp,
        in a case alternative
        at somesource/somefile/someposition
      Expected type: Operator t
        Actual type: Operator 'Boolean ```

Why? What is the proper way of doing this?

Reitman

Could you elaborate on the error you get? – Medalist

Sure, have just done it – Reitman

You need a singleton data AnyOp where AnyOp :: SType t -> Operator t -> AnyOp and data SType t where SNumeric :: SType 'Numeric ; SBoolean :: STYpe 'Boolean. You should find many examples of singletons in Haskell GADTs in you search for them. – Korney

Answer 1

From a distance, data families look a little like GADTs, in that two constructors for a data family can produce results of different types. But data families are not the same as GADTs! They're really much more like type families. You can't actually match on Add or Sub until you know that you have an Operator 'Numeric. Why is this? You can think of it operationally. Each constructor has to have a "tag" so that case expressions can distinguish them. If two Data instances are defined in different modules, then they may well end up using the same tag for different constructors! Furthermore, a newtype instance doesn't even get a tag, so there's no way to distinguish them at all! As chi indicates, you can work around this by wrapping up a singleton in your existential to keep track of which data instance you have.

---

My understanding is that data families don't really offer much, if any, power that can't be obtained without them. Let's see how a data family slightly more complex than yours can be expressed, very awkwardly, with a newtype, a type family, and pattern synonyms.

import Data.Kind (Type)

data Typ = Numeric Bool | Boolean

newtype Operator t = Operator (OperatorF t)

type family OperatorF (t :: Typ) :: Type

type instance OperatorF ('Numeric b) = OpNum b
type instance OperatorF 'Boolean = OpBool

-- This makes no sense; it's just for demonstration
-- purposes.
data OpNum b where
  Add' :: OpNum 'True
  Sub' :: OpNum 'False

data OpBool = And' | Or'

pattern Add :: () => (b ~ 'True) => Operator ('Numeric b)
pattern Add = Operator Add'

pattern Sub :: () => (b ~ 'False) => Operator ('Numeric b)
pattern Sub = Operator Sub'

pattern And :: Operator 'Boolean
pattern And = Operator And'

pattern Or :: Operator 'Boolean
pattern Or = Operator Or'

Setser