[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
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.
More information about the Haskell-Cafe
mailing list