Is there a way to bind the supressed type variable of an existential data type during pattern matching?

Question

Using GADTs, I have defined a depth-indexed tree data type (2–3 tree). The depth is there to statically ensure that the trees are balanced.

-- Natural numbers
data Nat = Z | S Nat

-- Depth-indexed 2-3 tree
data DT :: Nat -> Type -> Type where
  -- Pattern of node names: N{#subtrees}_{#containedValues}
  N0_0 :: DT Z a
  N2_1 :: DT n a -> a -> DT n a
    -> DT (S n) a
  N3_2 :: DT n a -> a -> DT n a -> a -> DT n a
    -> DT (S n) a

deriving instance Eq a => Eq (DT n a)

Now, some operations (e.g. insertion) might or might not change the depth of the tree. So I want to hide it from the type signature. I do this using existential data types.

-- 2-3 tree
data T :: Type -> Type where
  T :: {unT :: DT n a} -> T a

insert :: a -> T a -> T a
insert x (T dt) = case dt of
  N0_0 -> T $ N2_1 N0_0 x N0_0
  {- ... -}

So far so good. My problem is: I don't see how I can now define Eq on T.

instance Eq a => Eq (T a) where
  (T x) == (T y) = _what

Obviously, I would like to do something like this:

(T {n = nx} x) == (T {n = ny} y)
  | nx == ny = x == y
  | otherwise = False

I don't know how / whether I can bind the type variables in the patter match. And I am neither sure how to compare them once I get them. (I suspect Data.Type.Equality is for this, but I haven't seen any example of it in use.)

So, is there a way to implement the Eq (T a) instance, or is there some other approach that is recommended in this case?

Answer 1

You could use Data.Coerce.coerce to compare the contents of the trees: as long as you label the depth parameter as phantom, it should be willing to give you coerce :: DT n a -> DT m a.

But this doesn't really solve the problem, of course: you want to know if their types are the same. Well, maybe there is some solution with Typeable, but it doesn't sound like much fun. Absent Typeable, it seems impossible to me, because you want two contradictory things.

First, you want that trees of different depths should be separate types, not intermixable at all. This means everyone who handles them has to know what type they are.

Second, you want that you can give such a tree to someone without telling them how deep it is, have them munge it around arbitrarily, and then give it back to you. How can they do that, if you require type knowledge to operate on them?

Existentials do not "suppress" type information: they throw it away. Like all type information, it is gone at runtime; and you've made it invisible at compile time too.

I'm also not sure your problem is just with Eq: how will you even implement functions like insert? It's easy for N0_0, because that is known to have type DT Z a, but for the other cases I don't see how you will construct a DT (S n) a to wrap in your T when you can't know what n was.

Answer 2

You should write a depth-independent equality operator, which is able to compare two trees even if they have different depths n and m.

dtEq :: Eq a => DT n a -> DT m a -> Bool
dtEq N0_0                  N0_0                  = True
dtEq (N2_1 l1 x1 r1)       (N2_1 l2 x2 r2)       =
   dtEq l1 l2 && x1 == x2 && dtEq r1 r2
dtEq (N3_2 a1 x1 b1 y1 c1) (N3_2 a2 x2 b2 y2 c2) = 
   dtEq a1 a2 && x1 == x2 && dtEq b1 b2 && y1 == y2 && dtEq c1 c2
dtEq _                     _                     = False

Then, for your existential type:

instance Eq a => Eq (T a) where
  (T x) == (T y) = dtEq x y

Even if in the last line the depths are unknown (because of the existential), it won't matter for dtEq since it can accept any depth.

Minor side note: dtEq exploits polymorphic recursion, in that recursive calls can use a different depth from the one in the original call. Haskell allows polymorphic recursion, as long as an explicit type signature is provided. (We need one anyway, since we are using GADTs.)