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.