[Haskell-cafe] Synthetic values?

[Chris Smith]

On Wed, 2011-02-09 at 18:15 +0100, Cristiano Paris wrote:
> I've a type problem that I cannot solve and, before I keep banging my
> head against an unbreakable wall, I'd like to discuss it with the
> list.

If I'm understanding your high-level goals correctly, then you're going
about things the wrong way.  It looks like in your "Sealed" type, you're
accumulating a list of type class constraints that are needed by a
phantom type, in order to access the value.  But type classes are open;
anyone can make any new type an instance of the type class whenever they
want.

In particular, you say:

> ------------
> unseal :: p -> Sealed p a -> a
> unseal _ (Sealed x) = x
> ------------
> 
> Basically this function requires a witness value of the type p to
> peel-off the Sealed value. Notice that:
> 
> ------------
> unseal undefined $ appendLog "Foo" "Bar"
> ------------
> 
> won't work as the undefined value is unconstrained. That's good,
> because otherwise it'd very easy to circumvent the enforcing
> mechanism.

This is not true, though.  One could just as easily write:

    data Dummy
    instance PRead Dummy
    instance PWrite Dummy

    unseal (undefined :: Dummy) $ appendLog "Foo" "Bar"

and they've circumvented your security checks.

I think you'll need to back up and rethink your base strategy.  Without
really understanding fully what you want, I'll still point out that
there are tricks with existentials that work when you need someone to
have an authentic token to do something; e.g., see the ST monad.

-- 
Chris Smith