Comments (8)
Some additional helpful context: Can you estimate how (relative) frequently each of these annotations will occur?
In particular, if dynamic is not ubiquitous, then I might suggest no operator for it and using only keywords instead. I'm admittedly steeped in Haskell at this point, but my immediate instinct is that :
is the only extremely-well-established operator of the bunch. So I'd suggest :
for static (let signatures and also just term annotations) and a spelled-out keyword for dynamic. Maybe a word proximal to assert
/assume
/etc?
I had considered :!
and :?
but I think I could argue that either symbol make sense for either mode. That's an example of why I'd hesitate to rely on symbols alone.
I would vote against (the current motivation for) :>
because coercions and/or casts are useful even for statically-checked types (cf Haskell's System FC etc).
HTH. Good luck.
from nickel.
Some additional helpful context: Can you estimate how (relative) frequently each of these annotations will occur?
Good question. My take is:
Promise
would be used in library code: each time you have a function generic enough to be reused somewhere else which is also typable, you should type it via aPromise
. This documents the interface, you get static guarantees and, even if this is not the case today, it can in theory allow some run-time checks to be optimized away, given your type system is sound.Assume
has several use-cases:- Use untyped code inside typed code, a.k.a type casting. If you want to use untyped code in a typed code, it will have type
Dyn
, which you can only pass to functions acceptingDyn
or return. If you are convinced your value is aNum
for example, you'll use alet x_typed = Assume(Num, x)
and you can then use it as aNum
inside your typed code. I don't expect this to happen that often, given that a typed function will probably use explicitly declared arguments rather than an untyped variable from the environment, but who knows. It can still happen that you have to cast aDyn
value to something else, because it is returned by another function even if typed itself. - Type non-typable code. You may have a function which is a candidate for static typing, but not typable (either because of its complexity or the limitations of the type system). In this case, you would use an
Assume
as a poor man'sPromise
, as it still documents the functions, makes it possible to use it in statically typed code, and checks at run-time that every call conforms to the specified type. - Run-time check, a.k.a contracts.
Assume
makes it possible to check a value against a contract at run-time, which is specified by the type annotation. In that case, it is rather used in untyped code as a convenient way to check higher-order assertions, and has no static meaning. This is expected to be used rather frequently, since configurations are expected to be checked via contracts rather than via static typing. That is, contracts serve as data schemas. On the other hand, another mechanism (fields meta-data or enriched values) gives a preferred alternative syntax to describe record contracts, which is probably the most important usage.
- Use untyped code inside typed code, a.k.a type casting. If you want to use untyped code in a typed code, it will have type
To sum up, I expect Promise
to be used in library code, so not too rare, but not as much as in a statically typed language. I expect assume to be used directly less often, as even if it is the fundamental construct which underlies the other way of specifying contracts via field meta-data, the user will probably prefer the latter whenever possible.
from nickel.
I would vote against (the current motivation for)
:>
because coercions and/or casts are useful even for statically-checked types (cf Haskell's System FC etc).
After a bit more thinking, this is also a good remark. In particular, we may make use of static coercions to be able to convert a static record type {a: Num, b: Num}
to a dynamic one {_: Num}
for example, or to forget a part of the tail of a row type (see #158) from {a: Num, b: Num}
to {a: Num | Dyn}
. All of which could be checked at typechecking phase and avoid run-time checks, but currently require an assume.
from nickel.
A bit more widely used operator for type casting is the as
operator (Typescript, Swift), so term as type
.
from nickel.
non strict: the default mode, where no typing is enforced. This correspond to untyped code. The typechecker just traverses the term, looking for potential chunks that have to be statically checked.
strict: statically check a term against a type, and enforce that each subexpression is well-typed as well. Correspond to the behavior of the typechecker of a standard statically typed language.
This is a bit of an aside, but I'd like this terminology not to become part of the user-facing documentation. I don't think that they represent very well what's happening (i.e. looking for something to typecheck, and typechecking, respectively).
Some additional helpful context: Can you estimate how (relative) frequently each of these annotations will occur?
I thought Haskell's ::
vs :
thing taught us not to use this sort of metrics for syntax design 😛
Some proposals.
- I think that it's fairly uncontroversial that promise be written as
term : type
(probably parenthesised). - We also want to be able to add type annotations on
let
binders as you (@yannham ) suggests. - We probably also want type signature à la Haskell such as
let x : type x = term
As for assert: it is a form of a type-cast: from Dyn
to whatever type we are considering, so it's sort of fine to write it with a case-like notation. That being said, we may want to distinguish a cast where the from-type is inferred, from a cast where the from-type is just taken to be Dyn
. I'm just not sure that "inferring" means anything very precise as soon as we have a Dyn
type around. Do all term have one most-precise type that we can infer? If so, maybe we want to reserve :>
to "infer left-hand side's type then add a contract", as you suggest above.
from nickel.
It occurs to me, in light of #187 , that we can have attributes on lets as well. And
let x
| type mytype
| value term
Can also act as assert.
from nickel.
We probably also want type signature à la Haskell such as
let x : type x = term
This looks very close to let x : type = term
. I guess we should have one or the other, but the two together seems redundant and a bit confusing.
I'm just not sure that "inferring" means anything very precise as soon as we have a Dyn type around. Do all term have one most-precise type that we can infer?
I suppose so, this would be the type inferred by the typechecker. We have to exclude polymorphic types, or at least rank-N types as well as the Dyn type. But not having studied formally the current type system, this is just a supposition.
It occurs to me, in light of #187 , that we can have attributes on lets as well. And
let x | type mytype | value term
Can also act as assert.
I really like the idea, this looks good and makes the notation coherent with meta-values, which have precisely the same semantics. But I would prefer to keep the "= term" part, otherwise this would be confusing to go from = sth
to | value sth
:
let x = term in
exp
// need to change from "= term" to "| value term"
let x
| type mytype
| value term in
exp
// feel more natural, and just amount to adding a line to the original expression
let x
| type mytype
= term in
exp
from nickel.
from nickel.
Related Issues (20)
- Wrong version is reported by `nickel --version` for release artifacts HOT 7
- Variant of `std.contract.from_predicate` to specify an error message
- Some utilities in `std.array`: `remove_duplicates` and `filter_map` HOT 5
- Allow my users to use contracts shared on GitHub HOT 2
- `nickel doc` overflows the stack with recursive schemas HOT 2
- Forward the metadata when re-exporting a field HOT 1
- Hovering on a record field defined several times will only show the information for the first definition HOT 1
- Filter out the contract annotations on hover/completion when they don't add anything
- Output query results as JSON HOT 4
- Add empty YAML header when exporting
- Encode/decode JSON string HOT 2
- Make record pattern matching recursive HOT 6
- [Question] How to serialize sum type to json? HOT 3
- Bikeshed a name for `apply_as_custom`
- Short-circuiting version of `fold_left`
- Bikesheding: formatting of multi-line expressions enclosed in parentheses HOT 1
- Expose more math functions HOT 2
- Record row polymorphism can be destructive HOT 2
- 1.7.0 retag issue HOT 3
- Typechecking in recursive records shouldn't be confused by variables in an outer scope.
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 nickel.