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

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

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

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


types haskell pattern-matching type-families gadt
person radrow    schedule 28.10.2019    source источник
comment
Не могли бы вы уточнить ошибку, которую вы получаете?   -  person AJF    schedule 28.10.2019
comment
Конечно, только что сделал это   -  person radrow    schedule 28.10.2019
comment
Вам нужен синглтон data AnyOp where AnyOp :: SType t -> Operator t -> AnyOp и data SType t where SNumeric :: SType 'Numeric ; SBoolean :: STYpe 'Boolean. Вы должны найти много примеров синглетонов в Haskell GADT при их поиске.   -  person chi    schedule 28.10.2019

Ответы (1)


arrow_upward
3
arrow_downward

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

Насколько я понимаю, семейства данных на самом деле не предлагают много, если таковые имеются, силы, которую нельзя получить без них. Давайте посмотрим, как семейство данных, несколько более сложное, чем ваше, может быть очень неуклюже выражено с помощью синонимов 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'
person dfeuer    schedule 28.10.2019