<br><br><div class="gmail_quote">On Wed, Aug 17, 2011 at 4:49 PM, Tom Schouten <span dir="ltr">&lt;<a href="mailto:tom@zwizwa.be">tom@zwizwa.be</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
{-# LANGUAGE ExistentialQuantification #-}<br>
<br>
-- Dear Cafe, this one works.<br>
data Kl&#39; s i o = Kl&#39; (i -&gt; s -&gt; (s, o))<br>
iso&#39; :: (i -&gt; Kl&#39; s () o) -&gt; Kl&#39; s i o<br>
iso&#39; f = Kl&#39; $ \i s -&gt; (\(Kl&#39; kl&#39;) -&gt; kl&#39; () s) (f i)<br>
<br>
-- Is there a way to make this one work also?<br>
data Kl i o = forall s. Kl (i -&gt; s -&gt; (s, o))<br>
iso :: (i -&gt; Kl () o) -&gt; Kl i o<br>
iso f = Kl $ \i s -&gt; (\(Kl kl) -&gt; kl () s) (f i)<br></blockquote><div><br>Not without moving the quantifier, as Oleg says.  Here is why:<br><br>Existential types are equivalent to packing up a type with the constructor; imagine KI as<br>
<br>data KI i o = KI @s (i -&gt; s -&gt; (s,o))   -- not legal haskell<br><br>where @s represents &quot;hold a type s which can be used in the other elements of the structure&quot;.  An example element of this type:<br><br>
  KI @[Int] (\i s -&gt; (i:s, sum s)) :: KI Int Int<br><br>Trying to implement iso as you suggest, we end up with<br><br>iso f = KI ?? (\i s -&gt; case f i of ...)<br><br>What do we put in the ??.  In fact, it&#39;s not possible to find a solution; consider this:<br>
<br>ki1 :: KI () Int<br>ki1 = KI @Int (\() s -&gt; (s+1, s))<br><br>ki2 :: KI () Int<br>ki2 = KI @() (\() () -&gt; ((), 0))<br><br>f :: Bool -&gt; KI () Int<br>f x = if x then ki1 else ki2<br><br>iso f = KI ?? ??<br><br>The problem is that we have multiple possible internal state types!<br>
<br>  -- ryan<br><br></div><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<br>
{-<br>
    Couldn&#39;t match type `s0&#39; with `s&#39;<br>
      because type variable `s&#39; would escape its scope<br>
    This (rigid, skolem) type variable is bound by<br>
      a pattern with constructor<br>
        Kl :: forall i o s. (i -&gt; s -&gt; (s, o)) -&gt; Kl i o,<br>
      in a lambda abstraction<br>
    The following variables have types that mention s0<br>
      s :: s0 (bound at /home/tom/meta/haskell/iso.hs:<u></u>11:17)<br>
    In the pattern: Kl kl<br>
    In the expression: \ (Kl kl) -&gt; kl () s<br>
    In the expression: (\ (Kl kl) -&gt; kl () s) (f i)<br>
-}<br>
<br>
<br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br>