Сопоставление с образцом в семействе данных в Haskell - PullRequest
Новая
       80

Сопоставление с образцом в семействе данных в Haskell

5 голосов
/ 28 октября 2019

Я обернул все семейство данных в одну экзистенциальную: 

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

Теперь я хотел бы сделать сопоставление с шаблоном для него 

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

Но проверщик типов кричит на меняпотому что 

      ‘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 ```

Почему? Как правильно это сделать?

1 Ответ

2 голосов
/ 28 октября 2019

На расстоянии семейства данных немного похожи на GADT, так как два конструктора для семейства данных могут давать результаты разных типов. Но семейства данных не совпадают с GADT! Они действительно намного больше похожи на типовые семьи. Вы не можете на самом деле соответствовать Add или Sub, пока не узнаете, что у вас есть Operator 'Numeric. Почему это? Вы можете думать об этом оперативно. Каждый конструктор должен иметь «тег», чтобы выражения case могли их различать. Если два экземпляра Data определены в разных модулях, они могут в конечном итоге использовать один и тот же тег для разных конструкторов! Более того, экземпляр newtype даже не получает тега, поэтому нет никакого способа их различить! Как указывает Чи, вы можете обойти это, обернув единичный элемент в своей экзистенции, чтобы отслеживать, какой экземпляр данных у вас есть.

Насколько я понимаю, семейства данных на самом деле не предлагают много, еслилюбая, сила, которую невозможно получить без них. Давайте посмотрим, как семейство данных, несколько более сложное, чем ваше, может быть очень неловко выражено с помощью нового типа, семейства типов и синонимов шаблонов. 

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'
...