Are GADTs expressive? Simple proof-carrying code in Haskell98
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.
Hi, Oleg. It is nice to see how the eval function is encoded with type classes. I always wonder whether the HOAS example from Xi's POPL 03 paper can be programmed this way. In particular, it appears to me that the Fix clause requires non-inductive derivation of the form instance Eval (f e) a => Eval e a where eval e@(Fix f) = eval (f e) Any trick on getting this work? Meng -----Original Message----- From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of oleg@pobox.com Sent: 13 January 2007 09:20 To: haskell-cafe@haskell.org Subject: [Haskell-cafe] Are GADTs expressive? Simple proof-carrying code inHaskell98 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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On 1/13/07, oleg@pobox.com
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
See also Conor McBride's "Faking It: Simulating Dependent Types in Haskell" http://citeseer.ist.psu.edu/mcbride01faking.html Also, GADTs are extensible in GHC HEAD, though type classes are still necessary to write functions on them: http://haskell.org/haskellwiki/GHC/Indexed_types#Instance_declarations
Incidentally, the typeclass encoding has an advantage: If the submitted proof is invalid, the error will be reported at compile time. [more snipped]
I don't quite understand what you're getting at here. Is it that with the GADT approach, one could write Terminating (Apply omega omega) (undefined) (undefined) and the typechecker would not complain? That certainly is an issue, but I think you're saying something deeper that I'm not getting.
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 [snip] 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.
That's true, but there is at least one disadvantage to the PCC module: some functions manipulating terminating terms must be placed inside the trusted core. This is not the case with GADTs. For instance, we could write a term that takes a non-normalized (but terminating) term and beta-reduces it once to return a new normalizing term. We can't do this as a mere client of the PCC module without calling make_terminates again. Operations on types with hidden constructors sometimes have to be put in the trusted core. This was a small cost for terminating terms in the untyped lambda calculus, but it's a bigger cost for other structures. This is sort of like writing nested types for balanced trees vs. using Data.Set. Data.Set does guarantee that the tree is balanced, but we can only believe this after looking at each function in Data/Set.hs. Yes, the definition for balanced nested trees must be written with the same care as the functions in Data.Set, but there are a lot more functions in Data.Set Jim
participants (3)
-
Jim Apple -
Meng Wang -
oleg＠pobox.com