msp-strath / ask Goto Github PK

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.

We now have reached the stage of having a Main.hs file which can be compiled (in the src directory) by

ghc --make Main -o ask

yielding a shell-activated transducer, and the corresponding test file

./ask < ../eg/Proofs.ask

(which contains commutativity of conjunction and also the law of the excluded middle) is successfully mutated into a pile of steaming abstract syntax.

The best way to see if you like it is to check

• grep Junk which will tell you whether any present subproofs have been rejected
• grep Need which will tell you whether any missing subproofs are being demanded

Clearly, this mode of interaction falls short of an accceptable user experience. Some sort of printing is in order.

In #2, I was bothered by the possible consequences for layout of changing prove to proven. One of the options under consideration was to ban the "where-horizontal", as in

prove a & b by AndI where prove a ?
                          prove b ?

Not only because of the prove/proven thing, I am increasingly in favour of this option and am minded to go with it.

The proposed law is this:

Between a layout herald and its end of line, if there are any tokens other than whitespace or comments, the first of them must be {.

So if you want to indent after where you must take a new line, which is what we usually do and teach.

This move also mandates compliance with Hancock's Layout Law:

Ensure that your use of layout yields code invariant under alpha-equivalence.

And that means we might actually offer alpha-conversion as a transducer service. When we scope-check the input, we could note requests for renaming, then use the new name when generating the output.

Moreover, it opens the way to displaying proofs in a proportional font. Indeed, it might not be at all daft to consider multiple rendering options for ask output: what if we generated vaguely sensible html for the passive buffer (as well as stashing the raw text that you get when you click Accept)? We could even attach mouse-event-handlers to various regions (e.g., when you mouse-over a ?, it might illuminate the hypotheses in scope for it).

I'm writing to suggest two ideas, modulo bikeshedding, and a possible interaction between them.

1 the given method

At the moment, you can say

prove p -> p by ImpI

and leave ask to check that the subgoal is given, but there is no successful way to be explicit about it, i.e., if you write

prove p -> p by ImpI where
  given p prove p ?

In fact, we could add the rule prove p by Assumption where prove p ? and then users could make an explicit

prove p -> p by ImpI where
  given p prove p by Assumption

leaving the subgoal to be solved implicitly as before. But that's egregious, because it would lead to

prove p -> p by Assumption where
  prove p -> p ?

in situations where the goal is not given. For this reason, I propose to create a new method, given, which succeeds only if the goal really is given. This would allow the user to choose to document

prove p -> p by ImpI where
  given p prove p given

Note that ask checks which subgoals are discharged by subproofs before either declaring unused subproofs to be surplus or checking whether uncovered subgoals are actually obvious. So, as things stand, given p prove p given would neither be inserted nor removed by ask.

2 the proven proof

At the cost of a keyword (beloved of the Scots legal system), I propose that we allow prove to be replaced by proven when all subgoals have hereditarily been discharged. I moreover propose that ask acknowledge completion of goals and subgoals by making this substitution, amounting to a more explicit acknowledgement of achievement than "no comment". If the user writes proven but ask discovers open subgoals, then proven reverts to prove.

So, if we submit

prove p & q -> q & p by ImpI where
  given p & q prove q & p from q & p where
    given p, q prove q & p by AndI

we obtain

proven p & q -> q & p by ImpI where
  given p & q proven q & p from q & p where
    given p, q proven q & p by AndI

but if we submit

proven p & q -> q & p by ImpI where
  given p & q proven q & p by AndI

we get the corrective reminder

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI
    prove q ?
    prove p ?

and replacing the first ? with from p & q then yields

prove p & q -> q & p by ImpI where
  given p & q prove q & p by AndI
    proven q from p & q
    prove p ?

telling us we've made at least some progress.

3 prove versus proven and the insertion of givens

This is a bit of a subtle idea, and I'm not sure whether I like it. Perhaps, when ask gets this

prove p & q -> q & p by ImpI where
  given p & q prove q & p from p & q where
    given p, q prove q & p by AndI

the response should be

proven p & q -> q & p by ImpI where
  given p & q proven q & p from p & q where
    given p, q proven q & p by AndI
      proven q given
      proven p given

That is, if we start from a prove with no subproofs, ask inserts completed subproofs for the givens (except for the h in from h, which we usually expect to be given). However, if the user then deletes those givens and sends

proven p & q -> q & p by ImpI where
  given p & q proven q & p from p & q where
    given p, q proven q & p by AndI

then the proof is returned unaltered, because the head was a proven, not a prove.

If a prove is submitted with some existing subproofs, then missing proven ... givens are not inserted, as that implies the user has already chosen which subproofs to see. Meanwhile, if the user does not want proven ... givens are not inserted in a prove with no subgoals, they should jolly well write proven instead.

What to do?

1 and 2 are independent of each other. 3 requires both 1 and 2, but is entirely optional. Open to alternative syntactic choices.

There's a bunch of stuff I want to do under the hood, none of which will deliver the slightest extension of positive functionality. Rather, it will put the house in order before we move on.

0 Chuck Out Dead Files

I did a lot of refactoring today, which involved making replacement candidates for old files under new names (e.g., LexAsk → Lexing). I also chopped up the old Ask.Src.ChkRaw to split out "library" code. The old files are now useless. They should go.

1 Monadify

We have a lot of code (in Ask.Src.ChkRaw) which passes stuff like Setup and Context around explicitly. That should be tidied up into a monad, so we can hide the plumbing, and so that it is less disruptive to change how we manage the setup or add extra machinery. Speaking of which...

2 Go Locally Nameless

At the moment, unquantified variables in a top-level goal are treated as Skolem constants and represented as de Bruijn indices. This is sustainable only as long as no local variable binding happens. We should go locally nameless so that we get both weakening and alpha-equivalence for free. That means plumbing a name supply, which is just another bit of environment to hide in the monad.

3 Typechecking

Even if we have, so far, only one type, viz. Prop, we should check that the formulae people write are well typed. Just now, spurious "constructors" generate propositions with no introduction rules. We'd give better feedback about beginner mistakes (e.g. prove AndI ?) and we'd be getting ready for more interesting types. Just now, we don't need any type synthesis. That said, having gone locally nameless, the reference to any given name should cache a pointer to the type of that name.

4 Extract Rules from Prop Declarations

The parser can already get us from tokens to "raw" syntax, in declarations like

prop Prop -> Prop where
  prove a -> b by ImpI where
    given a prove b

but we don't get all the way to actionable values of type Rule, hence the current holding pattern that is Ask.Src.HardwiredRules. If we actually turned the head of prop declarations into proper constructor declarations that feed into the typechecker and the body into rules, we could do that stuff in software. It would be good to allow Marx-hosted ask puzzles to choose the "prelude" to any given task.

The Contradiction rule (TIS AGIN NATURE!) presents an anomaly that we'll need to bikeshed, in that it is a rule which is not extracted from a prop declaration. So how is it to be declared? Perhaps (resisting whole new keywords)

import where
  prove p by Contradiction where
    given Not p prove False

The question is what top-level declaration introduces a block of rules that we insist upon without justification (and do not invert when computing the behaviour of from).

But I digress.

5 Head/Full Normalisation

Internally introduce a notion of "prop synonym". Implement the machinery to head-normalise terms, and then push to full on normalisation. Do pattern matching up to head normalisation and "is it given?" checking up to full normalisation. Without giving the users the opportunity to write definitions, nobody will notice that we have done this.

Epilogue

When we have done these things, nobody will notice the blindest bit of difference, but we shall be cooking with gas.