Proposal: μ Syntax

tags: S-Juvix Juvix juvix-project

Preamble

Currenlty the syntax of Juvix is quite large, with an over 200 line BNF. This means that trying to make any extensions to the syntax should be carefully thoughtout and considered, as any change may make another part of the syntax inconsistent. Further, due to the large size it can't be studied in terms of any small data structure, we must write a 200 line nested ADT to properly hold and traverse this structure. Thus if we have any chance of properly extending the language to be ergonomic for validity-predicates or any domain an user may want. To facilitate this, we will hold the following values in-regards to syntax.

1. Be minimal.
2. Be consistent.
3. Be homoiconic.

Rule 1 gives us the outline that for the syntax we chose it should be as small as possible. This helps us to do analysis over the syntax.

Rule 2 gives the user a consistent interface to properly "intuit" the language, and have understanding one part of the syntax help the user undersatnd another part.

Rule 3 is what gives us the power. By viewing Juvix's syntax as a data-structure in Juvix, we can do analysis and extend to any degree we wish.

Consistent Syntax

Rules:

1. Symbols
2. Prefix-Application
3. Infix
4. stop (;)
5. Grouping
   • = .
   • ( )
6. Further Reader extensions

BNF

exprssion ::= <grouping-expression>

grouping-expression ::= <group-start> <stop-expression> <group-end>
                      | <stop-expression>

stop-expression ::= <infix-expression> <stop> <expression>
                  | <infix-expression>  <stop>
                  | <infix-expression>
                  ;; I believe this is correct to go up again
                  | <grouping-expression>

infix-expression ::= <expression-no-infix> <op> <epxression>
                   | <expression-no-infix>

expression-no-infix ::= <application>
                      | <name-symbol>
                      | <number>
                      | <string>

applicaiton ::= <expression> <expression>*

name-symbol ::= <symbol>.<name-symbol>
              | <symbol>

symbol ::= utf-8-no-infix

op ::= <symbol>.<op>
     | <infix-symbol>

infix-symbol ::= utf-8-infix

number ::= numeric-stack-here

group-start ::= (
              | =
group-end ::= )
            | .

Extensions

Builtin Reader Extensions

1. [ ]
   • list-able
2. { }
   • record-able
3. \ ~
   • Freeze and UnFreeze
4. " "
   • String-able

Indent Sensitivity

The Given Syntax rules, while concise and powerful, lack ergonomics when it comes to actually writing code. Even basic macros like def have to be written like

def foo a b c =
  a + b + c.;

Where we end the definition with a . and a ;. the . here ends the = . block, while the ; tells the def macro to finish taking arguments.

Ideally we could write such forms like

def foo a b c = 
  a + b + c

where the . and the ; are implied by the indentation. For basic forms like above, we can achieve it with the following algorithm:

1. for = . blocks, increase the indentation level by at least 1.
2. for applications, increase the indentation level by at least 1.
3. Code with the same indentation level shall be separated by ;.
4. When we reach the same indentation level as the last expression finish = . blocks with a . and finish with a ;.
5. If we reach the end of a block, and another block is open inside then close both of them.

This algorithm works quite great and even gets us the intended ML semantics of the following:

-- Example 1.

def foo a b =
  long-function-call
    a
   b
-- equal to

def foo a b =
  long-function-call a b.;


-- Example 2.

def foo a b =
  print a
  print b
  b + a

-- print a to stdout
def print a = IO.format True "~A" a

-- equal to

def foo a b =
  print a;
  print b;
  b + a.;

-- print a to stdout
def print a = IO.format True "~A" a.;

-- Example 3.

def add-3 xs =
  List.map (lambda x = 3 + x) xs
  
-- Translates into

def add-3 xs =
  List.map (lambda x = 3 + x.) xs.;

Note that although .'s are infered we can still write them by hand if that is considered more aesthetic

-- the ; is still inferred, but the . is placed explicitly here
def add-3 xs =
  List.map (lambda x = 3 + x.) xs.
  
