[Haskell] Non-terminating compilation of non-positive construction.

[Simon Peyton-Jones]

It's a documented bug in GHC.

http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html#BUGS-G
HC

Simon

| -----Original Message-----
| From: haskell-bounces at haskell.org [mailto:haskell-bounces at haskell.org]
On Behalf Of Stefan
| Karrmann
| Sent: 05 September 2004 13:57
| To: haskell at haskell.org
| Subject: [Haskell] Non-terminating compilation of non-positive
construction.
| 
| Hi,
| 
| in Coq (cf. <http://pauillac.inria.fr/coq/coq1-eng.html>) inductive
and
| coinductive (aka lazy) types are restricted by the positivity
condition
| (cf.
<http://pauillac.inria.fr/coq/doc8/Reference-Manual006.html#htoc91>).
| 
| My first try to violate this condition in Haskell is:
| ---------------------------------------------------
| module Limits (module Limits) where
| 
| import qualified Prelude$
| $
| data False = False !False
|    deriving (Prelude.Show)
| -- Approximation of: data False = {- no Value -}
| -- The lazy variant has the same result.
| -- Of course there is: f = False f
| 
| data Non_positive = Non_pos (Non_positive -> False)
| 
| app :: Non_positive -> Non_positive -> False
| app f x = case f of
|    Non_pos h -> h x
| 
| delta :: Non_positive
| delta = Non_pos (\ x -> app x x)
| 
| -- Up to this definition ghc terminates.
| 
| -- (\x -> x x) (\x -> x x)
| loop :: False
| loop = app delta delta
| ----------------------------------------------------
| 
| The compilation by the Glorious Glasgow Haskell Compilation System,
| version 6.2, loops on this small module. IMHO only the execution
should
| loop or non positive constructions should be excluded.
| 
| Is it a bug or is non positivity too dangerous?
| 
| Sincerly,
| --
| Stefan Karrmann
| _______________________________________________
| Haskell mailing list
| Haskell at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell