Re: [Haskell-cafe] Re: Non-termination of type-checking
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
Re: [Haskell-cafe] Re: Non-termination of type-checking
On Friday 29 January 2010 5:26:28 pm Matthieu Sozeau wrote: > data R (c :: *) where >R :: forall c' :: * -> *, (c' (c' ()) -> False) -> R (c' ()). This is what the data declaration is. The c on the first line and the c on the second line are unrelated. It's sort of an oddity of GADT declarations; variables used between the 'data' and 'where' are just placeholders. With KindSignatures enabled, one could also write: data R :: * -> * where R :: (c (c ()) -> False) -> R (c ()) or explicitly quantify c in the constructor's type. That confused me at first, as well. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
On Fri, Jan 29, 2010 at 8:56 AM, wrote:
>
> 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 ())
>
> -- instantiate c to R, so (c (c ())) and R (c ()) coincide
> -- and we obtain a recursive type
> --mu R. (R (R ()) -> False) -> R (R ())
>
> cond_false :: R (R ()) -> False
> cond_false x@(R f) = f x
>
> absurd :: False
> absurd = cond_false (R cond_false)
>
>
GHC (the compiler terminates)
The following variants terminate, either with GHCi or GHC,
absurd1 :: False
absurd1 = let x = (R cond_false)
in cond_false x
absurd2 = R cond_false
absurd3 x = cond_false x
absurd4 :: False
absurd4 = absurd3 absurd2
This suggests there's a bug in the type checker.
If i scribble down the type equation, I can't see
why the type checker should loop here.
-Martin
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Non-termination of type-checking
On Friday 29 January 2010 2:56:31 am o...@okmij.org wrote:
> 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 ())
>
> -- instantiate c to R, so (c (c ())) and R (c ()) coincide
> -- and we obtain a recursive type
> --mu R. (R (R ()) -> False) -> R (R ())
>
> cond_false :: R (R ()) -> False
> cond_false x@(R f) = f x
>
> absurd :: False
> absurd = cond_false (R cond_false)
This example is pretty weird in my view. For instance, consider:
data S x
type family T x :: *
type family T () = R ()
type family T (R ()) = S ()
s'elim :: S x -> False
s'elim x = undefined -- case x of {}
what :: T (T ()) -> False
what = s'elim
Now, we have T () ~ R (), and T (T ()) ~ S (R ()), so R (T ()) ~ R (R ()), no?
And T :: * -> *, so it should be an acceptable argument to R. So, one would
expect that I could write:
r :: R (R ()) -- R (T ())
r = R what
However, neither of those signatures for r goes through. With the second, I
get a complaint that:
Couldn't match expected type `S ()' against inferred type `()'
Expected type: S (S ())
Inferred type: T (T ())
though I'm not quite sure how it gets that error. With the R (R ()) choice, I
get:
Couldn't match expected type `R (R ())'
against inferred type `T (T ())'
NB: `T' is a type function, and may not be injective
but the injectivity GHC seems to be relying on isn't F x ~ F y => x ~ y, but:
f T ~ g T => f ~ g
or injectivity of ($ ()) in this case, so to speak. But this seems like a
significantly weirder thing to take for granted than injectivity of type
constructors. I suppose it's sufficient to limit c (in the constructor R's
definition) to accept only data type constructors, but that's significantly
more limiting than I'd expect to be the case (although, it does appear to be
what GHC does).
Anyhow, I don't particularly find this 'scary', as Haskell/GHC isn't
attempting to be an environment for theorem proving, and being able to encode
(\x -> x x) (\x -> x x) through lack of logical consistency isn't giving up
anything that hasn't already been given up multiple times (through general
recursion, error and negative types at least). Non-termination of type
checking is undesirable, of course.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
