<p dir="ltr">In Haskell, this looks like</p>
<p dir="ltr">data Counter where<br>
  Counter :: forall x . x -> (x -> Nat) -> (x -> x) -> Counter</p>
<p dir="ltr">Then</p>
<p dir="ltr">getNat :: Counter -> Nat<br>
getNat (Counter x get _) = get x</p>
<p dir="ltr">incNat :: Counter -> Counter<br>
incNat (Counter x get inc) = Counter (inc x) get inc</p>
<p dir="ltr">simpleCounter :: Nat -> Counter<br>
simpleCounter n = Counter n id (1 +)</p>
<p dir="ltr">mkCounter :: Integral n => n -> Counter<br>
mkCounter n<br>
  | n < 0 = error "Counters can't be negative."<br>
  | otherwise = Counter n fromIntegral (1 +)</p>
<p dir="ltr">All that said, this is not a great use-case for existentials, and in Haskell you'd be better off with</p>
<p dir="ltr">class Counter n where<br>
  getNat :: n -> Nat<br>
  step :: n -> n</p>
<div class="gmail_quote">On Apr 13, 2016 11:53 AM, "Dominik Bollmann" <<a href="mailto:dominikbollmann@gmail.com">dominikbollmann@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
Hi all,<br>
<br>
I'm currently reading Prof. Pierce's TAPL book. Reading the chapter on<br>
existential types, I've been wondering how to use existentials in<br>
Haskell.<br>
<br>
In particular, in the TAPL book there is a section on purely functional<br>
objects, which are encoded (e.g.) as follows:<br>
<br>
counter = {*Nat, { state = 5<br>
                 , methods = { get = \x:Nat. x<br>
                             , inc = \x:Nat. succ x }<br>
                 } } as Counter<br>
<br>
where Counter = {∃X, { state : X<br>
                     , methods = { get : X -> Nat<br>
                                 , inc : X -> X }<br>
                     } }<br>
<br>
That is, a Counter consists of some internal state as well as methods<br>
`get` to retrieve its state and `inc` to increment it.<br>
<br>
Internally, a Counter is just implemented with a natural<br>
number. However, from the outside, we hide this fact by making its state<br>
an existential type X. Thus, we can only modify a Counter instance<br>
(e.g., counter) using its exposed methods. For example,<br>
<br>
let {X, body} = counter in body.methods.get (body.state)<br>
<br>
(see Ch 24.2 on Existential Objects for further details)<br>
<br>
I've been wondering how to write such counters in Haskell. In<br>
particular, how to write a Counter instance like the above counter that<br>
uses a concrete representation type Nat, while exposing its state to the<br>
outside world abstractly with an existential type X. I've been trying to<br>
do this, but so far I haven't succeeded...<br>
<br>
If anyone could hint me at how to do this, would help me understanding<br>
existentials better, I think :-).<br>
<br>
Cheers, Dominik.<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>