Sun Aug 14 21:29:21 CEST 2011

Existential types

When using existential quantification[1], you can't actually do
anything with the values, because you don't know the type!

i.e. the difference between these two:

     data Foo   = forall a. Foo a
     data Bar a = Bar a

is that for Foo we don't know what type a is, and because Foo doesn't
have type parameters, we can't specify it elsewhere either.

Practically that means that for Foo, we can't really do anything with
the values it wraps because we just don't know the types.

I see two ways around this.  One is explained in [1] and it boils down
to giving information about a, i.e.

      data FooShow = forall a. Show a => Foo a

Here we still don't know what type a is, but we know that we can apply
the operations from the Show class to values wrapped by the Foo
constructor.  ( It seems this can't be done using a field accessor,
but it is possible with pattern matching. )

Another way is to use the quantified variable more than once.

      data FooApp = forall a. Foo a (a -> Int)

Here we still don't know anything about the type, but we know that we
can apply Foo's second argument to its first to obtain an Int.  This
is the trick I've used in the a state-space model (SSM) to record
initial state and state transition together.  The only operation
that's ever performed on state is to pass it to the state transition

I used existential types to make the following composition operation
on state machines fit the Category class.  This required that the
state parameter is hidden.

chainSSM :: ((a, s1) -> (b, s1)) ->
            ((b, s2) -> (c, s2)) ->
            (a, (s1,s2)) -> (c, (s1,s2))

chainSSM f g = fg where
  fg (a, (s1,s2)) = (c, (s1',s2')) where
    (b, s1') = f (a, s1)
    (c, s2') = g (b, s2)

data SSM i o = forall s. SSM s ((i, s) -> (o, s))

-- If this would be (SSM s i o) then the composition operation would
-- have been :: SSM s2 b c -> SSM s1 a b -> SSM (s1,s2) a c
-- which doesn't fit :: SSM b c -> SSM a b -> SSM a c

instance Category SSM where
  (.) (SSM f0 f) (SSM g0 g) = SSM (g0,f0) $ g `chainSSM` f
  id  = SSM () $ id

As is mentioned in a post in [2], universals give generics: we don't
know what the type is, and we don't care since we only pass values
around.  Existentials give interfaces: we don't know what the exact
type is but we do care that we can perform a number of operations from
a given interface.

[1] http://www.haskell.org/haskellwiki/Existential_type
[2] http://stackoverflow.com/questions/292274/what-is-an-existential-type