20 Mar
2008
20 Mar
'08
1:01 p.m.
Hi 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 letrec 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, Neil