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

Dominik Bollmann dominikbollmann at gmail.com
Wed Apr 13 15:54:59 UTC 2016

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

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.

More information about the Haskell-Cafe mailing list