[Haskell-cafe] GADTs are expressive

[John Meacham]

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⑈