[Haskell-cafe] restricted existential datatypes

[Misha Aizatulin]

hi,

  I am wondering whether it would be possible to use the existing
haskell type system to simulate a certain feature. Namely, I am trying
to apply ideas from [1] to existential datatypes. First I will describe
the problem and later say something about the context in which it arose.

  I am using existential boxes like
> data Box cxt = forall a . Sat (cxt a) => Box a
  here Sat is taken from [1]:
> class Sat a where dict :: a

  The result is a box type which can have variable context imposed on
its contents. What I noticed is that sometimes I want to write functions
that operate on the Box and make use of some part of the context without
knowing the context completely. Such a function would look something
like this:

> f :: (Contains cxt ShowCxt) => Box cxt -> String
> f (Box a) = show a

  The type is meant to say that the context of the box must contain Show
as one of the classes. I would imagine the Contains class to be
something like

> class Contains cxt subCxt where
>   subDict :: cxt a -> subCxt a

  Now inside f I would like to have the real (Show a) context available.
So I'd have an instance

> (Sat cxt a, Contains cxt ShowCxt) => Show a where
>   show = -- <the show function extracted from (subDict dict)>

  This instance of course does not work in ghc, because cxt is
hanging in the air - I get an error whenever it tries to infer (Show a).

  The question I'd like to ask is whether there is some trickery to
circumvent this problem. In the f function I'd like to be able to hint
to the compiler that I want Show to be derived from cxt which is
attached to the Box, but I see no way of doing that. (This by the way
seems connected to
http://www.mail-archive.com/haskell@haskell.org/msg19564.html).

  Now a couple of words about where I stumbled upon this problem. I am
writing a program that is supposed to use plugins. The plugins operate
among other things on Boxes as above. Now some plugins would like to
demand some additional capabilities from the Box that cannot be foreseen
at the spot where Box is defined. Parametrizing over context seems a
very natural solution to me - leading to the problem above.

  I would be very thankful for any suggestions!

Cheers,
  Misha Aizatulin

1. John Hughes, "Restricted Data Types in Haskell", September 4, 1999