Open ice1000 opened 5 years ago
I found minitt can not do this, only after I implemented it :: https://github.com/xieyuheng/cicada/blob/8599c2221857eda4483a3619c12579e1f90eeffc/example/minitt/paper.tt#L123 :(
Yes, sized vector is a well-known instance of GADT. This will be implemented in Narc along with dependent pattern matching.
Do you have overlapping pattern (and confluence check) support? I am quite interested.
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.
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.
Only Jesper's paper is found: https://jesper.sikanda.be/files/vectors-are-records-too.pdf
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.
Thanks for the info.
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
.
I was talking about GKminitt.pdf
yes, "A simple type-theoretic language: Mini-TT"
I defined standalone Normal Form type. I did not know about the source code hosted on one author's website.
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.
We have a fork in this organization. You can take a look.
I thought alpha conversion in the paper is handled by renaming all bound variables in readback functions.
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 :)
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.
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.
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.
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.
I talk too much :)
Is this about defining types like
Vec(A: type, n: Nat)
?