Restrict Pattern Matching to Subset of Constructors

Question

Say I have the following:

data Type
  = StringType
  | IntType
  | FloatType

data Op
  = Add Type
  | Subtract Type

I'd like to constrain the possible types under Subtract, such that it only allows for int or float. In other words,

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

Should be an exhaustive pattern match.

One way of doing this is to introduce separate datatypes for each operation, where it only has the allowed subtypes:

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

However, this makes things a lot more verbose, as we have to create a new constructor name for each category. Is there a way to 'restrict' the possible constructors within a type without making an explicit subset? Would this shorter with the use of DataKinds? I'm a bit unsure as to how to make it more concise than just specifying new data for each constraint.

This question is an extension of my original question, where I asked about datakind unions. There were lots of good suggestions there, but unfortunately the unions don't work when pattern matching; the compiler will still complain that the patterns are not exhaustive.

Coquetry

Answer 1

Indexing a GADT with DataKinds is one approach that may work, depending on your use case:

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

Note that Add works on either 'Numeric or 'NonNumeric Types because of the (existentially quantified) type variable a.

Now this will work:

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

But adding this will fail:

patternMatch (Subtract StringType) = ()

With a warning about inaccessible code: Couldn't match type ‘'Numeric’ with ‘'NonNumeric’.

If you need to add more type groupings, you may prefer to introduce type families to classify types instead, e.g.:

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

This will produce the (slightly less descriptive) warning Couldn't match type ‘'True’ with ‘'False’ if you add the redundant pattern.

When working with GADTs you will often want existentials and RankNTypes in order to work with runtime information; for that, patterns like these may prove useful:

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

Bogor

Answer 2

This solution works but it might not be very practical in the end. I'm using extensible variants from the red-black-record package.

We define our types like this:

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

Those annoying () parameters are there to overcome a limitation of red-black-record; currently there are no instances of ToVariant for sum types without constructor arguments.

Basically, we are removing the StringTy constructor from the VariantCode using the Delete type family, and defining a Variant with the reduced set of constructors.

We can then use the type like this:

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

Variants are eliminated using a Record of handlers, constructed using the addCaseI function. unit is the empty Record. If the Record doesn't cover all cases that will result in a (pretty inscrutable) type error.

---

The disadvantages with this solution are:

• Different syntax for handling the shrunk type.
• Worse type errors.
• Slower at runtime, not as efficient as native sum types.
• The usual bane of extensible record libraries: very slow compilation times for large types.

Other extensible record libraries (vinyl + vinyl-generics, perhaps) might offer better ergonomics.

Lied