BadInHaskell

See the official user manual for the most up-to-date version of the information on this page.

In the code below we show how can one define a looping computation in Haskell using a non strictly-positive datatype. This is the reason we don't allow this kind of inductive datatypes in Agda.

 module Bad where

 data Bad = Bad (Bad -> Bad)

 instance Show Bad where
   show (Bad _) = "BAD"

 getFun :: Bad -> (Bad -> Bad)
 getFun (Bad f) = f

 omega :: Bad -> Bad
 omega f = (getFun f) f

 loop :: Bad
 loop = omega (Bad omega)

 -- We have an infinite unfolding
 -- loop = omega (Bad omega) = (getFun (Bad omega)) (Bad omega) = omega (Bad omega) = loop