# [Haskell-cafe] A Finally Tagless Pi Calculus

Dan Doel dan.doel at gmail.com
Wed Jun 9 14:48:59 EDT 2010

```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
```

More information about the Haskell-Cafe mailing list