Comments (2)
Right now, when you add an annotation to an expression, the type is defaulted to
?
. This change would mean that we instead default the type to be whatever the type ofe
actually is. More precisely, ife
synthesisesT
then we would producee : T
, otherwise ife
is successfully checked againstS
during typechecking, we would producee : S
. Since a successful typechecking pass must synthesise or check every expression, this approach will always find a type.
I was just about to submit an issue on this particular point right here, but I was coming at it from the user's perspective, rather than the implementation's — i.e., if the user wants to add an annotation, the new annotation should be as specific as it can be given the information that the typechecker has available. I think this is consistent with our principle of being explicit rather than implicit. It might also help users develop their ability to determine types "by eye," by giving them an oracle by which to test their theories.
Therefore, obviously, I support this idea.
To deal with these two cases, we could disallow annotations on holes. The type of a hole is always
?
, so we can argue that annotations are never necessary. But they can be useful if you know what the type of the expression should be, but haven't finished constructing it yet.
Disallowing annotations on holes, this I am less sure about. If we're taking a types-first approach, then I can imagine this is the very first thing you want to do with the initial hole: I know the program/function I want to build, so let's start by specifying its type. What if we only allowed an annotation on a hole if it refines the type? By "refine" here I mean, "makes the type more specific."
So here I'm imagining something like: you click the "Add annotation" button on the initial hole and you're given a modal dialog[*] where you can only proceed once you've specified at least one concrete type (or parameterized type, for any parameterized type that might be in scope at this particular hole).
Does that make sense?
[*] edit Maybe not actually a modal dialog, as that might be weird if you're trying to construct, say, a function type.
from primer.
I'm generally in favour, but...
Right now, when you add an annotation to an expression, the type is defaulted to
?
. This change would mean that we instead default the type to be whatever the type ofe
actually is. More precisely, ife
synthesisesT
then we would producee : T
, otherwise ife
is successfully checked againstS
during typechecking, we would producee : S
. Since a successful typechecking pass must synthesise or check every expression, this approach will always find a type.
... it's not this easy. Sure, for "add an annotation" action, let's do this. But what about the annotations added by smart holes because you want to put something checkable where we need synthesis? E.g. in ? x
, try adding a lambda in the hole: this needs to give an annotation also, currently (λx. ? :: ?) x
. Certainly in this case we could annotate with ? -> ?
, but can we always do something non-trivial?
Similarly, what about if we have a non-trivial annotation and the user trivialises it: ? :: S -> T
and hit "delete" on the arrow which currently leaves ? :: ?
, but if we do this change should presumably just leave ?
and would "delete the thing under the cursor".
Certainly these issues are not insurmountable! They may even shed some light on the smart holes deletion thing that we have been considering lately as well: hackworthltd/vonnegut#194.
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.