Am Freitag 29 Januar 2010 23:26:28 schrieb Matthieu Sozeau: > Le 29 janv. 10 à 02:56, o...@okmij.org 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 non-recursive 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 > > type-checking. It type-checks when we comment-out 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe