Find match a parametric parameter

Question

Is it possible to match a type parameter for an arbitrary type via type families or otherwise?

I attempt to write a type function

type family Match s t a

which takes a two structures, s, and t (which are assumed two different parameterizations of the same type, e.g. Maybe Int and Maybe String) and a parameter which will be matched against. If a matching parameter is found, the type function supplies the replacement. Otherwise it supplies the original parameter.

Match (Maybe a) (Maybe b) a ~ b
Match (Maybe a) (Maybe b) c ~ c 

My attempted implementation:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}

import Data.Type.Equality
import Data.Type.Bool

type family Match (s::k) (t::k) (a :: * ) :: * where
  Match (f a :: *) (g b :: *) c = If ((a == c)) b c

The family apparently works as planned when the parameter is found:

>  :t (undefined :: (Match (Maybe a) (Maybe b) a))
(undefined :: (Match (Maybe a) (Maybe b) a)) :: b

But not for when not matching:

 >  :t (undefined :: (Match (Maybe a) (Maybe b) c))
     Couldn't match type ‘If
                             ghc-prim-0.5.0.0:GHC.Types.*
                             (Data.Type.Equality.EqStar a0 c0)
                             b0
                             c0’
                     with ‘If
                             ghc-prim-0.5.0.0:GHC.Types.*   (Data.Type.Equality.EqStar a c) b c’
      Expected type: Match * (Maybe a) (Maybe b) c
        Actual type: Match * (Maybe a0) (Maybe b0) c0
      NB: ‘If’ is a type function, and may not be injective
      The type variables ‘a0’, ‘b0’, ‘c0’ are ambiguous
    • In the ambiguity check for an expression type signature
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In an expression type signature: Match (Maybe a) (Maybe b) c
      In the expression: (undefined :: Match (Maybe a) (Maybe b) c)

Is something like what I'm asking possible? It doesn't have to be type families, I'm open to other approaches. OTOH, will allowing ambiguous types help here? I don't know the pitfalls so I hesitate.

Thanks!

Answer 1

You are asking for two different things. You looked for

[a type function] which takes a two structures, s, and t (which are assumed two different parameterizations of the same type, e.g. Maybe Int and Maybe String) and a parameter which will be matched against. If a matching parameter is found, the type function supplies the replacement. Otherwise it supplies the original parameter.

You've already mostly written it. You should probably avoid using (==), because you are allowed to use nonlinear matching, which is generally superior:

type family Match (a :: i) (b :: i) (c :: o) :: o where
    Match (f a) (f b) a = b
    Match (f a) (f b) b = a
    Match _     _     c = c

Later, you define two functions, and you want both to compile.

undefined :: Match (Maybe a) (Maybe b) a
undefined :: Match (Maybe a) (Maybe b) c

The first one takes two types as arguments:

\@(a :: Type) @(b :: Type) -> (undefined :: Match (Maybe a) (Maybe b) a)

The type signature matches the first equation of Match, and reduces to a.

\@(a :: Type) @(b :: Type) -> (undefined :: a)

Which allows the correct parameters to be inferred for the function undefined:

\@a @(b :: Type) -> undefined @'GHC.Types.LiftedRep @a

The second function is

\@(a :: Type) @(b :: Type) @(c :: Type) -> (undefined :: Match (Maybe a) (Maybe b) c)

It would be incorrect to infer the argument to undefined as the type family application Match (Maybe a) (Maybe b) c. There are many questions about "ambiguous type" errors that contain the reason why. Rather, the type family application must be reduced. But it cannot reduce. It matches the third equation, but it also might match the first and second equations, if a ~ c or b ~ c, so it would be incorrect to jump to the fallback choice when the primary one is still available. You might ask, "why aren't a/b and c different?" The answer is that a, b, and c are just variables (which happen to be type variables) and are just names for values (which happen to be types). These values are given as arguments to your function. If I gave you x, y :: Int, and asked you for the value of if x == y then "Yes" else "No", you would not be able to tell me, because you do not know the values of x and y. Yet, you have asked Haskell, "Here, a, b, c :: Type. What is if a == c then b else if b == c then a else c?" That is just as unanswerable. There is no way to tell variables with equal values apart, because that would really undermine the foundations of Haskell.

Notice that there is a rather cheeky answer to the question I gave you. You can just say "the value of if x == y then "Yes" else "No" is if x == y then "Yes" else "No"." Analogously, I can go in and manually supply a type argument of an unreduced type family application to undefined to define your function, by allowing ambiguous types. There is no longer any need to infer what the argument to undefined is by trying (and failing) to reduce the Match application.

fun :: forall a b c. Match (Maybe a) (Maybe b) c
fun = undefined @_ @(Match (Maybe a) (Maybe b) c)

This neatly sidesteps the impossible question. The result type of fun is now deferred to when it is used, which is the power/curse of AllowAmbiguousTypes. Now, fun @Int @String @Int :: String, by the first equation, fun @Int @String @String :: Int, by the second equation, and fun @Int @String @Bool :: Bool, by the third equation. There is no way to make this function "choose" the third equation at the definition.