diff --git a/doc/syntax-philosophy.md b/doc/syntax-philosophy.md index 8311a52f9..943c568cf 100644 --- a/doc/syntax-philosophy.md +++ b/doc/syntax-philosophy.md @@ -24,8 +24,9 @@ tightest-binding to loosest-binding. | Symbol(s) | Default Meaning | Associativity | |-----------------------|------------------------------------------|---------------| -| . ! | indexing, reference slicing | Left | -| juxtaposition (space) | function application | Left | +| . | field reference | Left | +| ! | reference slicing | Left | +| juxtaposition (space) | function argument extension | Left | | unary + - | negation, integer literals | Prefix | | backquoted functions | infix application of binary functions | Left | | other | user-defined operators | Left | @@ -45,27 +46,19 @@ tightest-binding to loosest-binding. | unary .. ..< | indices up to | Prefix | | unary .. >.. | indices from | Postfix | | => | array type arrow | Right | -| -> ?-> ?=> --o | function type arrows | Right | +| -> ->> | function type arrows | Right | | >>> | forward function composition | Left | | <<< | reverse function composition | Left | -| &>> | forward isomorphism composition | Left | -| <<& | reverse isomorphism composition | Left | -| binary @ | infix from_ordinal | Left | -| unary @ | computed field name | Prefix | -| unary @... | computed name for multiple fields | Prefix | -| ... | name for multiple fields | Prefix | -| \|> | reverse function application | Left | -| $ | loose-binding function application | Right | +| @ | infix from_ordinal | Left | | :: | infix "has type" on values | None | +| $ | loose-binding function arg extension | Right | +| \| | left function arg extension | Left | | := += | assignment, accumulation | None | | : | "has type" with a binder on the left | Right | -| = | let binding, field assignment | Left | -| ? | separator for labeled rows | Left | -| , | separator for tuples, records, others | Right | | ,> | separator for dependent pairs | Right | -| & | separator for record types | Right | | &> | separator for dependent pair types | Right | -| \| | separator for variants and variant types | Left | +| = | let binding, named arguments | Left | +| , | separator for tuples, records, others | Right | |-----------------------|------------------------------------------|---------------| Why this particular precedence table? The general guiding principle is to @@ -130,9 +123,7 @@ Specifially, we want the following things: - The array arrow `=>` is tighter than the function arrows because we often want arrays in function types but not so much vice versa. - - The function arrows (`->`, `--o`, `?->`, and `?=>`) follow. They are all at - the same precedence so they can chain to form functions with intermixed - implicit, explicit, class, and linear arguments. + - The function arrows (`->`, `->>`) follow. - The colon is looser than the arrows, to make it easier to annotate binders with function types. @@ -141,89 +132,46 @@ Specifially, we want the following things: with simply-typed arguments, but we decided against that on the grounds that explicit dependent types are rarer than binders annotated with function or array types. - + 5. With that core, we move on to universal operators that interact almost everything - - Juxtaposition as function application is tighter than all the above because - functions can compute arguments to those operators + - Juxtaposition as function argument extension is tighter than all the above + because functions can compute arguments to those operators - - However, we make array indexing and reference slicing tighter than function - composition because they make function arguments very often, and we like - punning x.i as a name (in this case, for the array element) + - However, we make reference slicing tighter than function argument extenion + because they make function arguments very often, and we like punning x[i] as + a name (in this case, for the array element) - - Dollar `$` as function application is looser than all the above because the - above can compute arguments to functions + - Dollar `$` as function argument extension is looser than all the above + because the above can compute arguments to functions - - Reverse function application `|>` is just one level tighter - than dollar, because - `value |> unary |> unary |> binary $ value` - sort of makes sense, and the left pipe should compute the first, - not second, argument to the binary function + - Pipe `|` as function argument extension on the left is one level looser than + `$` for the same reason - The assignment `:=` and accumulation `+=` operators are statement-like in that they return unit, so cannot be usefully nested. Thus, they are even - looser than dollar, so that dollar can be used to compute the RHS. + looser than dollar, so that dollar can be used to compute the RHS - Binary atsign `@` is sugar for `from_ordinal` taking the number on the left - and the type on the right, and producing an index. - - - If we make it looser than indexing, then it will have to be - parenthesized as a direct argument to indexing anyway, and we - might as well make it very loose so it doesn't force parens - on any type and arithmetic computations + and the type on the right, and producing an index. We make `@` loose + because indexing is bracketed anyway + - However, it feels weird to have @ be looser than number arithmetic because it seems to want to change the interpretation of one thing, rather than a computation for things - - On the other hand, maybe it is reasonable for it to be looser - than type arithmetic, so we can write `4 @ Fin 2 & Fin 3` - - An alternative would be to make `@` tighter than indexing, so - that `xs.5@_` works. However, because indexing is tighter than - application, there's no way for `xs.5@Fin 7` to work without parens - somewhere. - - If we make `@` loose, we should probably write it with surrounding - spaces. - Also, this decision doesn't matter very much, because binary `@` is not a very common operator anyway. - - Atsign `@` is also used in the curly brace syntaxes as a prefix - to a field label that makes that field name evaluated instead - of taken literally. In this capacity, the only requirement is - that it bind tighter than the separator between the label and - the value, namely, `:` or `=`. - - - At-ellipsis `@...` is used in such syntaxes as a prefix to - denote that the field label refers to multiple fields. - - - Type arithmetic (`&`, `|`) - - - `&` should be tighter than `|` for the same reason as `&&` and `||` - - - One might argue that these should be tighter than function arrows because - we want to return or consume tuples or pairs more than we want to form - pairs of functions. - - - However, they are also used as separators for record and variant types, - where they want to be looser than `:` because `:` is used as a - sub-separator separating the field name from its type. Also, records and - variants are already grouped by curlies, so there is no pressure to make - their separators tight. - - - We choose that the latter use dominates, with the down side that pairs and - `Either` types must always be enclosed in parens. But that's fine; the - parens serve as a pun reminding the user that a pair is just a binary - record with anonymous fields. - - The dependent pair operators `,>` and `&>` are little-used as of this - writing, so we arbitrarily dump them next to their non-dependent pair - variants `,` and `&`, discussed below. + writing, so we arbitrarily make them loose. - The double colon `::` type-annotates an arbitrary expression without otherwise changing its meaning. Since it can go anywhere, we make it looser - than all expression operators, except `|>` and `$`. The exception supports + than all expression operators, except `|` and `$`. The exception supports the common concept that `$` breaks up formulas completely (by being the loosest expression-like operator). - + - We make backquoted functions and user-defined operators bind tightly by default, but for no particularly good reason. They are currently rare in Dex, so it doesn't really matter. @@ -233,12 +181,9 @@ Specifially, we want the following things: - Function composition `>>>` and `<<<` are logically the same precedence, but we don't want them to chain with each other, because that's just confusing, so we arbitrarily make `>>>` tighter than `<<<`. They should be tighter - than `$` and `|>` and looser than juxtaposition but don't interact with + than `$` and `|` and looser than juxtaposition but don't interact with anything else; so we arbitrarily make them loose. - - The same logic applies to the isomorphism composition operators `&>>` and - `<<&`. We arbitrarily make them slightly looser than the function versions. - - The monoid combine operator `<>` can technically act like `*`, `+`, `&&`, `||`, `>>>`, or `<<<` depending on the monoid, but we assume that in practice people will only use it on other data types. We make it tighter @@ -251,38 +196,22 @@ Specifially, we want the following things: 7. Dex also has a class of "operators" whose groups are not expressions, but which have precedence so they can be treated uniformly by the operator precedence stage of parsing. - + - Equals `=` is used to separate the binder from the body in a `let` or a - `def`, and as the label separator for record and variant data. In both + `def`, and as the label separator for named function arguments. In both capacities, it's reasonable to make it an operator that's looser than - everything except the separators `&`, `,`, `|`, and `?`. Notably, `=` is - looser than `:`, `$`, and `|>`, which moderately often interact with it. + everything except the separator `,`. Notably, `=` is looser than `:`, `$`, + and `|`, which moderately often interact with it. - Colon `:` is used in several places as "the object on the left as the type - on the right". It also serves as a label separator for record and variant - types. For all of these, it's reasonable to make it very loose. But it is - tighter than `=`, because it can be used to type-annotated the binder being + on the right". For this, it's reasonable to make it very loose. But it is + tighter than `=`, because it can be used to type-annotate the binder being assigned. - - Ampersand `&` and pipe `|` separate fields of record and variant types, - respectively. They should be looser than `:`. - - - Comma `,` and pipe `|` separate fields of records and variant data, - respectively. For this use case, they should be looser than `=`. - - - Comma `,` is also used to separate fields in tuple constructors, def class - argument lists, and in effect rows. In all three cases, it's already - externally grouped, so can be very low precedence. - - - Pipe `|` should be looser than comma `,`, because `|` is used to separate - the remainder of an effect row. - - - Question mark `?` separates fields in labeled rows. It should be looser - than `:`, but tighter than `,` and `|`. - - - Ellipsis `...` marks remainder groups in almost all of the above. We make - it a unary prefix operator that's tighter than the separators comma `,`, - ampersand `&`, pipe `|`, and question mark `?`, but looser than expressions. + - Comma `,` separates entries in lists: fields in tuple constructors, function + argument lists, both at definitions and applications, and effect rows. In + all these cases, it's already externally grouped, so can be very low + precedence. 8. We arbitrarily make user-defined operators tight, but looser than unary `-` and `+`, because the latter are often part of numeric literals. diff --git a/lib/prelude.dx b/lib/prelude.dx index 39c80dd8a..d58100690 100644 --- a/lib/prelude.dx +++ b/lib/prelude.dx @@ -1223,6 +1223,8 @@ def fanout(x:a) -> n=>a given (n|Ix, a) = for i. x def sq(x:a) -> a given (a|Mul) = x * x def abs(x:a) -> a given (a|Sub|Ord) = select(x > zero, x, zero - x) def mod(x:a, y:a) -> a given (a|Add|Integral) = rem(y + rem(x, y), y) +def (>>>)(f:(a) -> b, g:(b) -> c) -> (a) -> c given (a, b, c) = \x. g(f(x)) +def (<<<)(f:(b) -> c, g:(a) -> b) -> (a) -> c given (a, b, c) = \x. f(g(x)) '## Table Operations diff --git a/src/lib/ConcreteSyntax.hs b/src/lib/ConcreteSyntax.hs index 04297bcce..2f3f04f0b 100644 --- a/src/lib/ConcreteSyntax.hs +++ b/src/lib/ConcreteSyntax.hs @@ -676,19 +676,18 @@ ops = , [arrow, symOpR "->>"] , [symOpL ">>>"] , [symOpL "<<<"] - , [symOpL "&>>"] - , [symOpL "<<&"] , [symOpL "@"] - , [unOpPre "@"] - , [unOpPre "@..."] - , [unOpPre "..."] + -- TODO Actually delete code for parsing records + -- , [unOpPre "@"] + -- , [unOpPre "@..."] + -- , [unOpPre "..."] , [symOpN "::"] , [symOpR "$"] + , [symOpL "|"] , [symOpN "+=", symOpN ":="] -- Associate right so the mistaken utterance foo : i:Fin 4 => (..i) -- groups as a bad pi type rather than a bad binder , [symOpR ":"] - , [symOpL "|"] , [symOpR ",>"] , [symOpR "&>"] , [symOpL "="] diff --git a/src/lib/Lexing.hs b/src/lib/Lexing.hs index f49d3d1d3..d3533e248 100644 --- a/src/lib/Lexing.hs +++ b/src/lib/Lexing.hs @@ -162,8 +162,8 @@ doubleLit = lexeme $ knownSymStrs :: HS.HashSet String knownSymStrs = HS.fromList [ ".", ":", "::", "!", "=", "-", "+", "||", "&&" - , "$", "&", "&>", "|", ",", ",>", "<-", "+=", ":=" - , "->", "->>", "=>", "?->", "?=>", "--o", "--", "<<<", ">>>", "<<&", "&>>" + , "$", "&>", "|", ",", ",>", "<-", "+=", ":=" + , "->", "->>", "=>", "?->", "?=>", "--o", "--", "<<<", ">>>" , "..", "<..", "..<", "..<", "<..<", "?", "#", "##", "#?", "#&", "#|", "@"] -- string must be in `knownSymStrs`