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

[Ryan Ingram]

But your example uses a recursive type; the interesting bit about this
example is that there is no recursive types or function, and yet we
can encode this loop.

  -- ryan

On Wed, Jan 27, 2010 at 4:49 PM, Matthew Brecknell
<matthew at brecknell.net> wrote:
> Ryan Ingram wrote:
>> The compiler doesn't loop for me with GHC6.10.4; I think GADTs still
>> had some bugs in GHC6.8.
>>
>> That said, this is pretty scary.  Here's a simplified version that
>> shows this paradox with just a single GADT and no other extensions.
>> No use of "fix" or recursion anywhere!
>>
>> {-# LANGUAGE GADTs #-}
>> module Contr where
>>
>> newtype I f = I (f ())
>> data R o a where R :: (a (I a) -> o) -> R o (I a)
>>
>> run :: R o (I (R o)) -> R o (I (R o)) -> o
>> run x (R f) = f x
>> rir :: (R o) (I (R o))
>> rir = R (\x -> run x x)
>>
>> absurd :: a
>> absurd = run rir rir
>
> I think that's essentially the same as this:
>
> data Fix a = Fix { unFix :: Fix a -> a }
>
> run :: Fix a -> Fix a -> a
> run x f = unFix f x
>
> rir :: Fix a
> rir = Fix (\x -> run x x)
>
> absurd :: a
> absurd = run rir rir
>
> Non-positive recursive occurrences in type definitions provide various
> ways to encode the Y-combinator in a typed lambda calculus, without the
> need for any recursive "let" primitive. Haskell allows such non-positive
> occurrences, but for strong normalisation, languages like Coq must
> disallow them.
>
> If you change "data" to "newtype" in the above, the GHC 6.10.4 compiler
> (but not GHCi) will loop. I think this is just a case of the infelicity
> documented here:
>
> http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html
>
> Regards,
> Matthew
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>