Improve structural equality of function definitions

[timjs]

Related problem

Structural equality of types and functions is Unison's key feature. However, with the current language incarnation, there is an issue with structural equality on functions. Branching on booleans can be written in different ways: with guards, with an if-then-else expression, or with a match-with expression.

Take for example the filter function on lists. Below three definitions are minor variations on its definition. However, they are currently not regarded structurally equal.

filter1 p xs = match xs with
  [] -> []
  x +: xx
    | p x -> x +: filter1 p xx
    | otherwise -> filter1 p xx

// is structurally different from
filter2 p xs = match xs with
  [] -> []
  x +: xx -> if p x
    then x +: filter2 p xx
    else filter2 p xx

// is structurally different from
filter3 p xs = match xs with
  [] -> []
  x +: xx -> match p x with
    true -> x +: filter3 p xx
    false -> filter3 p xx

I think we can improve on this matter.

Solution 1

One could argue that if-then-else could be translated into match-with using the following transformation:

if e0 then e1 else e2
  ==>
match e0 with
  true -> e1
  false -> e2

In other words: if-then-else is syntactic sugar, so filter2 and filter3 should now be structurally equal. However, we still have guards! So filter1 is still structurally different...

Solution 2

The reason filter1 is structurally different from filter2 and filter3, is because Unison mixes declarative-based syntax with expression-based syntax. In Haskell, one can write filter in two styles:

-- declarative based
filter1 p [] = []
filter1 p (x : xs)
   | p x = x : rest
   | otherwise = rest
   where
     rest = filter1 p xs

-- expression-based
filter2 p xs = case xs of
   [] -> []
   x : xx ->
      let rest = filter2 p xx
      in  if p x
         then x : rest
         else rest

Note the first example uses several equations for one function, guards, and a where-block at the end of an equation. The second example uses case-of, if-then-else, and let-in at the start of the subexpression.

As is, Unison syntax is mostly expression based: match-with, if-then-else, and bindings (in Unison without keywords) are all expressions. There is just one exception: guards!

Proposal

Therefore I'd like to propose the following:

1. remove guards from the language, making Unison fully expression based;
2. introduce a multi-way branch expression, called guard;
3. rewrite matches on boolean expressions to a multi-way branch;
4. (probably) remove if-then-else from the language in favour of guard.

filter would then be written as follows. filter3 from above, would be internally rewritten to this as well.

filter p xs = match xs with
  [] -> []
  x +: xx -> guard
    p x -> x +: filter p xx
    otherwise -> filter p xx

Alternatives

• Solution 1 could be an incomplete alternative to this problem, as argued above.
• One could keep if-then-else as sugar for guard instead of removing it from the language, we'd have:

  if e0 then e1 else e2
    ==>
  guard
    e0 -> e1
    otherwise -> e2
  

• Obviously, one can bike shed about the keyword. Alternatives could be when, cond, or if. I choose guard for two reasons:
  1. the term "guard" is already naturalised in the FP community, especially for multi-way branching;
  2. it is similar in feeling to match, which is already used by Unison.
• We could translate if-then-else and the equivalent match-with from filter2 and filter3 to an empty match-with with guards:

  if e0 then e1 else e2
    ⇒
  match () with
    _ | e0 -> e1
      | otherwise -> e2
  

  However, doing this translation would not merge nested declarative-based matches. When translating filter3 for example, one would get:

  filter4 p xs = match xs with
    [] -> []
    x +: xx -> match () with
      _ | p x -> x +: filter4 p xx
        | otherwise -> filter4 p xx
  

  Which is still structurally different from filter1 above.

Prior art

• Haskell has a multi-way if expression, reading:

  if | guard1 -> expr1
     | ...
     | guardN -> exprN
  -- being roughly equivalent to
  case () of
    _ | guard1 -> expr1
    ...
    _ | guardN -> exprN
  

• Lisp/Scheme-like language tend to provide a cond macro, like Racket, which is used for multi-way branching.
• Elixir has cond for multi-way branching and doesn't support if-then-else for two-way branching.

Additional context

(None)