"Pattern-matching" types in Haskell

Question

I want a function f that acts as an increment on Ints and as an identity on all the other types. I tried to enable the TypeApplications extension and do this the most straight-forward way possible:

f :: forall a. a -> a
f @Int x = x + 1
f @_   x = x

But the extension does not enable such patterns:

<interactive>:6:1: error: Parse error in pattern: f @Int

Is there pattern-matching for types (or a similar mechanism) in Haskell?

score 9 · Accepted Answer · answered Apr 21 '21 at 14:29

As stated, this is impossible to achieve in Haskell since it would violate one of the fundamental properties of parametric polymorphism known as "parametricity", which ensures that any polymorphic function satisfies a specific property knows as the "free theorem".

In particular, a terminating function of type forall a. a -> a must be the identity. There are no other possible implementations.

That being said, if we allow a constraint on type a, this becomes possible. Typically, run-time type-testing is done in Haskell through the Typeable type class:

f :: forall a. Typeable a => a -> a
f x = case eqT @a @Int of    -- Is a ~ Int ?
   Just Refl -> x + 1        -- If it is, we can add one.
   Nothing   -> x            -- Otherwise, return x as-is.

This requires a bunch of GHC extensions, and to import Data.Typeable.

score 8 · Answer 2 · answered Apr 21 '21 at 14:31

There is, but you cannot have a fall-through pattern like you can at the computation level. That is, at the computation level, I could write

f 0 = 42
f n = n-1

with a fall-through pattern n that works exactly when none of the other patterns matched. At the type-level, you can't do this -- even nested inside other patterns. You can have a pattern that matches anything, but not "anything else" -- if you match anything, you can't have any other patterns.

So, once you have the collection of patterns you want to match against, you can write a type class and instances. So, if you want to support Int, Bool, and lists, you could write:

class F a where f :: a -> a
instance F Int where f = succ
instance F Bool where f = id
instance F [a] where f = id

The last shows an example of what I meant before, where you can have a pattern that matches anything, but not a pattern that matches "anything else": [a] is a fine instance, but it precludes the creation of a [Bool] instance later.

score 2 · Answer 3 · answered Apr 21 '21 at 18:57

Here you’re trying to produce different term-level code based on type-level information, so you need a typeclass; and you’re trying to match on types, so you can use an associated type family. This method requires overlapping instances:

{-# Language
    AllowAmbiguousTypes,
    FlexibleInstances,
    TypeFamilies #-}

-- The class of overloads of ‘f’.
class F a where
  type family T a   -- Or: ‘type T a’
  f :: T a -> T a

-- The “default” catch-all overload.
instance {-# Overlappable #-} F a where
  type instance T a = a  -- Or: ‘type T a = a’
  f x = x

-- More specific instance, selected when ‘a ~ Int’.
instance {-# Overlapping #-} F Int where
  type instance T Int = Int
  f x = x + 1

Then f @Int 1 gives 2, and f 'c' gives 'c'.

But in this case, type family is unnecessary because it happens to be the identity—I include it for the sake of giving a point of generalisation. If you want to produce types by pattern-matching on types just like a function, then a closed type family is a great fit:

{-# Language
    KindSignatures,
    TypeFamilies #-}

import Data.Int
import Data.Word
import Data.Kind (Type)

type family Unsigned (a :: Type) :: Type where
  Unsigned Int   = Word
  Unsigned Int8  = Word8
  Unsigned Int16 = Word16
  Unsigned Int32 = Word32
  Unsigned Int64 = Word64
  Unsigned a     = a

Back to your question, here’s the original example with plain typeclasses:

class F a where
  f :: a -> a

instance {-# Overlappable #-} F a where
  f x = x

instance {-# Overlapping #-} F Int where
  f x = x + 1

Unfortunately, there’s no notion of a “closed typeclass” that would allow you to avoid the overlapping instances. In this case it’s fairly benign, but problems with coherence can arise with more complex cases, especially with MultiParamTypeClasses. In general it’s preferable to add a new method instead of writing overlapping instances when possible.

Note that in either case, f now has an F a constraint, e.g. the latter is (F a) => a -> a. You can’t avoid some change in the type; in Haskell, polymorphic means parametrically polymorphic, to preserve the property that types can be erased at compile time.

Other options include a GADT:

data FArg a where
  FInt :: Int -> FArg Int
  FAny :: a -> FArg a

f :: FArg a -> a
f (FInt x) = x + 1  -- Here we have ‘a ~ Int’ in scope.
f (FAny x) = x

Or (already mentioned in other answers) a Typeable constraint for dynamic typing:

{-# Language
    BlockArguments,
    ScopedTypeVariables #-}

import Data.Typeable (Typeable, eqT)
import Data.Type.Equality ((:~:)(Refl))

f :: forall a. (Typeable a) => a -> a
f x = fromMaybe x do
  Refl <- eqT @a @Int
  pure (x + 1)

"Pattern-matching" types in Haskell

3 Answers3

Linked