Tesla Zhang‮

You can actually implement*some* 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...

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

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...

I was talking about GKminitt.pdf

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...

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. Note: `NGen` is only used in the context. They readback lambdas to...

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"...

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...