[Haskell-cafe] Using existential types from TAPL book in Haskell

[David Feuer]

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>