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
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