[Top] [All Lists]

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

 Subject: Re: [Haskell-cafe] Re: Non-termination of type-checking Dan Doel Fri, 29 Jan 2010 07:24:21 -0500
 ```On Friday 29 January 2010 2:56:31 am [email protected] 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 [email protected](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 [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe ```
 Current Thread [Haskell-cafe] Re: Non-termination of type-checking, oleg Re: [Haskell-cafe] Re: Non-termination of type-checking, Dan Doel <= Re: [Haskell-cafe] Re: Non-termination of type-checking, Martin Sulzmann [Haskell-cafe] Re: Non-termination of type-checking, Matthieu Sozeau