<br><br><div class="gmail_quote">On Wed, Aug 17, 2011 at 4:49 PM, Tom Schouten <span dir="ltr"><<a href="mailto:tom@zwizwa.be">tom@zwizwa.be</a>></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' s i o = Kl' (i -> s -> (s, o))<br>
iso' :: (i -> Kl' s () o) -> Kl' s i o<br>
iso' f = Kl' $ \i s -> (\(Kl' kl') -> kl' () s) (f i)<br>
<br>
-- Is there a way to make this one work also?<br>
data Kl i o = forall s. Kl (i -> s -> (s, o))<br>
iso :: (i -> Kl () o) -> Kl i o<br>
iso f = Kl $ \i s -> (\(Kl kl) -> 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 -> s -> (s,o)) -- not legal haskell<br><br>where @s represents "hold a type s which can be used in the other elements of the structure". An example element of this type:<br><br>
KI @[Int] (\i s -> (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 -> case f i of ...)<br><br>What do we put in the ??. In fact, it's not possible to find a solution; consider this:<br>
<br>ki1 :: KI () Int<br>ki1 = KI @Int (\() s -> (s+1, s))<br><br>ki2 :: KI () Int<br>ki2 = KI @() (\() () -> ((), 0))<br><br>f :: Bool -> 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't match type `s0' with `s'<br>
because type variable `s' 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 -> s -> (s, o)) -> 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) -> kl () s<br>
In the expression: (\ (Kl kl) -> 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>