On Mon, Jan 08, 2007 at 09:48:09PM +0100, Roberto Zunino wrote:
Robin Green wrote:
Well, not really - or not the proof you thought you were getting. As I am constantly at pains to point out, in a language with the possibility of well-typed, non-terminating terms, like Haskell, what you actually get is a "partial proof" - that *if* the expression you are demanding terminates, you will get a value of the correct type.
I only want to point out that the above "terminates" actually is "can be put in NF", since putting the expression in WHNF is not enough. In other words, you need deepSeq, not seq when forcing/checking proofs.
To partially mitigate this problem, I believe strictness annotations can be used, as in
jhc allows (in special cases at the moment, in full generality hopefully soon) the declaration of new strict boxed types.
data StrictList a :: ! = Cons a (StrictList a) | Nil
I think this could be used to help the situation, as absence analysis can discard unused portions since there is no need to deepSeq everything. John -- John Meacham - ⑆repetae.net⑆john⑈