Ограничить сопоставление с образцом подмножеством конструкторов

Question

Скажите, у меня есть следующее:

data Type
  = StringType
  | IntType
  | FloatType

data Op
  = Add Type
  | Subtract Type

Я бы хотел ограничить возможные типы в Subtract, чтобы он допускал только int или float. Другими словами,

patternMatch :: Op -> ()
patternMatch (Add StringType) = ()
patternMatch (Add IntType) = ()
patternMatch (Add FloatType) = ()
patternMatch (Subtract IntType) = ()
patternMatch (Subtract FloatType) = ()

Должно быть исчерпывающее совпадение с образцом.

Один из способов сделать это - ввести отдельные типы данных для каждой операции, где у нее есть только разрешенные подтипы:

newtype StringType = StringType
newtype IntType = IntType
newtype FloatType = FloatType

data Addable = AddableString StringType | AddableInt IntType | AddableFloat FloatType

data Subtractable = SubtractableInt IntType | SubtractableFloat FloatType

data Op = Add Addable | Subtract Subtractable

Однако, это делает вещи более многословными, так как мы должны создать новое имя конструктора для каждой категории. Есть ли способ «ограничить» возможные конструкторы внутри типа без создания явного подмножества? Будет ли это короче с использованием DataKinds? Я немного не уверен, как сделать его более кратким, чем просто указание новых данных для каждого ограничения.

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

Answer 1

Это решение работает, но в конце оно может оказаться не очень практичным. Я использую расширяемые варианты из пакета red-black-record .

Мы определяем наши типы следующим образом:

{-# LANGUAGE DeriveGeneric, DataKinds, TypeFamilies, TypeApplications #-}
import           GHC.Generics
import           Data.RBR

data Ty
  = StringTy ()
  | IntTy ()
  | FloatTy ()
  deriving (Show,Generic)
instance ToVariant Ty

type ShrunkTy = Variant I (Delete "StringTy" () (VariantCode Ty))

data Op
  = Add Ty
  | Subtract ShrunkTy

Эти раздражающие параметры () предназначены для преодоления ограничения красно-чёрной записи; в настоящее время нет экземпляров ToVariant для типов сумм без аргументов конструктора.

В основном мы удаляем конструктор StringTy из VariantCode, используя семейство типов Delete и определяя Variant с сокращенным набором конструкторов.

Затем мы можем использовать такой тип:

foo :: Op -> String
foo op = 
    case op of
        Add ty -> 
            show "add" ++ show ty
        Subtract ty -> 
            let cases = addCaseI @"IntTy"   show
                      . addCaseI @"FloatTy" show
                      $ unit
            in  show "add" ++ eliminateSubset cases ty

Variant с исключены с использованием обработчиков Record, сконструированных с использованием функции addCaseI. unit является пустым Record. Если Record не охватывает все случаи, которые приведут к (довольно непостижимой) ошибке типа.

---

Недостатки этого решения:

• Другой синтаксис для обработки сокращенного типа.
• Хуже ошибки типа.
• Медленнее во время выполнения, не так эффективно, как собственные типы сумм.
• Обычная боль расширяемых библиотек записей: очень медленный время компиляции для больших типов.

Другие расширяемые библиотеки записей ( винил + винил-дженерики , возможно) могут предложить лучшую эргономику.

Answer 2

Индексирование GADT с помощью DataKinds - один из подходов, который может работать в зависимости от вашего варианта использования:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

-- The “group” of a type
data TypeGroup = NonNumeric | Numeric

-- A type indexed by whether it’s numeric
data Type (g :: TypeGroup) where
  StringType :: Type 'NonNumeric
  IntType :: Type 'Numeric
  FloatType :: Type 'Numeric

data Op where
  Add :: Type a -> Op
  Subtract :: Type 'Numeric -> Op

Обратите внимание, что Add работает на 'Numeric или 'NonNumeric Type с из-за (экзистенциально количественной) переменной типа a.

Теперь это будет работать:

patternMatch :: Op -> ()
patternMatch (Add StringType) = ()
patternMatch (Add IntType) = ()
patternMatch (Add FloatType) = ()
patternMatch (Subtract IntType) = ()
patternMatch (Subtract FloatType) = ()

Но добавить это не удастся:

patternMatch (Subtract StringType) = ()

С предупреждением о недоступном коде: Couldn't match type ‘'Numeric’ with ‘'NonNumeric’.

Если вам нужно добавить больше группировок типов, вы можете вместо этого ввести семейства типов для классификации типов, например ::1010 *

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

-- An un-indexed type
data TypeTag = StringTag | IntTag | FloatTag

-- A type indexed with a tag we can dispatch on
data Type (t :: TypeTag) where
  StringType :: Type StringTag
  IntType :: Type IntTag
  FloatType :: Type FloatTag

-- Classify a type as numeric
type family IsNumeric' (t :: TypeTag) :: Bool where
  IsNumeric' 'StringTag = 'False
  IsNumeric' 'IntTag = 'True
  IsNumeric' 'FloatTag = 'True

-- A convenience synonym for the constraint
type IsNumeric t = (IsNumeric' t ~ 'True)

data Op where
  Add :: Type t -> Op
  Subtract :: IsNumeric t => Type t -> Op

Это приведет к (немного менее описательному) предупреждению Couldn't match type ‘'True’ with ‘'False’, если вы добавите избыточный шаблон.

При работе с GADT вам часто требуются экзистенциалы и RankNTypes для работы с информацией времени выполнения; для этого могут пригодиться такие шаблоны:

{-# LANGUAGE RankNTypes #-}

-- Hide the type-level tag of a type
data SomeType where
  SomeType :: Type t -> SomeType

-- An unknown type, but that is known to be numeric
data SomeNumericType where
  SomeNumericType :: IsNumeric t => Type t -> SomeNumericType

parseType :: String -> Maybe SomeType
parseType "String" = Just (SomeType StringType)
parseType "Int" = Just (SomeType IntType)
parseType "Float" = Just (SomeType FloatType)
parseType _ = Nothing

-- Unpack the hidden tag within a function
withSomeType :: SomeType -> (forall t. Type t -> r) -> r
withSomeType (SomeType t) k = k t