"We can't parse ... unless we know all the operators that it uses."
Yes, that was my reaction as well. I thought https://en.wikipedia.org/wiki/Polish_notation requires either a clear separation between operators and values (so no higher-order functions) or all operators to be binary. Parentheses (whether of the lisp or ML or other variety) permit mult-iary higher-order operations.
Also, doesn't https://en.wikipedia.org/wiki/Shunting-yard_algorithm require some sort of delimiter between operations? I thought it didn't work for nested operations without commas or parens, or the simplifying assumptions in the previous paragraph.
I think those simplifying assumptions are consistent with what dagfroberg was saying. I think "Polish notation" and "shunting-yard algorithm" make sense as terminology here, even if dagfroberg and I might each have slight variations in mind.
---
"so no higher-order functions"
I think we can get read-time arity information for local variables, but only if our read-time arity information for the lambda syntax is detailed enough to tell us how to obtain the arity information for its parameter. For instance...
-- To parse 3: We've completed an expression.
3 =:: Expr
-- To parse +: Parse an expression. Parse an expression. We've
-- completed an expression.
+ =:: Expr -> Expr -> Expr
-- To parse fn: Parse a variable. Parse an expression where that
-- variable is parsed by (We've completed an expression.). We've
-- completed an expression.
fn =:: (arg : Var) -> LetArity arg Expr Expr -> Expr
-- To parse letArity: Parse a variable. Parse an arity specification.
-- Parse an expression where that variable is parsed by that arity
-- specification. We've completed an expression.
letArity =:: (arg : Var) -> Arity n -> LetArity arg n Expr -> Expr
-- To parse arityExpr: We've completed a specification of arity
-- (Expr).
arityExpr =:: Arity Expr
-- To parse arityArrow: Parse a specification of some arity m. Parse a
-- specification of some arity n. We've completed a specification of
-- arity (Parse according to arity specification m. We've completed a
-- parse according to arity specification n.).
arityArrow =:: Arity m -> Arity n -> Arity (m -> n)
-- ...likewise for many of the other syntaxes I'm using in these arity
-- specifications, which isn't to say they're all *easy* or even
-- *possible* to specify in this metacircular way...
This extensible parser is pretty obviously turning into a half parser, half static type system, and now we have two big design rabbit holes for the price of one. :)
Notably, Telegram's binary protocol actually takes an approach that seems related to this, using dependent type declarations as part of the protocol: https://core.telegram.org/mtproto/TL