-- Also Valid
def add-3 xs =
  List.map (lambda x = 3 + x) xs.

However issues start to arise when we get to infix functions, how do we handle the following

def even-mod-p? xs p =
  List.map (lambda x = mod x p) xs
  |> List.filter (lambda x = mod x 2 == 0)

-- translates into
def even-mod-p? xs p =
  List.map (lambda x = mod x p.) xs;
  |> List.filter (lambda x = mod x 2 == 0.).;

Here we can see that we end up with the confusing form

def even-mod-p? xs p =
  List.map (lambda x = mod x p.) xs;
  |> List.filter (lambda x= mod x 2 == 0.).;

Where |> is applied to 1 argument and the List.map is just tossed away, ideally this would be resolved into

def even-mod-p? xs p =
  List.map (lambda x = mod x p.) xs
  |> List.filter (lambda x = mod x 2 == 0.).;

where |> is now applied, piping the output from List.map into List.filter.

This isn't the only instance of this idiosyncrasy, it also shows up here

def quadratic-formula a b c =
  -b + sqrt (b^2 - 4 * a * c) / 
  2 * a * c
  
-- Translates into
def quadratic-formula a b c =
  -b + sqrt (b^2 - 4 * a * c) /;
  2 * a * c.;

You can see when the / here is applied to 1 argument, an unexpected result for what we meant.

These issues can be solved by adding 2 rules to the current set:

1. for = . blocks, increase the indentation level by at least 1.
2. for applications, increase the indentation level by at least 1.
3. Code with the same indentation level shall be separated by ;.
4. When we reach the same indentation level as the last expression finish = . blocks with a . and finish with a ;.
5. If we reach the end of a block, and another block is open inside then close both of them.
6. If in a a;b block has a end with an infix-symbol, then combine the blocks by the infix symbol in a.
7. If in a a;b block has b start with an infix-symbol, then combine the blocks by the infix symbol in b.

Now we can write our two examples

-- Example 1.
def quadratic-formula a b c =
  -b + sqrt (b^2 - 4 * a * c) / 
  2 * a * c


-- Translates into
def quadratic-formula a b c =
  -b + sqrt (b^2 - 4 * a * c) / (2 * a * c).;

-- Example 2

def even-mod-p? xs p =
  List.map (lambda x = mod x p) xs
  |> List.filter (lambda x = mod x 2 == 0)

-- Translates into
def even-mod-p? xs p =
  List.map (lambda x = mod x p.) xs 
  |> List.filter (lambda x = mod x 2 == 0.).;

With this, indent sensitivity is complete.

Reminders for myself

#{3 : 4, 4 : 5} {| foo : int } { foo = 3 }
fmap (match (3 + 4))
     `[ = foo 5 bar 3
      ; { foo 8 bar (8 + 3) }
      ; { foo => (8 + 3); bar => 8 }
      ; = foo => 5; bar => 3. ]

(=> foo (+ 8 3))

`((foo 3) (baz 5))
{ foo => 3; baz => 5}


def foo =
  match (3 + 4) {
    foo => 5
    baz => 3
  }

{| foo = 3; fi = 5}
{| foo = 3; fi = 5} ====> record {foo = 3; fi = 5} ===> record-object
def foo =
  match (3 + 4) {
    foo (5 + 3)
    baz 3
  }

def foo =
  match (3 + 4) =
    foo (5 + 3)
    baz 3
  .

zipWith (\x y -> def x a b c) ['foo; 'bar; 'baz] [1; 2; 3]
zipWith (λ (x y) def x a b c) ['foo; 'bar; 'baz] [1; 2; 3]
zipWith (λ (x y) { def x a b c }) ['foo; 'bar; 'baz] [1; 2; 3]
zipWith (λ (x y) { def x a b c = y.}) ['foo; 'bar; 'baz] [1; 2; 3]
zipWith (λ (x y) { def x a b c y}) ['foo; 'bar; 'baz] [= 1 .; = 2 .; = 3.]

First class syntax is real, don't ignore it

• = . freezes
• { } freezes