Generalized algebraic data types (indexed inductive families)

[ice1000]

[xieyuheng]

Is this about defining types like Vec(A: type, n: Nat) ?

[xieyuheng]

I found minitt can not do this, only after I implemented it :: https://github.com/xieyuheng/cicada/blob/8599c2221857eda4483a3619c12579e1f90eeffc/example/minitt/paper.tt#L123 :(

[ice1000]

Yes, sized vector is a well-known instance of GADT. This will be implemented in Narc along with dependent pattern matching.

[ice1000]

Do you have overlapping pattern (and confluence check) support? I am quite interested.

[xieyuheng]

Yes, sized vector is a well-known instance of GADT. This will be implemented in Narc along with dependent pattern matching.

Looking forward to your implementations.

[ice1000]

You can actually implementsome GADTs using dependent pi/sigma types (which means -- yeah, we can do this in minitt). I remember there's a page on Agda wiki, I'm trying to find it.

[ice1000]

Only Jesper's paper is found: https://jesper.sikanda.be/files/vectors-are-records-too.pdf

[xieyuheng]

Do you have overlapping pattern (and confluence check) support? I am quite interested.

I am not sure about the meaning of overlapping pattern. If confluence check means convertibility check, I have it.

The use of pattern and implementation of checkers are faithful to original minitt paper.

[xieyuheng]

Thanks for the info.

[ice1000]

Note: the source code hosted on one author's website is different from the paper appendix. In the paper appendix there are standalone Normal Form type for Val, Neutral and the telescope type that is returned by the readback function, while in the hosted project the readback function returns Expr.

[ice1000]

I was talking about GKminitt.pdf

[xieyuheng]

yes, "A simple type-theoretic language: Mini-TT"

[xieyuheng]

I defined standalone Normal Form type. I did not know about the source code hosted on one author's website.

[ice1000]

This is a bad title. It's very complicated since it has chosen to do readback+syntactic comparison instead of the straightforward conversion check. Also, both official implementations of minitt do not respect alpha conversion.

[ice1000]

We have a fork in this organization. You can take a look.

[xieyuheng]

I thought alpha conversion in the paper is handled by renaming all bound variables in readback functions.

[xieyuheng]

I also have some ideas about implementing record type and subtype too. I will apply what I learned from minitt to my ideas. maybe forward my progress to you too :)

[ice1000]

I thought alpha conversion in the paper is handled by renaming all bound variables in readback functions.

Note: NGen is only used in the context. They readback lambdas to Branch which contains Expr. Thus the thing you're actually comparing is the surface syntax tree.

[ice1000]

Do you plan to implement contravariance for pi types' parameters? I heard it's different from non dependent type systems, but the person told me this didn't explain the reason.

[ice1000]

The cause of the difference is that you're adding a contravaraint-typed variable to the context during typechecking. You want to keep the "this variable may be of a different type" in ~~mind~~ the typing context to avoid unsoundness.

[ice1000]

Btw, if you can provide a bnf/peg-formatted grammar definition of your language, an SVG icon for it (optional) and the scoping rule (described using natural language), I am willing to add your language support to intellij-dtlc (can be found in JetBrains plugin Marketplace, named "Dependently-Typed Lambda Calculus"). But I cannot guarantee a finishing time.

[ice1000]

I talk too much :)