[Haskell-cafe] A Finally Tagless Pi Calculus

[Dan Doel]

On Wednesday 09 June 2010 2:32:29 pm Dupont Corentin wrote:
> I am making a little GATD:
> > {-# LANGUAGE GADTs#-}
> > 
> > data Obs a where
> > 
> >     Equal :: Obs a -> Obs a -> Obs Bool
> >     Plus :: (Num a) => Obs a -> Obs a -> Obs a
> 
> (etc..)
> 
> > instance Show t => Show (Obs t) where
> > 
> >     show (Equal a b) = (show a) ++ " Equal " ++ (show b)
> >     show (Plus a b) = (show a) ++ " Plus " ++ (show b)
> > 
> > instance Eq t => Eq (Obs t) where
> > 
> >     a `Equal` b == c `Equal` d = (a == c) && (b == d)
> >     a `Plus` b == c `Plus` d = (a == c) && (b == d)

Your two symptoms have the same underlying cause. The 'a' in Equal is 
existentially quantified. It might help to think about bundling the type in 
the Equal constructor:

  Equal T x y :: Obs Bool
   where
   T :: *
   x :: Obs T
   y :: Obs T

Now we write:

  show (Equal T x y) = ...

but we have no evidence that (Show T), so we cannot conclude (Show (Obs T)), 
and thus cannot use show on x and y.

Similarly:

  Equal T x y == Equal T' x y = ...

Your definition assumes that T = T' (or, it assumes that Obs T = Obs T', but 
that reduces to T = T'), but we have no reason to suspect that is the case. 
Hence the mismatch.

The first can be solved by putting a Show constraint on the type of the Equal 
constructor, if that's what you really want. The second can probably only be 
solved by having Equal take some kind of type rep, and checking that the types 
are equal.

Hope that helps.
-- Dan