Reducing the use of dependent types in saw-core

[brianhuffman]

In particular, it would be beneficial to remove the size parameter from the saw-core Vec type, and have the type include vectors of all lengths (like the Haskell list type). We should consider removing other uses of dependent types as well.

Problems caused by dependent types:

• The saw-core type checker is quite complicated, and must evaluate terms (especially those of type Nat) during type checking
• In practice, unsafeCoerce is often necessary to circumvent the type system (e.g. in the Cryptol translator)
• Rewriting on terms is not guaranteed to preserve well-typedness (this most commonly shows up when rewriting size parameters on type Vec)
• Many potentially useful rewrite rules are not expressible in a well-typed form (e.g. associativity of append)

Challenges:

• Using ordinary saw-core lambdas to represent quantifiers in proofs won't work. We will need to encode quantifiers as bounded quantifiers that explicitly state the sizes.
• We won't be able to use the type checker to ensure that imported terms don't have size mismatch errors. We will need to implement a separate checker for that.

[kiniry]

On May 19, 2016, at 17:30, brianhuffman [email protected] wrote:

In particular, it would be beneficial to remove the size parameter from the saw-core Vec type, and have the type include vectors of all lengths (like the Haskell list type). We should consider removing other uses of dependent types as well.

Problems caused by dependent types:

The saw-core type checker is quite complicated, and must evaluate terms (especially those of type Nat) during type checking
In practice, unsafeCoerce is often necessary to circumvent the type system (e.g. in the Cryptol translator)
Rewriting on terms is not guaranteed to preserve well-typedness (this most commonly shows up when rewriting size parameters on type Vec)
Many potentially useful rewrite rules are not expressible in a well-typed form (e.g. associativity of append)
Challenges:

Using ordinary saw-core lambdas to represent quantifiers in proofs won't work. We will need to encode quantifiers as bounded quantifiers that explicitly state the sizes.
We won't be able to use the type checker to ensure that imported terms don't have size mismatch errors. We will need to implement a separate checker for that.
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly or view it on GitHub #136

This is a bold proposal, Brian. Why throw the baby out with the bathwater, and instead just go ahead and mechanize the type system, evolving it with a goal toward improving/correcting those first four bullets?

[brianhuffman]

@kiniry Yes it is bold, but I wouldn't say we're throwing out the baby. I think we've kept our dependent type system much too long as a result of a sunk-cost fallacy, and we will have a much easier time going forward without it. If we keep our dependent types, then fixing the bullet points above will be a major original research project. We can't just take any existing dependent type system off the shelf, because we have a unique combination of special features: type-level proofs coexisting with recursive definitions; a large collection of built-in datatypes and primitive functions; a very complex (undecidable) equational theory involving natural numbers that the type system and unification/matching are supposed to take into account.

In contrast, the "challenges" I listed above are basically just "extra things I'll have to implement", which I already know how to do.

I should also point out that some "features" of a dependent type system are things that we really don't want. For example, with our dependent type system we must construct type equality proofs to cast values between types with equivalent size parameters; these are proofs that Cryptol's type checker (in coordination with z3) has already done. Currently we cheat by using the totally unsound unsafeCoerce for every equality proof obligation. A possible fix would be for Cryptol to give explicit proof objects from z3 to saw-core, and to reconstruct the proofs in our type system. This would make sense if we had a proof kernel that we trusted more than we trust z3, but this is not the case.

In any dependently typed proof system, there is a balance between encoding properties in typing judgments vs proving separate theorems. I am basically proposing that we do size checking with separate proofs instead of with typing. We will already need to do separate proofs for array-bounds checking and other safety properties, so this just makes things more consistent. At the same time, getting rid of dependent types will make the semantics of saw-core vastly simpler and let us avoid some blatant unsoundnesses in the type system.

[brianhuffman]

We're probably not going to go this route; vector types with a size index are fairly well established by now.