Binding patterns

[ccshan]

A simple useful piece of syntactic sugar would be to allow lambda and let to bind not just a variable but any pattern. At least a pattern should be

pattern ::= var tpannot | (pattern,...) tpannot
tpannot ::= | : type

but maybe we should also allow

• discarding (_)
• selecting a component of an additive tuple
• matching a constructor, perhaps only if there is no other constructor in that data type

But if we allow matching a constructor, then it would be ambiguous to write

data Unit = Unit
\Unit. ...

because we have no lexical distinction between constructor (Unit being used) and variable (Unit being bound).

This would help discourage currying or partial application (#95).

[davidweichiang]

85

[davidweichiang]

This would get more interesting if case xs of Cons x _ does not count as a use of xs.

[davidweichiang]

An interesting test case for this would be edit distance, which I'd like to write as:

data Symbol = A | B;
data String = Nil | Cons Symbol String;

define ins = \y. factor 0.5 in ();
define del = \x. factor 0.5 in ();
define sub = \x. \y. factor 0.5 in ();

define distance = \xs. \ys.
  case (xs, ys) of
      (Nil, Nil) -> ()
      (Cons x xs, Nil) -> let () = del x in distance xs Nil
      (Nil, Cons y ys) -> let () = ins y in distance Nil ys
      (Cons x xs', Cons y ys') -> amb (let () = del x in distance xs' ys)
                                      (let () = ins y in distance xs ys')
                                      (let () = sub x y in distance xs' ys')

distance (Cons A (Cons B Nil)) (Cons B (Cons A Nil))

The tuple patterns are nicer than nested cases, but the fourth case has nonlinear use of xs and ys.

[davidweichiang]

One idea would be to write it like this:

case (xs, ys) of
    ...
    (Cons x xs', Cons _ _) -> let () = del x in distance xs' ys
    (Cons _ _, Cons y ys') -> let () = ins y in distance xs ys'
    (Cons x xs', Cons y ys') -> let () = sub x y in distance xs' ys'

The underscores would not count as uses, so this is linear, and if case has multiple matching patterns, all of them match in an implicit amb.

In other words, amb e1 e2 could be thought of as syntactic sugar for case () of () -> e1 | () -> e2 (which has a certain symmetry to it, since we're also internally treating <e1, e2> as amb (e1, ()) ((), e2).

[ccshan]

To clarify, I originally wanted to focus on patterns that always match (in exactly one way) in places like lambda and let.

I would want to write distance as

define distance = \xs. \ys.
  amb (case (xs,ys) of (Nil, Nil) -> ())
      (case (xs,ys) of (Cons x xs', _) -> let () = del x in distance xs' ys)
      (case (xs,ys) of (_, Cons y ys') -> let () = ins y in distance xs ys')
      (case (xs,ys) of (Cons x xs', Cons y ys') -> let () = sub x y in distance xs' ys')

perhaps with some explicit liberating marker that allows overlapping patterns.

[davidweichiang]

Does your version also need | _ -> fail?

So the idea on the table is to allow patterns in lambda, let, and case, and make _ a special pattern that does not count as a use of the thing it matches against?

[ccshan]

My original idea FWIW would only extend the syntax for lambda and let, and I would make the parser expand it as syntactic sugar.

[davidweichiang]

Partly addressed in #129