
Am Freitag 29 Januar 2010 23:26:28 schrieb Matthieu Sozeau:
> Le 29 janv. 10 à 02:56, [email protected] a écrit :
> > Here is a bit more simplified version of the example. The example has
> > no value level recursion and no overt recursive types, and no
> > impredicative
> > polymorphism. The key is the observation, made earlier, that two types
> > c (c ()) and R (c ())
> > unify when c = R. Although the GADTs R c below is not recursive, when
> > we instantiate c = R, it becomes recursive, with the negative
> > occurrence. The trouble is imminent.
> >
> > We reach the conclusion that an instance of a nonrecursive GADT
> > can be a recursive type. GADT may harbor recursion, so to speak.
> >
> > The code below, when loaded into GHCi 6.10.4, diverges on
> > typechecking. It typechecks when we commentout absurd.
> >
> >
> > {# LANGUAGE GADTs, EmptyDataDecls #}
> >
> > data False  No constructors
> >
> > data R c where  Not recursive
> > R :: (c (c ()) > False) > R (c ())
>
> Thanks Oleg,
>
> that's a bit simpler indeed. However, I'm skeptical on
> the scoping of c here.
The c in "data R c" has nothing to do with the c in
"R :: (c (c ()) > False) > R (c ())"
It would probably have been less confusing to declare it
data R :: * > * where
R :: (c (c ()) > False) > R (c ())
> Correct me if I'm wrong but in R's
> constructor [c] is applied to () so it has to be a type
> constructor variable of kind :: * > s. But [c] is also
> applied to [c ()] so we must have s = * and c :: * > *.
> Now given the application [R (c ())] we must have
> [R :: * > *]. Then in [data R c] we must have [c :: *],
> hence a contradiction?
>
> My intuition would be that the declaration is informally
> equivalent to the impredicative:
>
> data R (c :: *) where
> R :: forall c' :: * > *, (c' (c' ()) > False) > R (c' ()).
>
>  Matthieu
_______________________________________________
HaskellCafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskellcafe

