Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generalized algebraic data types (indexed inductive families) #11

Open
ice1000 opened this issue Mar 16, 2019 · 22 comments
Open

Generalized algebraic data types (indexed inductive families) #11

ice1000 opened this issue Mar 16, 2019 · 22 comments
Labels
gadts Generalized algebraic data types

Comments

@ice1000
Copy link
Member

ice1000 commented Mar 16, 2019

No description provided.

@ice1000 ice1000 added the gadts Generalized algebraic data types label Mar 16, 2019
@xieyuheng
Copy link

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

@xieyuheng
Copy link

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

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

@ice1000
Copy link
Member Author

ice1000 commented Sep 13, 2019

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

@xieyuheng
Copy link

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

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

@xieyuheng
Copy link

xieyuheng commented Sep 13, 2019

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
Copy link

Thanks for the info.

@ice1000
Copy link
Member Author

ice1000 commented Sep 13, 2019

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

I was talking about GKminitt.pdf

@xieyuheng
Copy link

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

@xieyuheng
Copy link

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

@ice1000
Copy link
Member Author

ice1000 commented Sep 13, 2019

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

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

@xieyuheng
Copy link

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

@xieyuheng
Copy link

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

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
Copy link
Member Author

ice1000 commented Sep 13, 2019

I talk too much :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
gadts Generalized algebraic data types
Projects
None yet
Development

No branches or pull requests

2 participants