Using existential types from TAPL book in Haskell
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.
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"
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
participants (2)
-
David Feuer -
Dominik Bollmann