Implement self parameters

[timsueberkrueb]

• Lay groundwork
• Implement substitution of constructor/codef label for self
• Implement local pattern matches with motives
• Implement local definitions
• Implement local copattern matches with self support

[eternaleye]

Assuming I'm understanding correctly, the absence of this functionality's later steps are why this works:

data Eq (a: Type, x: a, y: a) {
    Refl(a: Type, x: a) : Eq(a, x, x)
}

codata Monoid_1 (m: Type) {
    Monoid_1(m).id_1(m: Type): m,
    Monoid_1(m).op_1(m: Type, a b: m): m,
    (self: Monoid_1(m)).id_is_unitl_1(m: Type, a: m): Eq(m,
        self.op_1(m, self.id_1(m), a), a
    ),
    (self: Monoid_1(m)).id_is_unitr_1(m: Type, a: m): Eq(m,
        self.op_1(m, a, self.id_1(m)), a
    ),
    (self: Monoid_1(m)).id_is_assoc_1(m: Type, a b c: m): Eq(m,
        self.op_1(m, self.op_1(m, a, b), c),
        self.op_1(m, a, self.op_1(m, b, c))
    )
}

but this does not?

data Eq (a: Type, x: a, y: a) {
    Refl(a: Type, x: a) : Eq(a, x, x)
}

codata Monoid_0 {
    ob: Type,
    (self: Monoid_0).id_0: self.ob,
    (self: Monoid_0).op_0(a b: self.ob): self.ob,
    (self: Monoid_0).id_is_unitl_0(a: self.ob): Eq(self.ob,
        self.op_0(self.id_0, a), a
    ),
    (self: Monoid_0).id_is_unitr_0(a: self.ob): Eq(self.ob,
        self.op_0(a, self.id_0), a
    ),
    (self: Monoid_0).id_is_assoc_0(a b c: self.ob): Eq(self.ob,
        self.op_0(self.op_0(a, b), c),
        self.op_0(a, self.op_0(b, c))
    )
}

Specifically, id_0 works, but op_0 does not.

EDIT: It can, of course, be done with Fun, but the result is rather less elegant:

codata Monoid_0 {
    ob: Type,
    (self: Monoid_0).id_0: self.ob,
    (self: Monoid_0).op_0: self.ob -> self.ob -> self.ob,
    (self: Monoid_0).id_is_unitl_0: Π(self.ob, \a. Eq(self.ob,
        self.op_0.ap(self.ob, self.ob -> self.ob, self.id_0).ap(self.ob, self.ob, a), a
    )),
    (self: Monoid_0).id_is_unitr_0: Π(self.ob, \a. Eq(self.ob,
        self.op_0.ap(self.ob, self.ob -> self.ob, a).ap(self.ob, self.ob, self.id_0), a
    )),
    (self: Monoid_0).id_is_assoc_0: Π(self.ob, \a. Π(self.ob, \b. Π(self.ob, \c. Eq(self.ob,
        self.op_0.ap(                  self.ob, self.ob -> self.ob,
            self.op_0.ap(              self.ob, self.ob -> self.ob, 
                a                 ).ap(self.ob, self.ob, 
                b
            )                     ).ap(self.ob, self.ob,
            c
        ),
        self.op_0.ap(                  self.ob, self.ob -> self.ob,
            a                     ).ap(self.ob, self.ob,
            self.op_0.ap(              self.ob, self.ob -> self.ob,
                b                 ).ap(self.ob, self.ob,
                c
            )
        )
    ))))
}

[BinderDavid]

What you are running into is a restriction in our implementation of the binding order.
In a declaration of a destructor of the form (self : T(es)).d(Gamma) : tau all the variables bound in Gamma can be used for writing the arguments es of the type constructor T, and both the variables from Gamma together with the binding self : T(es) can be used in tau. But it is currently not possible to use the binding self : T(es) in Gamma, because that is potentially circular.

If we want to lift this restriction then we probably need two arguments list for d. This might look like this:

(self : T(es)) .d(Gamma1; Gamma2) : tau

The es would be typed in context Gamma1, Gamma2 would be checked in the context Gamma1, self: T(es) and tau would be checked in context Gamma1, self: T(es), Gamma2.

And your example would be a very good motivation to implement such a feature in the language 👍

[eternaleye]

