[Haskell-cafe] GADTs are expressive

[Roberto Zunino]

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

data Nat t where
    Z :: Nat Zero
    S :: ! Nat t -> Nat (Succ t)

Now one could safely write

foo :: Nat t -> A t -> B
foo proof value = proof `seq`
    -- here you can assume t to be a finite type-level natural

If proof is invalid, foo will return _|_.

Using no strictess annotation, but still using seq instead of deepSeq, 
the code above would be unsafe, since one can always pass (S undefined) 
as proof.

Using seq also allows to check the proof in constant time (neglecting 
the proof generation time, of course). deepSeq instead would require 
traversing the proof each time one wants to check it, e.g. in different 
functions.

Does anyone else believe that using strictess annotations in GADT proof 
terms would be good style?

Zun.