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
Page last modified on December 14, 2018, at 06:35 pm
Powered by
PmWiki