I do wonder if this could also be used to improve the ergonomic weaknesses that arise from the condition that Ξ₁ and Ξ₂ are entirely separately declared, by doing the split slightly differently for codata, data, def, and codef, and using three contexts together:
- Γ₁ (the "declaration telescope")
- Γ₂ (the "self telescope")
- Γ₃ (the "observation telescope")

We would then have:

codata C(...Γ₁) {
    -- Typed in Γ₁, Γ₂
    (self: C(...))
    .op(
        -- Typed in Γ₁
        ...Γ₂;
        -- Typed in Γ₁, Γ₂, self: C(...)
        ...Γ₃
    -- Typed in Γ₁, Γ₂, self: C(...), Γ₃
    ): ...
}
                   
codef Imp(
    ...Γ₁;
    -- Typed in Γ₁
    ...Γ₂
-- Typed in Γ₁, Γ₂
): C(...) {
    op(
        -- Typed in Γ₁, Γ₂
        ...Γ₃
    -- Typed in Γ₁, Γ₂, Γ₃
    ) => ...
}

data D(...Γ₁) {
    Con(
        -- Typed in ...Γ₁
        ...Γ₂;
        -- Typed in Γ₁, Γ₂
        ...Γ₃
    -- Typed in Γ₁, Γ₂, (Γ₃?)
    ): D(...)
}

-- Typed in Γ₁, Γ₂
def (self: D(...)).obs(
    ...Γ₁;
    -- Typed in Γ₁; semicolon _retained_ for closure under dualization
    ...Γ₂;
    -- Typed in Γ₁, Γ₂, self: D(...)
    ...Γ₃
-- Typed in Γ₁, Γ₂
): ... {
   -- Typed in Γ₁, Γ₂, self: D(...), Γ₃
   ...
}

In addition, I would expect only Γ₃ to actually need passed to destructors as parameters.

That would enable the following, rather more "typical" monoid definition:

-- Taking the convention that semicolon absence "defaults right", i.e.
-- `((Γ₁;)? Γ₂;)? Γ₃` to abuse regex notation.
codata Monoid_1 (m: Type) {
    Monoid_1(m).id_1: m,
    Monoid_1(m).op_1(a b: m): m,
    (self: Monoid_1(m)).id_is_unitl_1(a: m): Eq(m,
        self.op_1(self.id_1, a), a
    ),
    (self: Monoid_1(m)).id_is_unitr_1(a: m): Eq(m,
        self.op_1(a, self.id_1), a
    ),
    (self: Monoid_1(m)).id_is_assoc_1(a b c: m): Eq(m,
        self.op_1(self.op_1(a, b), c),
        self.op_1(a, self.op_1(b, c))
    )
}

With this, the difference between Monoid_0 and Monoid_1 becomes much closer to the usual experience of moving a record field into the telescope.

Additionally, because the self is now possibly only dependent on Γ₁, it would also broaden the cases in which we may omit the explicit invocant in a codata declaration:

codata Monoid_1 (m: Type) {
    id_1: m,
    op_1(a b: m): m,
    (self: Monoid_1(m)).id_is_unitl_1(a: m): Eq(m,
        self.op_1(self.id_1, a), a
    ),
    (self: Monoid_1(m)).id_is_unitr_1(a: m): Eq(m,
        self.op_1(a, self.id_1), a
    ),
    (self: Monoid_1(m)).id_is_assoc_1(a b c: m): Eq(m,
        self.op_1(self.op_1(a, b), c),
        self.op_1(a, self.op_1(b, c))
    )
}

Thus limiting the need for its use to when stating destructors that rely upon other destructors in their signature, or when self is typed as a subobject of its total space.

It may be possible to reduce this further, to only when self is typed as a subobject of its total space, by allowing uses of destructors on the current codata in contexts typed in self to omit the invocant. However, this would likely present challenges in dualization.

Another possibility is to place Γ₂ before self, and use the semicolon similarly. For example, in a codata declaration:

codata C(...Γ₁) {
    (
        -- Typed in Γ₁
        ...Γ₂;
        -- Typed in Γ₁, Γ₂
        self: C(...)
    ).op(
        -- Typed in Γ₁, Γ₂, self: C(...)
        ...Γ₃
    -- Typed in Γ₁, Γ₂, self: C(...), Γ₃
    ): ...
}

This would have the benefit of generally retaining reading order, which may help user comprehension.