Patterns

^Syntax
Pattern :
      PatternNoAlt

PatternNoAlt :
      BindingPattern
   | Unit
   | PairPattern
   | ExistentialPattern

PatternList :
      PatternNoAlt (, PatternNoAlt)^* ,^?

There are two properties of a pattern: What names it binds and whether it’s refutable.

Patterns can appear in several places:

• in a let binding:

  // as an expression
  let p = x in y
  
  // or in process syntax
  let p = x
  rest...
  

  All bindings of p must be used in y or rest... respectively. Here, p must be irrefutable.

• between [ and ]

  // in a function expression
  [p] body
  
  // destructing a pair (process syntax)
  tail[p]
  rest...
  

  All bindings of p must be used in body or rest... respectively. Here, p must also be irrefutable.

• in pattern matching, i.e. either destruction/choice construction

  // either destruction
  x {
    .label (p) rest_payload => y
    ...
  }
  // in process syntax, the rest_payload isn't present
  // (instead, x becomes it)
  
  // choice construction
  {
    .label (p) => y
    ...
  }
  

  All bindings of p must be used in y. Here, p must also be irrefutable.

Binding Patterns

^Syntax
BindingPattern : ID Annotation^?

The pattern name or name: T is always irrefutable and binds name to x when matching x.

The pattern name can be used on a value which type is known. Otherwise, name: T must be used, which can only be used on a value of type T.

Binding patterns are the most used patterns.

// break up an expression
do {
  let v1 = e1
  let v2 = e2
} in // expression using v1 and v2

If the type of the value matched is already known, a type annotation would have to match it. Such an annotation can be useful for declaring functions, though:

// no extra type annotation/declaration needed
def negate = [b: Bool] let result: Bool = b {
  .true! => .false!
  .false! => .true!
} in result

The Unit Pattern

^Syntax
Unit : !

^{Type | Constructing Expression | Destructing Statement}

The unit pattern ! is always irrefutable and binds nothing. It can only be used on values of type !.

// if there is a value of a type T,
// there is a function [!] T
def returns_true: [!] Bool = [!] .true!

// ! can be used to destroy a unit
def drop_two_bools: [Bool, Bool] ! = 
  [b1, b2] let ! = drop(b1) in drop(b2)

// though process syntax is generally used for this
def drop_two_bools: [Bool, Bool] ! = [b1, b2] do {
  drop(b1)?
  drop(b2)?
} in !

dec drop_bool : [Bool] ! 
def drop_bool = [b] {
  .true! => !
  .false! => !
}

Pair Patterns

^Syntax
PairPattern : ( PatternList ) Pattern

^{Type | Constructing Expression | Destructing Statement}

• A pair pattern (p) q is irrefutable if and only if both p and q are irrefutable
• When p can be used on type A and q on type B, (p) q can be used on type (A) B
• (p) q matches (a) b if and only if p matches a and q matches b
• When matching (a) b, the bindings are those of p matching a, together with those of q matching b

Having multiple patterns between ( and ) is just syntax sugar:

// the pattern
(p, q) r
// is equivalent to
(p) (q) r

A pair pattern is used to destruct a value of a pair type:

dec uncurry : [type A, B, C] [[A, B] C] [(A, B)!] C
def uncurry = [type A, B, C] [f] [(a, b)!] f(a, b)

Existential Patterns

^Syntax
ExistentialPattern : ( type ID ) Pattern

^{Type | Constructing Expression | Destructing Statement}

• An existential pattern (type X) p can only be used on an existential type (type T) A and p must be able to be used on type A
• When it can match, it is irrefutable if and only if p is irrefutable
• (type X) p matches (type T) a if and only if p matches a
• When matching (type T) a, the bindings are those of p matching a, and X is bound to T

Having multiple types between ( and ) is just syntax sugar:

// the pattern
(type X, Y) p
// is equivalent to
(type X) (type Y) p

An existential pattern is used to destruct a value of an existential type

type Any = (type T) T

def any_test: Any = do {
  let x: Any = (type Bool) .true!
  let (type X) x_val = x
  // X = Bool
  // x_val = .true!
  let y: X = x_val
} (type X) y

Future

More extensive pattern matching, along with more types of patterns is planned in the future. See here for more.