Yep. I just filed a precedence bug at https://github.com/jbangert/nail/issues/7 for Nail, which is a security-concious project. (It was presented at LangSec 2014).
> It doesn’t have dependent types.
Yep. Programming language theorists love type systems, and dependent types are one way to prove bounds safety, but they're not the only way. Puffs is an imperative language, not functional (for the reasons described in https://github.com/google/puffs/blob/master/doc/related-work...). With mutable state, a Puffs variable's within-bounds-ness can change over that variable's lifetime, but its type does not.
> There is limited effect typing: functions can be marked pure, impure (!), or impure coroutine (?).
Yep. That's the current design, although I'll probably revise that based on recent experience. The question mark denotes a coroutine, as you noted, but also whether that function can (very roughly speaking) throw an exception. I think we will need separate syntaxes for those two concepts, since I've wanted the latter without the former.
> There doesn’t appear to be any kind of polymorphism—over types, effects, refinements, or proofs.
Yep. Haven't needed it yet, and I've erred on the side of simplicity and leaving things out.
Doesn't that mean it rejects precedence? In a language equal precedence (e.g. Smalltalk), operators would just be executed from LTR or RTL.
That… is true, and I have a hard time computing how it would even work.
[1, 2] ⧺ [3, 4] ⧺ [5, 6] × 2 × 3
(([1, 2] ⧺ ([3, 4] ⧺ [5, 6])) × 2) × 3
[ [ [1…6], [1…6] ],
[ [1…6], [1…6] ],
[ [1…6], [1…6] ] ]
2-3^4See e.g the "precedence bug" comment I wrote elsewhere on this page.
Just to play devil's advocate (aka be annoying); parentheses are operators.
Ref: https://softwareengineering.stackexchange.com/a/208354/69247
It comes from canonization process in Vatican where someone (who is not an actual satan worshiper or against the church) argued in favor of the devil (against the candidate) to force the other pro-sainthood side to provide good solid proof of the sainthood, miracles done, etc. of the candidate.
What you're doing is just being annoying by nitpicking the casual wording. There is no debate to be had from "parentheses are kinda operators" and the meaning of the original line was understandable, even if you consider parentheses operators.
WP describes: https://en.wikipedia.org/wiki/Operator_(computer_programming...
> Occasionally parts of a language may be described as "matchfix" or "circumfix" operators, either to simplify the language's description or implementation.
Bu then, the term "operator" seems to also have mathematical roots: https://en.wikipedia.org/wiki/Operator_(mathematics)
The relevant part seems to be the definition refering to syntax, or denotation:
> Operator is also used for denoting the symbol of a mathematical operation. This is related with the meaning of "operator" in computer programming
Now, whether "the symbol" implies a singular symbol, and excludes delimiter symbols might be a matter of semantics ;-)
• All operators have equal precedence, so parentheses are required when mixing operators. I guess they’ve seen one too many bugs from precedence confusion.
• It doesn’t have dependent types; rather, it uses a proof checker with some built-in knowledge about the language, and a way to specify preconditions, postconditions, and invariants that the checker can reason about.
• There is limited effect typing: functions can be marked pure, impure (!), or impure coroutine (?).
• There doesn’t appear to be any kind of polymorphism—over types, effects, refinements, or proofs.