[Haskell-cafe] GADTs are expressive
john at repetae.net
Tue Jan 23 23:17:52 EST 2007
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
John Meacham - ⑆repetae.net⑆john⑈
More information about the Haskell-Cafe