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⑈ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe