Abstracting/annotating the result of a recursive call

[mikeshulman]

I'm not sure exactly what's going on here:

rule True type
rule False type
rule A type
rule a : A
rule refl (x : A) : x ≡ x : A

let rec foo s T =
  match T with
  | True  -> let x = fresh x : A in
             abstract x (foo s False)
  | False -> refl s
  end ;;

I get Type error: cannot determine the type of this expression, please annotate it on the abstract line. Comparing this to other variants that do work, I suspect that perhaps since foo is
in the process of being defined, Andromeda can't infer its type sufficiently to be able to do the abstraction. (It works fine if the call is to a previously defined function rather than a recursive call, and also without the abstract.) So okay, sure, and if the function is computing a term rather than an equality I can figure out how to annotate the return value to make it work:

let rec foo s T =
  match T with
  | True  -> let x = fresh x : A in
             abstract x (foo s False : A)
  | False -> s
  end ;;

But I can't figure out how to annotate something as an equality. My first guess was

abstract x (foo s False : s ≡ s : A)

but that gives Parsing error: unexpected ). I tried leaving off the : A and/or adding all the parentheses I could think of, but nothing seems to work. Is there a way to annotate something as an equality?

[haselwarter]

Thanks for reporting this. Your suspicion is correct, the problem is that the AML type checker doesn't know what ML type to assign to foo. The correct solution is judgement → judgement → judgement, so you can circumvent the issue by using the following annotation on the definition of foo:

let rec foo s T
    :> judgement → judgement → judgement
  =
  match T with
  | True  -> let x = fresh x : A in
             abstract x (foo s False)
  | False -> refl s
  end ;;

A different solution is to locally annotate the expression (the computation) that is reported as problematic, namely the recursive call:

let rec foo s T =
  match T with
  | True  -> let x = fresh x : A in
             abstract x (foo s False :> judgement)
  | False -> refl s
  end ;;

Finally, to answer your question of how to annotate an expression as an equality judgement. In Andromeda the verification of derivability of a judgement is bi-directional, to save the user some annotations. Only derivable judgements can be constructed. However, sometimes the user wants to input something like a judgement to steer the construction in a certain direction. In your case, you want to write down s ≡ s : A, but you haven't actually derived this judgement yet (the recursive call should do it for you), and therefore you can't just write s ≡ s : A as a judgement.

But there is a different AML type, namely boundary, that represents "judgements with a hole". The case of a term judgement is most familiar. If you have a type A and you want to assert that a certain computation c (that may contain AML function calls etc) produces a term of type A. To specify the boundary of the judgement that you want c to produce, define
let b = ?? : A
i.e. b is looks like a term judgement with a hole in the "head" position. Now we can guide Andromeda in the evaluation of c with an ascription
c :? b
Analogously, the other judgement forms have corresponding boundaries with ?? in the "head" position. This is necessary to disambiguate them from proper judgements. Correspondingly, to enforce that a computation c' is evaluated to a type judgement, you would write

c'  :?  ( ?? type )

Equations are a bit more peculiar because they don't have a head as such. The syntax we use is similar to the way we name equations in rules. In particular, for the equation you wrote, the syntax is

let b =  ( s ≡ s : A as ?? )

You can then use b to prescribe the boundary of the recursive call:

let rec foo s T =
  match T with
  | True  -> let x = fresh x : A in
             let b = ( s ≡ s : A as ?? ) in
             abstract x (foo s False :? b)
  | False -> refl s
  end ;;

A computation that was ascribed a boundary must be of type judgement, so this too appeases the AML type checker and tells it that foo will produce a judgement.

Epilogue:
One might hope that abstract would be smart enough to figure out that its second argument has to be a judgement and that this information would propagate to foo. However, this is not the case. abstract can also be used to abstract an atom from a boundary, and thus exhibits a very limited form of polymorphism. This is not useful because we need to specify the type of its second argument in all cases. We sometimes get lucky and some other constraint forces that choice, but a choice always has to be made, it cannot be left "polymorphic in judgement + boundary". Something has to be done here, a language keyword that operates on exactly two types is not a great solution.

[mikeshulman]

Wow, thank you for that very extensive answer (i.e. for essentially writing some documentation of code-in-progress just for me (-:O ). I thought that I also tried annotating things as judgement but I guess I didn't get the right combination of that syntax with the different ascription syntax :>.

One question: when I ascribe something to a type like c : A, as in the version that worked in my original question, does that mean the same thing as c :? (?? : A)?

[mikeshulman]

Ah, I see what i didn't figure out. The error message highlighted the entire expression abstract x (foo s False), so when it said "cannot determine the type of this expression, please annotate it" I assumed that the entire expression was being referred to by "this" and "it", so I only tried annotations like abstract x (foo s False) :> judgement and not the correct abstract x (foo s False :> judgement).

[haselwarter]

Yeah the annotation on recursive functions is a bit unfortunate right now, we'll fix that.

The error being reported on the abstract x c rather than on the c seems legit to me, but annotating as abstract x c :> judgement should also solve the issue. I'll look into this.

Indeed, c : A is exactly the same thing as c :? (?? : A) ! If we had macros / notations, we could even define it that way, but currently it's a special syntax for a (supposedly) common use case.

[mikeshulman]

It's too bad there can't be a parallel syntax for equalities, especially since the syntax for defining rules is parallel:

rule a : A
rule e : a == b : A
(c : A)
(c : a == b : A)  (* doesn't work *)

[mikeshulman]

Is there a way for an AML function to explicitly access the boundary that's been given to it, if any?