[Haskell-cafe] restricted existential datatypes

[oleg at pobox.com]

Misha Aizatulin wrote
>   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

It seems what you'd like is an opaque datum that responds to
(generally open) set of messages giving a reply dependent on a
message. Sounds like an object, doesn't it? Why does it have to be an
existential? True, existentials (that is, type abstraction) is one way
to implement objects. There are other ways.

Let's consider a very simple example:

> data Box = forall a . Show a  => Box a
> f (Box a) = show a

Now, the *only* meaningful thing we can do with the value `a' after 
unboxing is to pass it to the function `show'. Right? One may wonder
why not to perform this application to show right upfront:

> data Box1 = Box1 String
> box a = Box1 (show a)

This is _precisely_ equivalent to the above. Thanks to lazy
evaluation, the application `show a' won't be evaluated unless we
really need its value. The obvious benefit of Box1 is the simplicity
of it: no existentials. 

The value 'Box1' is an object that responds to only one message,
`show'. We'd like to have several messages, and we'd like to have the
set of messages open. There are two choices: HList or the
typeclasses. Both do the same thing, only the heterogeneous set of
dictionaries is explicit in the former approach and implicit in the
latter. Given below is the example. The box data constructor can be
hidden in a module; its details are not important anyway. What is
important is the membership in the Boxable class. The code below
works with GHC 6.4.1 (no advanced versions required) and even in Hugs.


{-# OPTIONS -fglasgow-exts #-}
module RestrictedEx where

-- Box labeled l responding to a message msg gives the result x
class Boxable l msg x | l msg -> x where
    box_value :: l -> msg -> x

-- A few message labels
data SHow = SHow
data CastToInt = CastToInt
data Print = Print

-- Create one box
data MyBox1 = MyBox1 String

-- Define its response to messages

instance Boxable MyBox1 SHow String where
    box_value (MyBox1 s) _ = s

instance Boxable MyBox1 Print (IO ()) where
    box_value (MyBox1 s) _ = putStrLn s

-- A function that takes any box that can be shown
f1 :: Boxable b SHow String => b -> String
f1 b = box_value b SHow