Provide a way to define top-level definitions

[Ailrun]

Without that it is highly cumbersome to give more interesting examples.

[Ailrun]

A related additional feature: module system

[HuStmpHrrr]

Let binding in this rule is effectively just top level definition. We can do something like this for now.

[Ailrun]

@HuStmpHrrr One issue with that is T' cannot depend on x. For example, if we define a Pair type (by church encoding), we cannot use that type as the result type.

[HuStmpHrrr]

we should replace x in T' with t.

[Ailrun]

We cannot still mention Pair (or so) at the final result type. Otherwise, presupposition ({{ Gamma |- T' : Type@i }}) for {{ Gamma |- let ... in ... : T' }} cannot be true.

[HuStmpHrrr]

we should replace x in T' with t.

T' can refer to Pair, it's just that it will be expanded. T' sees x as an extra variable.

[Ailrun]

I mean T' as the result type. Or, with that substitution, T'[t/x]. Our current impl expects the type that the expression checks against, and that type cannot refer to Pair.

[Ailrun]

So, for example, with a "proper" top-level,

def Pair : forall (A : Type@0) (B : Type@0) -> Type@1 =
  fun (A : Type@0) (B : Type@0) -> forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C

def pair : forall (A : Type@0) (B : Type@0) (a : A) (b : B) -> Pair A B =
  fun (A : Type@0) (B : Type@0) (a : A) (b : B) (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> pair a b

pair Nat (forall (x : Nat) -> Nat) 3 (fun (x : Nat) -> succ (succ x)) : Pair Nat (forall (x : Nat) -> Nat)

will be possible, but with that "let" approach,

let Pair = fun (A : Type@0) (B : Type@0) -> forall (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> C in
let pair = fun (A : Type@0) (B : Type@0) (a : A) (b : B) (C : Type@0) (pair : forall (a : A) (b : B) -> C) -> pair a b in
pair Nat (forall (x : Nat) -> Nat) 3 (fun (x : Nat) -> succ (succ x))
  : Pair Nat (forall (x : Nat) -> Nat)

will not be possible (because of the reference to Pair in the type of the entire expression)

[HuStmpHrrr]

that's because the last column lives outside of the lets. problems like this can always be worked around by fitting the last expression to another layer of let:

...
let foo : Pair Nat (forall (x : Nat) -> Nat) := pair Nat (forall (x : Nat) -> Nat) 3 (fun (x : Nat) -> succ (succ x)) in
0 : Nat

It's not perfect, but passing the typechecker implies foo is also well-typed.

[HuStmpHrrr]

I am not saying it's perfect, but I would expect a local let binding is implemented in this very same way. It does no harm to use this solution for now.

[Ailrun]

I agree on that this solution is easy to implement, and a good temporary solution. What I wanted to say is that there is the abovementioned issue I want to note.

[HuStmpHrrr]

yeah let's do this and figure out a mechanizable solution for genuine top-level definitions at a later time, which can wait. I think even this solution might induce some downstream optimizations that would complicate the proof.

[HuStmpHrrr]

I think what I have above won't work. We do need to change the context structure to allow binding a variable to a value. Then the question goes to how the substitution calculus should work. c.f. Coq's let rule https://coq.inria.fr/doc/V8.18.0/refman/language/cic.html#id6 and the Delta-local rule: https://coq.inria.fr/doc/V8.18.0/refman/language/core/conversion.html#delta-reduction-sect

[Ailrun]

What would be the problem?

[HuStmpHrrr]

T' alone might not be well-typed without knowing t, that means we only know T'[t/x] is well-typed but not T', so we cannot apply equivalence of substitutions to it.

[Ailrun]

What about the independent version? Although that's identical to the "syntactic sugar" approach Antoine is building (based on lambda and application).

[HuStmpHrrr]

T' Independent of x? Still the same problem applies for t'. It cannot be well-typed in general without knowing t, so substitution calculus can't apply.

[Ailrun]

Ah true. Yeah we need a proper top-level definition.