Check when two type parameters are equals

Learn
1

Consider a datatype data Foo a with one type parameter.

Is there a way to write something like

data SameFoos = forall a. SameFoos (Foo a) (Foo a)

sameFoos :: Foo a -> Foo b -> Maybe SameFoos

which returns a Just if a and b are equal?

This is certainly possible with dependent types, what about in current Haskell?

2

Can you provide a program in a dependently typed language that does this? Or at least a sketch of what it would look like?

I think it might not be possible because you cannot simply pattern match on arbitrary types and there is no built-in decidable equality on types.

3

My Idris and Agda are too rusty to do it. I probably was too optimistic.

Thanks for pointing that out

4

Either statically-dispatched different code paths using type class, or dynamically at runtime using Typeable?

I don’t think the latter is necessary. I’m just pointing it out for completeness.

You can get away with the “UndecidableInstances” + “Overlappable” trick.

5

You need some run-time witness of the types to compare. The class Typeable provides features for this purpose:

sameFoos :: (Typeable a, Typeable b) => Foo a -> Foo b -> Maybe SameFoos

You can build a restricted variant of Typeable with GADTs, if you are okay with a closed universe of types (whereas Typeable is “open” because it automatically extends to newly declared types).

data MyTypeable a where
  MyInt :: MyTypeable Int
  MyBool :: MyTypeable Bool
  MyList :: MyTypeable a -> MyTypeable [a]
  MyPair :: MyTypeable a -> MyTypeable b -> MyTypeable (a, b)

sameFoos :: MyTypeable a -> MyTypeable b -> Foo a -> Foo b -> Maybe SameFoos
4 Likes
6 
newtype Foo a = Foo a
data SameFoos = forall a. Show a => SameFoos (Foo a) (Foo a)

deriving instance Show a => Show (Foo a)
deriving instance Show SameFoos

class SameFoosClass a b where
  sameFoos :: Foo a -> Foo b -> Maybe SameFoos

instance Show a => SameFoosClass a a where
  sameFoos a b = Just (SameFoos a b)

instance {-# OVERLAPPABLE #-} SameFoosClass a b where
  sameFoos _ _ = Nothing

main = do
  print $ sameFoos (Foo True) (Foo "hello")
  print $ sameFoos (Foo True) (Foo False)

without Typeable.

6 Likes
7

If Foo :: Type -> Type then Typeable is the answer, as suggested by others. If Foo :: k -> Type, for some other kind k, then SingI is the answer (and Typeable is basically the SingI of Type, so it’s a strict generalization).

8

To expand on Lysxia’s solution you can

sameFoos :: (Typeable a, Typeable b) => Foo a -> Foo b -> Maybe SameFoos
sameFoos bar baz = do
  Refl <- testEquality (typeRep @bar) (typeRep @baz)
  Just $ SameFoos bar baz

If you wanted to be even more of a charlatan:

sameFoos :: (Typeable a, Typeable b) => a -> b -> Maybe SameFoos
sameFoos bar baz = case typeRep @bar of
  App t1 t2 -> do 
       HRefl <- eqTypeRep t1 (typeRep @Foo) 
       Refl <- testEquality (typeRep @bar) (typeRep @baz)
       Just $ SameFoos bar baz
  _ -> Nothing

The second dynamically checks if both are Foo AND if the are the same kind of Foo.

I’d imagine dependent typing has a better solution than this or even the overlapping instances solution.

1 Like
9

You can also pass in TypeRep if it’s more convenient than type-classes:

sameFoos :: TypeRep a -> TypeRep b -> Foo a -> Foo b -> Maybe SameFoos
sameFoos a b x y = do
  HRefl <- eqTypeRep a b
  pure $ SameFoos x y

The Type.Reflection module makes it easy to convert between the two, but some programs are a bit easier/more direct with one or the other.

(This also “feels” a bit more like dependent types.)