Comments (5)
One approach is to remove the hole regardless, and then make downstream insert holes if they break. Consider
{? 1 ?} True
which would stay as it is: we remove the hole when considering synthesising a type for it, but then when considering the App
node, we re-add the hole as we need an arrow type. Now consider {? ? :: Nat -> Nat ?} True
which would change to (? :: Nat -> Nat) {? True ?}
as we remove the hole but then we require that Nat \ni True
, which is false so we add a hole there. This "jumping holes" seems like bad UX to me.
from primer.
What's the status of this issue wrt the new smart holes implementation?
from primer.
What's the status of this issue wrt the new smart holes implementation?
Essentially unchanged. We attempt to remove holes, but the implementation is somewhat ad-hoc and should be improved to both be more general and more intuitive.
Some particular issues we currently have
- the "change this empty hole into a non-empty hole"
? ~> {? ? ?}
action is broken, since we automatically elide this non-empty hole again - some "obviously pointless" hole/annotations are not elided, e.g.
foo : ∀a:*.? ; foo = {? ? : ∀a:*.? ?}
where we have "the same annotation" twice
However, I still don't know how to remove all(/most) "pointless" things whilst not making it awkward to intentionally create something like foo : Bool ; foo = {? ? : Int ?}
, which can be useful when trying to work out how to complete your program. To create this one probably wants to go via foo : Bool ; foo = {? ? : ? ?}
, which is a "pointless" hole/annotation.
Perhaps we need to rethink the decision to operate only on the AST, and instead track whether holes were automatically created?
from primer.
It would be great if we could reach a point where the manual FinishHole
action is never actually necessary. I figured this should be possible, since a naive implementation would just be to perform a post-TC pass of auto-applying the action wherever it's available.
However, while tring to work out exactly when the action is offered in the first place (the Succ
example in OP is invalid now with saturated-constructors), I've just noticed that we sometimes offer it in expressions where it has no effect, e.g. {? singleton @_ _ ?} : Bool
where singleton : ∀a. a -> List a
. This seems odd.
from primer.
It would be great if we could reach a point where the manual
FinishHole
action is never actually necessary. I figured this should be possible, since a naive implementation would just be to perform a post-TC pass of auto-applying the action wherever it's available.
I agree (modulo one concern). The issue here is how to do it efficiently, and potentially how to choose which subset of holes to finish if there are conflicts (I haven't thought about whether this is possible).
My one concern here is that there may be holes that the student wants to keep around for some reason -- perhaps it contains a type-correct term but it is semantically wrong. This however is somewhat orthogonal, and maybe should be dealt with by adding a flag on holes "student-defined"/"automatically-created".
However, while tring to work out exactly when the action is offered in the first place (the
Succ
example in OP is invalid now with saturated-constructors), I've just noticed that we sometimes offer it in expressions where it has no effect, e.g.{? singleton @_ _ ?} : Bool
wheresingleton : ∀a. a -> List a
. This seems odd.
Yes, we simply offer it at any hole. I have not thought about how to detect whether it is a sensible action efficiently.
from primer.
Related Issues (20)
- Are we building (should we build) dependencies with `-O2`
- More robust Wasm support
- When looking for matches for holes, prefer local bindings over top-level/in-scope module binding
- Future work on interpreter
- wasm: always build with `-O2`
- Property test failure (possibly Wasm-related?) HOT 1
- Primer language -> Wasm compiler HOT 1
- Compile Primer programs to Wasm
- Only run Wasm tests on merge queue or workflow dispatch HOT 2
- Use Buildkite artifacts to cache Wasm build artifacts HOT 1
- Benchmark results aren’t fetched from Cachix HOT 3
- `primer-service`: look into RFC 9457
- Duplication in interpreter implementation
- Hook interpreter up to API
- `tasty_two_interp_agree` property test failure HOT 3
- `tasty_redex_independent` property test failure
- `tasty_multiple_requests_accepted` property test failures HOT 1
- `RecordPair TyConName ValConName` does not serialize nicely in the OpenAPI API
- Interpreter can't reduce top-level definitions
- Investigate `weeder-nix`
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from primer.