Jean-Alexandre Barszcz pushed new branch ja-barszcz at Stefan / Typer

Here are some comments on your code.

+type Decidable (prop : Type)

• | mkDecidable (Unit -> (Decided prop));

In a pure and strongly normalizing language the difference between `Unit -> Foo` and `Foo` is only when the result is computed. Since Typer is trying to be call-by-value, `Unit -> Foo` basically simulates call-by-name. So unless the result is not used, `Unit -> Foo` just adds overhead but doesn't solve any underlying problem.

+if_with_then_else_ :

• (prop : Type) -> (Decidable prop) ->
• (prop ≡> ?res) -> ((Not prop) ≡> ?res) -> ?res;

Right. Here `prop` should be explicit indeed, but we'd also want it to be erasable (which Typer currently doesn't offer). We can get the "explicit and erasable" in this specific case by using a macro instead of a function.

The second argument (of type `(Decidable prop)`) should be implicit, OTOH.

+if_with_then_else_ prop dec t e =

• case decide dec
• | yes => t
• | no => e;

Typer should not currently be able to type this correctly, because it does not have the needed infrastructure to find which proofs to pass as implicit arguments to `t` and `e`.

IOW we do want Typer to accept such code, but if it does accept it now it's a lucky bug. It should instead force us to write something like:

case decide dec | yes (_ := p) => t (_ := p) | no (_ := p) => e (_ := p);

+Eq_trans :

• (x : ?t) => (y : ?t) =>
• (a : ?t) -> (ax : Eq a x) ≡> (ay : Eq a y) ≡> Eq x y;

+Eq_trans =

• % Why are ℓ and t not added automatically when we use ?t
• lambda (ℓ : ##TypeLevel) (t : ##Type_ ℓ) ≡> % FIXME remove those
• lambda (x : t) (y : t) =>
• lambda (a : t) ->

Supposedly they are (and so as `x` and `y`). IOW the following should work:

Eq_trans a = ...

as well as [ I think; less sure, tho ]:

Eq_trans = lambda x y => ...

I think the problem you saw is that the annotation `t` is elaborated before the insertion of implicit `lambda (ℓ : ##TypeLevel) (t : ##Type_ ℓ)` takes place, so it doesn't (yet) know about the variable `t`.

+discriminate =

[...]

•     	       		  (cons (Sexp_symbol "believe_me")
  

[...]

+test : (Not (Eq true false)); +test = discriminate true false;

We can prove `Not (Eq true false)` without any hack like "believe_me":

test : Not (Eq true false); test p = Eq_cast (f := lambda x -> if x then True else False) (p := p) ();

+decideBoolEq : (a : Bool) => (b : Bool) => Unit -> Decided (Eq a b); +decideBoolEq =

• lambda (a : Bool) (b : Bool) =>
• lambda (u : Unit) ->
• case (a, b)
• | (false, false) => yes (p := Eq_trans false)
• | (false, true) => no (contra := lambda (p : Eq a b) ->

•   absurd (Eq_trans (ax := Eq_trans a) b) (discriminate false true))
  

• | (true, false) => no (contra := lambda (p : Eq a b) ->

•   absurd (Eq_trans (ax := Eq_trans a) b) (discriminate true false))
  

• | (true, true) => yes (p := Eq_trans true);

I think for this to type check correctly, we need support for dependent elimination, which is currently not implemented (yes, this means that currently Typer is severely restricted when it comes to writing proofs).

Of course, for boolean equality (as well as several other such operations), we'll want to provide built-ins instead anyway.

+++ b/shell.nix

Nice.

• add_builtin_cst "believe_me" DB.believe_me

I hope we'll never need such a thing, because I don't know how to implement it.

+let type_believe_me =

• let lv = (dloc, Some "l") in
• let tv = (dloc, Some "t") in
• mkArrow (Aerasable, lv,

•       type_level, dloc,
  

•       mkArrow (Aerasable, tv,
  

•                mkSort (dloc, Stype (mkVar (lv, 0))), dloc,
  

•                mkVar (tv, 0)))
  

+let believe_me = mkBuiltin ((dloc, "believe_me"), type_believe_me, None)

It lacks a corresponding evaluation rule.

•               -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1')
  

•                 then lexp_error (lexp_location lt1') lt1'
  

•                                 ("Type mismatch!  Context expected `"
  

•                                  ^ lexp_string lt1 ^ "`"));
  

•               ->   (match Unif.unify lt1' lt1 (ectx_to_lctx ctx) with
  

•                     | ((ck, _ctx, t1, t2)::_)
  

•                       -> lexp_error (lexp_location lt1') lt1'
  

•                            ("Type mismatch("
  

•                             ^ (match ck with | Unif.CKimpossible -> "impossible"
  

•                                              | Unif.CKresidual -> "residue")
  

•                             ^ ")!  Context expected:\n    "
  

•                             ^ lexp_string lt1 ^ "\nbut parameter has type:\n    "
  

•                             ^ lexp_string lt1' ^ "\ncan't unify:\n    "
  

•                             ^ lexp_string t1
  

•                             ^ "\nwith:\n    "
  

•                             ^ lexp_string t2);
  

•                          assert (not (OL.conv_p (ectx_to_lctx ctx) lt1' lt1))
  

•                     | [] -> ()));
  

Hmm... we should move this unify+signal error to a common place (or use `check_inferred`, or something) to avoid copy&pasting.

I think using unification instead of `conv_p` here is good, but I'm curious how you bumped into this.

and sexp_dispatch loc depth args =

• let eval a b = eval a b depth in
• let sxp, nd, ctx_nd,

•        sym, ctx_sym,
  

•        str, ctx_str,
  

•         it, ctx_it,
  

•        flt, ctx_flt,
  

•        blk, ctx_blk = match args with
  

• let trace_dum = (Var ((loc, None), -1)) in
• let eval_call a b = eval_call loc trace_dum depth a b in
• let sxp, nd, sym, str, it, flt, blk = match args with (* FIXME: Don't match against `Closure` to later use `eval`, instead
  • pass the value to "funcall". *)

[...]

You forgot to remove this FIXME which your patch fixes. This looks very good, thanks. Feel free to push this part directly to `trunk`.

• | Cons (it, name) -> Cons (apply_inv_subst it s, name)

• | Cons (it, name) -> mkCons (apply_inv_subst it s, name)

Good catch, thanks!

• | Cons (it, name) -> Cons (mkSusp it s, name)

• | Cons (it, name) -> mkCons (mkSusp it s, name)

Idem

Please push those two to `trunk` as well.

• | (Arrow _, Imm _) -> [(CKimpossible, ctx, arrow, lxp)]
• | (Arrow _, Var _) -> ([(CKresidual, ctx, arrow, lxp)])
• | (Arrow _, _) -> unify' lxp arrow ctx vs

•   else [(CKimpossible, ctx, arrow, lxp)]
  

This is justified by the order in which we perform the tests in the main `unify` function. We should clarify this with a general comment in that main function describing this ordering and how it's used.

Stefan