Arc Forumnew | comments | leaders | submitlogin
2 points by rocketnia 2041 days ago | link | parent

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