[Haskell-cafe] Using existential types from TAPL book in Haskell
David Feuer
david.feuer at gmail.com
Wed Apr 13 16:24:30 UTC 2016
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 at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160413/a5d06a23/attachment.html>
More information about the Haskell-Cafe
mailing list