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

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

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

{-# 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 не охватывает все случаи, это приведет к (довольно непостижимой) ошибке типа.

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

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

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

Индексирование 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, либо с 'NonNumericType из-за переменной типа (экзистенциально определяемой) 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’.

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

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