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" <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
participants (2)
-
David Feuer -
Dominik Bollmann