[Haskell-cafe] Existential problem
Niklas Broberg
niklas.broberg at gmail.com
Thu Mar 31 06:44:04 EST 2005
> > -- Explicitly recursive continuation type
> > data C t a = forall t2 . C (C t2 a -> IO t a)
>
> If you write
>
> data C t a = C (forall t2 . C t2 a -> IO' t a),
>
> it will compile (versions 6.2.2, 6.4). Whether that'll do exactly what you
> want, I don't know :-(
Actually, I think it does. Originally I thought this would be too
restrictive, since all possible continuations must then be polymorphic
in their argument, but in practise that's actually the case anyway.
:-)
> > transition :: Bool -> IO tx () -> IO t () -> IO t ()
> > transition b c d = undefined
> >
> > s1 :: C t () -> IO H ()
> > s1 (C k) = trans (True)
> > (k (C s1)) -- :: IO t ()
> > (s1 (C k)) -- :: IO H ()
>
> trans = transition, I suppose?
Indeed... the dangers of trimming code for the sake of presentation... :-)
> > --------------------------------------
> > The error message is:
> > Inferred type is less polymorphic than expected
> > Quantified type variable `t2' is unified with `H'
> > When checking an existential match that binds
> > k :: C t2 a -> IO t a
> > The pattern(s) have type(s): C t1 ()
> > The body has type: IO H ()
> > In the definition of `s1':
> > s1 (C k) = trans (True) (k (C s1)) (s1 (C k))
[...]
> Now I'm not an expert, but I think it's roughly thus:
> by the original definition, from the pattern 'C k', it follows that there is
> some type, call it t1, such that k has type
> C t1 () -> IO' t ().
> Now applying k to C s1 requires t1 to be H, which may or may not be the case,
> that can't be decided by pattern matching.
You are right of course. k is not polymorphic in its argument, since
t1 is not a type variable but an actual type. we just don't know which
type that is, and we certainly can't guarantee that it's H.
Moving the forall to make k polymorphic solves the problem, just like
you said above.
Thanks a lot,
/Niklas
More information about the Haskell-Cafe
mailing list