[Haskell-cafe] Are GADTs expressive? Simple proof-carrying code in Haskell98

[oleg at pobox.com]

Inspired by the recent post by Jim Apple, we demonstrate a datatype
`Terminates' that can hold only an assuredly terminating (strongly
normalizable) term in untyped lambda-calculus. Furthermore, the values
of the datatype `Terminates' contain all and only those untyped
lambda-calculus terms with that property. As in Jim Apple's solution,
to create the value `Terminates', the user submits the term in
question and the proof of its termination. The proof will be verified
-- and if it holds, the Terminates certificate will be created. As in
Jim Apple's solution, verification of the submitted proof has to be
done at run-time, to make sure the proof is not fake, that is, has no
undefined values. Our solution uses neither GADTs nor typeclasses; in
fact, it is in Haskell98. Also, the required proof from the user
couldn't be simpler.

Jim Apple wrote:
> To show how expressive GADTs are, the datatype Terminating can hold
> any term in the untyped lambda calculus that terminates, and none that
> don't. I don't think that an encoding of this is too surprising, but I
> thought it might be a good demonstration of the power that GADTs
> bring.
The shown GADT encoding seems to be of the kind that is convertible to
typeclasses in the straightforward way, see for example,
	http://pobox.com/~oleg/ftp/Haskell/GADT-interpreter.hs 

Inn this particular example, GADT do not bring any
power. Incidentally, the typeclass encoding has an advantage: If the
submitted proof is invalid, the error will be reported at compile
time. There is not even a possibility of a run-time error. This is
because the typeclasses approach does only type-level computations and
does not look at values at all (which may as well be
undefined). Placing a value into a (rank-1) datatype forces the
typechecker to resolve any constraints associated with the value, or
report an error if constraints are not satisfiable.

However, it seems that the problem at hand admits a far simpler
solution -- in Haskell98. The solution is in spirit of lightweight
static capabilities. Here it is:

> module PCC (Terminates,  -- data constructor is not exported
> 	      make_terminates, get_term) where
>
> import YourFavorite.Lambda_calc 
>
> data Terminates = Terminates{get_term::Term}
>
> make_terminates :: Term -> Integer -> Maybe Terminates
> make_terminates term limit = 
> 	case reduce_term_nsteps term limit of
> 	  Left _ -> Nothing
> 	  Right normal_form -> Just (Terminates term)


Because the data constructor is not exported, the only way to
construct a value `Terminates' from which a term can be extracted is
by invoking the function make_terminates. The function accepts a
lambda-term, and a proof of its termination. The proof takes the form
of the (upper bound of the) number of steps needed to normalize the
term. The function make_terminates checks the proof, by trying to
reduce the term that many steps. If the normal form is found in the
process, the term is normalizable and we create the
certificate. Otherwise, we conclude the termination proof does not
hold and we return Nothing. This proof checking is clearly decidable.

The module PCC constitutes the `trusted kernel' with respect to the
Terminates datatype. The function make_terminates must be rigorously
verified in order to deserve our trust. But the same should be said
for the GADT or any other solution: e.g., one can easily add a new
case alternative to the Normal datatype declaring Omega to be in the
normal form.