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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe