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 <[email protected]> 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
