
31 May
2007
31 May
'07
5:15 p.m.
In this function data C = C Int foo :: C -> C foo ~(C x) = C x foo is _not_ the identity: its result must be non bottom, i.e. the constructor C is "forced" to its argument. I wonder if a similar function is definable for existential types: data E = forall a . E a foo :: E -> E foo, as defined above does not work (lazy patterns not allowed), and in foo y = E (case y of E x -> x) a variable escapes. I also tried with CPS with no success. Is foo definable at all? I'm starting to think that it is not, and that there must be a very good reason for that... Thank you, Zun.