In Haskell, this looks like data Counter where Counter :: forall x . x -> (x -> Nat) -> (x -> x) -> Counter Then getNat :: Counter -> Nat getNat (Counter x get _) = get x incNat :: Counter -> Counter incNat (Counter x get inc) = Counter (inc x) get inc simpleCounter :: Nat -> Counter simpleCounter n = Counter n id (1 +) mkCounter :: Integral n => n -> Counter mkCounter n | n < 0 = error "Counters can't be negative." | otherwise = Counter n fromIntegral (1 +) All that said, this is not a great use-case for existentials, and in Haskell you'd be better off with class Counter n where getNat :: n -> Nat step :: n -> n On Apr 13, 2016 11:53 AM, "Dominik Bollmann" <dominikbollmann@gmail.com> wrote:
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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe