Similarly, Agda has a well-typed mixfix operator syntax – you define a function like (_foo_bar_baz) and can automatically write "X foo Y bar Z baz". It does mean that the operator parser has to be extensible at runtime, but it's not a huge cost for a dependently-typed language.