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.