Thu Aug 25 10:43:38 CEST 2011

Eliminating Existentials

I'm trying to represent a sequence as an initial value :: s and an
update function :: s -> (o,s).  According to Oleg's reply[2] pointing
to [1] it's possible to use laziness to avoid these kinds of
existentials, by applying them.

Some points from [1] that might be useful:

  - Replace functions that operate on hidden types with type class
    constraints (bounded quantification) if functions are constant
    over types.

  - Replace other such functions as thunks: "apply away" the hidden

In my case this would mean to repesent the type as a list [o], or a
list function [i] -> [o].  The problem then is of course that the
original function is not observable.

Maybe my original point is completely wrong then: the function is not
observable anyway, unless the state is somehow part of a class that
can allow initial values, "and" a run function that produces the

class InitState r where
  initFloat :: Float -> r Float
  initInt   :: Int   -> r Int
  run       :: (s, (s, i) -> (s, o)) -> ???

However, in case there is no structure that depends on input (No
Monad?) it should be possible to evaluate the update function
abstractly on a singleton list, obtaining the (i,s) -> o relation.
But this does not expose the state output.

It's actually not so hard: if I want to observe the state at some
point, I can't hide it completely.  Placing the evaluator in a type
class seems to be the thing to do.  This should allow evaluation to
list processors, and machine code separately.

But the stuff mentioned in the HC thread is quite interesting.  I
thought I understood then I see this weird other approach..  See next

[1] http://okmij.org/ftp/Computation/Existentials.html