[email protected]
[Top] [All Lists]

Re: [Haskell-cafe] Re: Non-termination of type-checking

Subject: Re: [Haskell-cafe] Re: Non-termination of type-checking
From: Daniel Fischer
Date: Fri, 29 Jan 2010 23:48:15 +0100
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 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
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe

<Prev in Thread] Current Thread [Next in Thread>