redprl / cooltt Goto Github PK
View Code? Open in Web Editor NEW😎TT
Home Page: http://www.redprl.org/
License: Apache License 2.0
😎TT
Home Page: http://www.redprl.org/
License: Apache License 2.0
This will be a con
.
right now, given the input
def formation : {
(A : dim -> univ) (a : A 0) (b : A 1) -> univ
} = {
\A a b => -- normal lambda form
path A a ? -- this is the new form for paths
}
the pretty printer gives the following information for the hole
Emitted hole:
A : (-> [_x : dim] univ)
a : (el (A 0))
b : (el (A 1))
_x : dim
_x₁ : (prf (or (= _x 0) (= _x 1)))
_x₂ : (prf (= _x 1))
|- ? : (el (A _x)) [_x₃ : (= _x 0) => []]
This is correct but somewhat misleading. The constraint [_x₃ : (= _x 0) => []]
is satisfied vacuously: _x = 1
is in the context and equality of dimensions is decidable, we know that _x
cannot ever be zero. Therefore any el (A _x)
will do because they all satisfy that constraint definitionally, which is to say any el (A 1)
will do, including the one in the context b
.
A better output might look like
Emitted hole:
A : (-> [_x : dim] univ)
a : (el (A 0))
b : (el (A 1))
_x : dim
_x₁ : (prf (or (= _x 0) (= _x 1)))
_x₂ : (prf (= _x 1))
|- ? : (el (A _x))
An even better output might even look like
Emitted hole:
A : (-> [_x : dim] univ)
a : (el (A 0))
b : (el (A 1))
_x : dim
_x₁ : (prf (or (= _x 0) (= _x 1)))
_x₂ : (prf (= _x 1))
|- ? : (el (A 1))
but that's a different issue.
Some initial cost of apparent code duplication (which I strongly believe can still be factored away) is a small price to pay for simplifying the code conceptually and making it more uniform.
When something like phi \/ psi
is already in the context, conversion doesn't really do the right thing --- it tries converting uniformly under the assumption, but it really needs to split on it ASAP. (It does do the right thing when adding new assumptions to the context; this is just about existing assumptions.)
This can be fixed as follows: before doing equality checks in the elaborator, first go through the context and bundle up all the assumed cofibrations and then do under_cofs (meet phis) (equate ...)
.
I'd like to think of hcom/coe as constants in the logical framework (regardless of whether we end up implementing them this way); so, in particular, it would be appropriate to think of the line and tube things as lambda-bound functions.
This would imply #35.
[phi -> M | ... | psi -> N]
This would correspond nicely to the use of n-ary joins in the cofibrations. With n-ary splits, we would have a single elimination form for joins, removing the need for nesting as well as a separate abort
.
I had a nice idea for a cool use of the cofibration machinery. If the user can declare a fresh cofibration, then this is basically enough to define a strict "open modality". Then we could potentially use cooltt to mechanize some neat artin gluing arguments.
this can be a real rabbit hole but i think these are increasing order of preference for me:
_x₁ : (prf (or (= _x 0) (= _x 1)))
_x₁ : prf (_x = 0) ∨ (_x = 1)
_x₁ : prf (_x = 0 ∨ _x = 1)
Blocked by #24
A case that I didn't consider is when we go under the binder of a pi-in-prf (x : [phi]) -> A
; we need to special case this to add [phi]
to the environment.
The simplest example of coercions will be for universe levels. Later on, I wish to experiment with weak substitutions, ultimately deleting the type equality judgment entirely (as an experiment).
I would like to build into the elaboration and evaluation environments some kind of mask, which I will call a "veil", to control unfolding of top-level constants during evaluation.
Ideally, a great deal of evaluation can be done with the discrete veil (unfolding nothing); only evaluation that is meant to be shunted to a pattern match should be done with the chaotic veil (unfolding everything).
Things like all that monad crap, etc.
continue to work through the things in comments in path-nat
def simple : {
(A : univ) (a : A) -> A
} = {
\A a =>
let b : A = a in
b
}
normalize simple
raises Internal error (Failed to normalize): do_sub_out
.
I failed to track down the reason. (The same thing happens on the pathcoe or fhcom branches btw.)
Blocked by #23
The idea is that this would be an elaborator from raw core-language terms, calling the primitive tactics from the refiner.
The result would be that the real typechecking code is always shared, and trusted in the refiner.
OK, my proposal for getting started is as follows:
The ElabEnv
should have a "current span" field --- the invariant is that as you get deeper into an elaboration problem the span narrows. It is the responsibility of the elaborator to set this span correctly. This information can then be used when emitting messages or errors.
I guess we should annotate the concrete syntax in such a way that the elaborator has this information. One way is to add dummy nodes in the concrete syntax that annotate with source information, and then the elaborator executes these by locally updating the ElabEnv
.
The global environment should be a state, whereas the local environment should be "reader".
The current design is that the main type theory of cooltt is a (cubical) logical framework, with no notion of Kan operation or even universe level, etc. Then, "cubical type theory" will be implemented (primitively) as a universe of Kan types in the CuLF, where everything decodes to LF types. The original ideas was that (for instance) the extension type code would decode to a complex LF type involving pi
and sub
.
Because this decoding is necessarily lossy at the level of type-codes, I think it may be advantageous to have it not hold up to definitional equality, but instead be mediated by a real El(A)
connective with intro and elim (and beta and eta) rules that enact one step of standard El
decomposition. In other words, it would be a weak universe à la Tarski rather than a strict one. The motivation is to improve the usability of the proof assistant --- the elaborator will take care of applying those El/intro,El/elim
rules as needed, and we would gain the advantage of not losing that information immediately. This can be used to, for instance, support having fewer annotations in the source language, and make interactive development easier.
While the motivation for this idea is essentially syntactic and pertains to human usability, it also has mathematical advantages. Weak universes `a la Tarski are much more natural in the mathematics than strict ones, so it seems like this would be a net benefit on all fronts.
Blocked by #22
This purpose of this ticket is to make outputted code mode readable.
This can be done in one of two ways: remember the name at the binding site, or remember the name at the variable site. These both have advantages and disadvantages:
If we remember the name at the binding site, then we can ensure a correct mapping in pretty printed output between binders and variables --- that is, printing-shadowing bugs are impossible. But the disadvantage is that printing requires a local environment, and there is no way to print some term without that environment (hence the use of these dump
functions for debugging).
If we remember the name at the variable site, then printing becomes very easy; but we may also somehow introduce confusing shadowing issues in the printed output, depending on various factors.
this code snippet causes a stack over flow:
def foo : path {λ _ => ?} zero zero = {
λ _ => zero
}
A place to discuss.
So, the only potential way I see of getting owned (usability-wise) by having substitutions only up to isomorphism would be in connection with types that don't have eta rules, specifically the eliminators of inductive types.
Here, you could get into all sorts of nasty situations where you have a coercion around the eliminator vs inside it, etc., and it is painful to mediate between them. So, the question should be whether this is something that can be overcome, using some very clever approach, or if it is something fatal to the idea.
Ultimately, I would like to de-emphasize the typechecker; it is frankly not something that should be being called by the elaborator on a regular basis anyway. The invariant of the elaborator is that it produces well-typed terms, and in most cases, it is not necessary to "guard" this with a call. So, the elaborator environment should be the primary thing.
I'd like to open this ticket to track some papercuts in the grammar caused by me not knowing how to write parsers lol.
{A b c} -> D e f
instead of A b c -> D e f
{i==0}\/{i==1}
instead of i==0 \/ i==1
We will need a special form like << ... >>
or something that does the following: it temporarily ignores the required boundary and just elaborates something at the requested type. The result is that it leaves a hole, but lets you interactively develop on the inside.
This is for cases where you have partly written some code but it doesn't have the right boundary yet.
This would roughly be a chk_tac -> bchk_tac
.
Not sure if this is a good idea. Sometimes I'm defining a cube and for whatever reason it's more convenient if I flip it along some diagonal first. I could define a flip : (dim -> dim -> A) -> (dim -> dim -> A)
, but then when I write flip ?
I won't have any boundary information in the hole. So maybe it would be useful to be able to write something like this:
def cool : {
(A : univ)
(p : dim -> dim -> A)
-> sub {dim -> dim -> A} #t {\i j => p j i}
} = {
\A p * j => p j
}
where *
means "skip over binding this variable". It should be possible for a tactic like that to propagate boundary info, right?
@jonsterling @ivoysey Do we have to remember why the environment is inconsistent? Could we drop env.cof
and use this instead?
This proposal is so dumb. Let's ignore it for the moment.
This first step to be able to do this is to write down the refinement rule in math. I want to support the bchk_tac
in a stronger way than redtt did.
This way, a hole can be added without re-binding everything.
This is required for implementing nat-elim
of fhcom
.
I want to see if it is possible to make the nbe equality checker return a list of flex-flex and flex-rigid constraints which would make the equation true. Alternatively, a naive but possibly workable-to-start version would be to raise such a constraint as an exception which carries a continuation, kind of like an algebraic effect.
I believe there is a reasonable way to support moving many of those custom closures into 'con'; this would provide a path forward for treating the arguments to hcom
not as primitive binders but as LF terms, and then we would additionally get rid of the use of n-ary binders and n-ary closures, greatly simplifying things.
I'm going to think about this and chart a path forward, but I intend to avoid stepping on #33. There will be some churn, but I will find an appropriate time to carry it out that doesn't disturb ongoing work.
(Update: I just did this inside of #33; none of the raise Todo
is affected, so I consider the "stepping on" avoided.)
let* piuniv =
lift_cmp @@
quasiquote_tp @@
QQ.foreign_tp univ @@ fun univ ->
QQ.term @@
TB.pi TB.tp_dim @@ fun i ->
univ
appears once in Nbe and twice in Refiner;
let* bdry_tp =
lift_cmp @@
quasiquote_tp @@
QQ.foreign_tp univ @@ fun univ ->
QQ.foreign fam @@ fun fam ->
QQ.term @@
TB.pi TB.tp_dim @@ fun i ->
TB.pi (TB.tp_prf (TB.boundary i)) @@ fun prf ->
TB.el @@ TB.ap fam [i]
appears more or less verbatim in Nbe and the Refiner. It's not clear that this is enough code duplication for the overhead of making a library of combinators for building commonly-built terms (possibly as an extension to TermBuilder
) worthwhile or just an obfuscation.
Given phi !- A type
, a type phi => A
whose elements are sections.
To implement a number of things properly, it will be useful and/or necessary to have a flat
modality; it is OK if it is restricted to occur as an argument to a pi type, which often simplifies matters --- these kind of types are called "virtual" in cooltt, and include dim,cof
as well.
See, for example, what @favonia did in redtt.
Following #44, let's accumulate more items here. Don't close this issue immediately if you fix the first problem. 😄
k=0 ∨ {∂ i}
instead of k=0 ∨ ∂ i
(done by #70 and #63)i=0 ∨ j=0 ∨ k=0
(done by #73)[ a => b ]
means):
(#94 and then partially reverted by #105)fst x y
should be parsed as fst x y
. So do snd
, vproj
, and cap
.A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.