[Haskell-cafe] Using existential types from TAPL book in Haskell

[Dominik Bollmann]

Hi all,

I'm currently reading Prof. Pierce's TAPL book. Reading the chapter on
existential types, I've been wondering how to use existentials in
Haskell.

In particular, in the TAPL book there is a section on purely functional
objects, which are encoded (e.g.) as follows:

counter = {*Nat, { state = 5
                 , methods = { get = \x:Nat. x
                             , inc = \x:Nat. succ x }
                 } } as Counter

where Counter = {∃X, { state : X
                     , methods = { get : X -> Nat
                                 , inc : X -> X }
                     } }

That is, a Counter consists of some internal state as well as methods
`get` to retrieve its state and `inc` to increment it.

Internally, a Counter is just implemented with a natural
number. However, from the outside, we hide this fact by making its state
an existential type X. Thus, we can only modify a Counter instance
(e.g., counter) using its exposed methods. For example,

let {X, body} = counter in body.methods.get (body.state)

(see Ch 24.2 on Existential Objects for further details)

I've been wondering how to write such counters in Haskell. In
particular, how to write a Counter instance like the above counter that
uses a concrete representation type Nat, while exposing its state to the
outside world abstractly with an existential type X. I've been trying to
do this, but so far I haven't succeeded...

If anyone could hint me at how to do this, would help me understanding
existentials better, I think :-).

Cheers, Dominik.