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

[Jim Apple]

On 1/13/07, oleg at pobox.com <oleg at pobox.com> wrote:
> 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