Overhaul struct

[mio-19]

This means that we will support arend-style anonymous-extensions and extends as well as this expression.

Structs have arguments no more and we will use partially instantiation to express thing that are currently expressed using arguments, which means that following 2 definitions are equivalent.

open struct Pair (A : Type) (B : Type) : Type
  | fst : A
  | snd : B
  | we-are-together : Sig A ** B => (fst, snd)

open struct Pair : Type
  | A : Type
  | B : Type
  | fst : A
  | snd : B
  | we-are-together : Sig A ** B => (fst, snd)

However, we might want to remove fields instead of telescope of the StructDef class in the current implementation of aya for the reason that telescope is defined in a superclass of StructDef called Def.

For the this expression, we will support the keyword this and this@context for nested struct expressions.

[imkiva]

Does the code in classable branch mean we only accept the second definition? I see there's no telescopic thing in that StructDecl

[mio-19]

@imkiva The first definition is accepted as a syntactic sugar

[imkiva]

@imkiva The first definition is accepted as a syntactic sugar

I don't think we need an extra ClassDecl in this case, we can delay the desugar of telescope until we are tycking them and produce a tele-free StructDef.

[imkiva]

@imkiva The first definition is accepted as a syntactic sugar

I don't think we need an extra ClassDecl in this case, we can delay the desugar of telescope until we are tycking them and produce a tele-free StructDef.

So we can get rid of these annoying and complicated inheritance relationships between these *Decls

[mio-19]

@imkiva We can reverted to previous inheritances

[imkiva]

@imkiva We can reverted to previous inheritances

I tried some refactorings but it became worse because we have made lots of assumptions of concrete decls (like the Signatured, the result and the ctx). I think we just need some simplification based on your work (no need to revert)

[imkiva]

I tried some refactorings but it became worse because we have made lots of assumptions of concrete decls (like the Signatured, the result and the ctx). I think we just need some simplification based on your work (no need to revert)

see #428

[mio-19]

Maybe we should consider more fully on taking this change. This overhaul brings a lot more engineering difficulties. Kiwa mentioned that the root of its complexity is that tele is made to be field, that there are not many examples painful to write without this feature, and that it brings confusion on some examples.

def c1 => new Child { | dad => 1 | son => 2 }
def c2 => new Child 2 { | dad => 1 }

c2 is legal but obviously we don't want to write code in the c2 way.

Kiwa also mentioned that maybe we want to implement 2 features, typeclass without inheritance and coercion to typeclass, before struct inheritance.

Previous aya discussion on inheritance: https://github.com/aya-prover/aya-dev/issues/42 https://github.com/aya-prover/aya-dev/issues/43

[ice1000]

I think c2 should not be legal. The args to a class should be in order, because otherwise there will be many ambiguities. Does that make things easier?

[mio-19]

I think c2 should not be legal. The args to a class should be in order, because otherwise there will be many ambiguities. Does that make things easier?

I forgot to add struct definitions. The order is right in the example.

Disallowing unordered apply might make things slightly easier, but it is not the main issue.

[ice1000]

I think c2 should not be legal. The args to a class should be in order, because otherwise there will be many ambiguities. Does that make things easier?

I forgot to add struct definitions. The order is right in the example.

Disallowing unordered apply might make things slightly easier, but it is not the main issue.

What's the main issue?

Is it still an issue if we decide to remove struct and keep class only? Struct can be "class without instance resolution" and hence we have less messy implementation.

[mio-19]

@ice1000 The support of any partially application brings implementation difficulties, and might not necessarily be useful, as is mentioned by kiwa

[ice1000]

@ice1000 The support of any partially application brings implementation difficulties, and might not necessarily be useful, as is mentioned by kiwa

I see. I'll think more about this, but I tend to agree with you and kiwa now 💭

[ice1000]

I am now trying to implement this. Writing down some notes:

• How to use classes: https://arxiv.org/pdf/2202.01629.pdf
• Lean4: https://leanprover.github.io/lean4/doc/typeclass.html + https://arxiv.org/abs/2001.04301
• Jesper's idea on Agda instances: https://github.com/agda/agda/issues/6378
• Nomination-based instance resolution with named instances: https://www.cs.cmu.edu/~rwh/papers/mtc/short.pdf (also defines overlapping instances)

[ice1000]

After that we'll start playing with Sets: https://github.com/JetBrains/arend-lib/blob/master/src/Set.ard

[ice1000]

Plan:

• [x] Implement the non-core features of classes, like serialization, parsing, etc. (should be the first huge PR)
• [ ] Deal with typing (mainly substitution) of field projections
• [ ] Instance system