Data Types and Inductive Programming

[pigworker]

I have added data declarations in the style of classic Haskell. (Perhaps there should be GADTs, but...later.)

data TyCon binding* = VaCon placeholder* | ... | VaCon placeholder*

In a slight liberalisation of the Haskell syntax, a binding may be a variable x but (x :: type) is also acceptable. And (you guessed it) a placeholder may be a type but (x :: type) is also acceptable. The difference is that the bindings scope over all the constructor declarations.

I have not yet implemented a (strict) positivity check: that will prove important in due course. Moreover, it is good to detect which parameters are co-, contra- and equi-variant. (Ask me about functoriality another time.)

I am now planning how programming will look.

Type signatures will be compulsory for all definitions. They also are more liberal, in that

(+) :: Nat -> Nat -> Nat
(+) :: (x :: Nat) -> (y :: Nat) -> Nat
Nat + Nat :: Nat
(x :: Nat) + (y :: Nat) :: Nat

will all be ok and mean the same thing. If there is no definition, ask should insert one, by default as fully applied as in the type signature. If argument names are not supplied, there will doubtless be a ghastly heuristic. The user is free to change names and appliedness. So, for example, the above would yield (respectively)

define (+) ?
define (+) ?
define n + n' ?
define x + y ?

At this point, I propose three methods one may deploy:

The induction Method

You say induction and then a nonempty list of variables inhabiting inductive data types.

(x :: Nat) + (y :: Nat) :: Nat
define x + y by induction x
  given (x :: Wee Nat) + (y :: Nat) :: Nat define x + y ?

and you get given a thing with the same name as the thing you are defining whose type signature follows the original style, but where the types of the induction variables are marked Wee (bikeshed!). Behind the scenes, we have acquired a fresh Skolem constant i ∈ Size and a hypothesis

(+) ∈ &forall n. Sized Nat i (S n) -> Nat -> Nat

where Size is an abstract type, and Sized T i n is a type if Type ∋ T, Size ∋ i and Dug ∋ n. Dug is an internal copy of Nat which counts how far we have dug into a thing. I don't intend Sized, Size and Dug to be exposed to the user: Sized T i (S n) is Wee T and Sized T i Z is Big T. Guess what? The goal is now really

define (x :: Big Nat) + (y :: Nat) ?

We have subtyping: Sized T i m ≤ T. Sized T i m ≤ Sized T i n if n ≤ m. That is, we can forget smallness.

The from Method

We're now ready to use from to invert the construction of a pattern variable of inductive type.

(x :: Nat) + (y :: Nat) :: Nat
define x + y by induction x
  given (x :: Wee Nat) + (y :: Nat) :: Nat define x + y from x
    define Z + y ?
    define S x + y ?

Now, when the from variable (and it must be a variable) has a Sized type, the exposed inductive substructures are one step more Dug. At this point, we're good to finish off.

The = Method

We're done.

(x :: Nat) + (y :: Nat) :: Nat
define x + y by induction x
  given (x :: Wee Nat) + (y :: Nat) :: Nat define x + y from x
    define Z + y = y
    define S x + y = S (x + y)

You may give the output by writing = and a term of the right type. If you accidentally write a variable that is out of scope, ask will respond by inserting a where clause. We could say

(x :: Nat) + (y :: Nat) :: Nat
define x + y by induction x
  given (x :: Wee Nat) + (y :: Nat) :: Nat define x + y from x
    define Z + y = y
    define S x + y = S n

and we'd be asked

(x :: Nat) + (y :: Nat) :: Nat
define x + y by induction x
  given (x :: Wee Nat) + (y :: Nat) :: Nat define x + y from x
    defined Z + y = y
    define S x + y = S n where
      n :: Nat
      define n ?

Anyhow, that's my sketch of what and how.

[pigworker]

At the moment, when I check subproofs, I validate them first, then I check which subgoals they cover. That is, I don't match subgoals to subproofs until after I've validated the subproofs. For subdefinitions I won't get away with that. I'll need some sort of superficial matching to identify which subdefinition addresses which subgoal. Fortunately, constructors show up helpfully, so that should be enough of a clue.

[pigworker]

This is now beginning to work. But induction is now spelled inductively. And there's no sign of sizes.

We also have

test S (S Z) + S (S Z)

yielding

tested S (S Z) + S (S Z) = S (S (S (S Z)))

[pigworker]

We're not out of the woods yet, but I think I'll close this issue and open another in the morning. Some careful rationalisation and refactoring is on the cards.