[Haskell-cafe] Termination of substitution
ndmitchell at gmail.com
Thu Mar 20 13:01:36 EDT 2008
Thanks for the interesting comments. Its looks like learning some of
the basics about System Fw is probably the way forward.
> However GHC goes beyond Fw by adding
> data types
> This blows strong normalisation out of the water. (Assuming you have reasonable rules for case and letrec.) But perhaps if you restrict data types a bit, and place draconian restrictions on letrec (e.g. never inline one) you could retain strong normalisation. It depends how much you want your rules to do.
I have restricted letrec appropriately. I haven't looked at the data
type problem, but given that GHC manages to ignore it, I think its
probably fair for me to ignore it for the time being.
Thanks very much for the helpful comments,
More information about the Haskell-Cafe