Syntactic Sugar

• Hidden argument puns

• Do-notation

  • Desugaring

  • Example

• Idiom brackets

Hidden argument puns

If the option --hidden-argument-puns is used, then the pattern {x} is interpreted as {x = x}, and the pattern ⦃ x ⦄ is interpreted as ⦃ x = x ⦄. Here x must be an unqualified name that does not refer to a constructor that is in scope: if x is qualified, then the pattern is not interpreted as a pun, and if x is unqualified and refers to a constructor that is in scope, then the code is rejected.

Note that {(x)} and ⦃ (x) ⦄ are not interpreted as puns.

Note also that {x} is not interpreted as a pun in λ {x} → … or syntax f {x} = …. However, {x} is interpreted as a pun in λ (c {x}) → ….

Do-notation

A do-block consists of the layout keyword do followed by a sequence of do-statements, where

do-stmt    ::= pat ← expr [where lam-clauses]
             | let decls
             | expr
lam-clause ::= pat → expr

The where clause of a bind is used to handle the cases not matched by the pattern left of the arrow. See details below.

Note

Arrows can use either unicode (←/→) or ASCII (<-/->) variants.

For example:

filter : {A : Set} → (A → Bool) → List A → List A
filter p xs = do
  x    ← xs
  true ← p x ∷ []
    where false → []
  x ∷ []

Do-notation is desugared before scope checking and is translated into calls to _>>=_ and _>>_, whatever those happen to be bound in the context of the do-block. This means that do-blocks are not tied to any particular notion of monad. In fact if there are no monadic statements in the do block it can be used as sugar for a let:

pure-do : Nat → Nat
pure-do n = do
  let p2 m = m * m
      p4 m = p2 (p2 m)
  p4 n
check-pure-do : pure-do 5 ≡ 625
check-pure-do = refl

Desugaring

do x ← m
   m’

m >>= λ x →
m’

do p ← m
     where pᵢ → mᵢ
   m’

m >>= λ where
         p  → m’
         pᵢ → mᵢ

do () ← m

m >>= λ ()

do m
   m’

m >>
m’

do let ds
   m’

let ds in
m’

If the pattern in the bind is exhaustive, the where-clause can be omitted.

Example

Do-notation becomes quite powerful together with pattern matching on indexed data. As an example, let us write a correct-by-construction type checker for simply typed λ-calculus.

First we define the raw terms, using de Bruijn indices for variables and explicit type annotations on the lambda:

infixr 6 _=>_
data Type : Set where
  nat  : Type
  _=>_ : (A B : Type) → Type
data Raw : Set where
  var : (x : Nat) → Raw
  lit : (n : Nat) → Raw
  suc : Raw
  app : (s t : Raw) → Raw
  lam : (A : Type) (t : Raw) → Raw

Next up, well-typed terms:

Context = List Type
-- A proof of x ∈ xs is the index into xs where x is located.
infix 2 _∈_
data _∈_ {A : Set} (x : A) : List A → Set where
  zero : ∀ {xs} → x ∈ x ∷ xs
  suc  : ∀ {y xs} → x ∈ xs → x ∈ y ∷ xs
data Term (Γ : Context) : Type → Set where
  var : ∀ {A} (x : A ∈ Γ) → Term Γ A
  lit : (n : Nat) → Term Γ nat
  suc : Term Γ (nat => nat)
  app : ∀ {A B} (s : Term Γ (A => B)) (t : Term Γ A) → Term Γ B
  lam : ∀ A {B} (t : Term (A ∷ Γ) B) → Term Γ (A => B)

Given a well-typed term we can mechanically erase all the type information (except the annotation on the lambda) to get the corresponding raw term:

rawIndex : ∀ {A} {x : A} {xs} → x ∈ xs → Nat
rawIndex zero    = zero
rawIndex (suc i) = suc (rawIndex i)
eraseTypes : ∀ {Γ A} → Term Γ A → Raw
eraseTypes (var x)   = var (rawIndex x)
eraseTypes (lit n)   = lit n
eraseTypes suc       = suc
eraseTypes (app s t) = app (eraseTypes s) (eraseTypes t)
eraseTypes (lam A t) = lam A (eraseTypes t)

Now we’re ready to write the type checker. The goal is to have a function that takes a raw term and either fails with a type error, or returns a well-typed term that erases to the raw term it started with. First, lets define the return type. It’s parameterised by a context and the raw term to be checked:

data WellTyped Γ e : Set where
  ok : (A : Type) (t : Term Γ A) → eraseTypes t ≡ e → WellTyped Γ e

We’re going to need a corresponding type for variables:

data InScope Γ n : Set where
  ok : (A : Type) (i : A ∈ Γ) → rawIndex i ≡ n → InScope Γ n

Lets also have a type synonym for the case when the erasure proof is refl:

infix 2 _ofType_
pattern _ofType_ x A = ok A x refl

Since this is a do-notation example we had better have a monad. Lets use the either monad with string errors:

TC : Set → Set
TC A = Either String A
typeError : ∀ {A} → String → TC A
typeError = left

For the monad operations, we are using instance arguments to infer which monad is being used.

We are going to need to compare types for equality. This is our first opportunity to take advantage of pattern matching binds:

_=?=_ : (A B : Type) → TC (A ≡ B)
nat      =?= nat      = pure refl
nat      =?= (_ => _) = typeError "type mismatch: nat ‌≠ _ => _"
(_ => _) =?= nat      = typeError "type mismatch: _ => _ ≠ nat"
(A => B) =?= (A₁ => B₁) = do
  refl ← A =?= A₁
  refl ← B =?= B₁
  pure refl

We will also need to look up variables in the context:

lookupVar : ∀ Γ n → TC (InScope Γ n)
lookupVar []      n       = typeError "variable out of scope"
lookupVar (A ∷ Γ) zero    = pure (zero ofType A)
lookupVar (A ∷ Γ) (suc n) = do
  i ofType B ← lookupVar Γ n
  pure (suc i ofType B)

Note how the proof obligation that the well-typed deBruijn index erases to the given raw index is taken care of completely under the hood (in this case by the refl pattern in the ofType synonym).

Finally we are ready to implement the actual type checker:

infer : ∀ Γ e → TC (WellTyped Γ e)
infer Γ (var x)    = do
  i ofType A ← lookupVar Γ x
  pure (var i ofType A)
infer Γ (lit n)    = pure (lit n ofType nat)
infer Γ suc        = pure (suc ofType nat => nat)
infer Γ (app e e₁) = do
  s ofType A => B ← infer Γ e
    where _ ofType nat → typeError "numbers cannot be applied to arguments"
  t ofType A₁     ← infer Γ e₁
  refl            ← A =?= A₁
  pure (app s t ofType B)
infer Γ (lam A e)  = do
  t ofType B ← infer (A ∷ Γ) e
  pure (lam A t ofType A => B)

In the app case we use a where-clause to handle the error case when the function to be applied is well-typed, but does not have a function type.

Idiom brackets

Idiom brackets is a notation used to make it more convenient to work with applicative functors, i.e. functors F equipped with two operations

pure  : ∀ {A} → A → F A
_<*>_ : ∀ {A B} → F (A → B) → F A → F B

As do-notation, idiom brackets desugar before scope checking, so whatever the names pure and _<*>_ are bound to gets used when desugaring the idiom brackets.

The syntax for idiom brackets is

(| e a₁ .. aₙ |)

or using unicode lens brackets ⦇ (U+2987) and ⦈ (U+2988):

⦇ e a₁ .. aₙ ⦈

This expands to (assuming left associative _<*>_)

pure e <*> a₁ <*> .. <*> aₙ

Idiom brackets work well with operators, for instance

(| if a then b else c |)

desugars to

pure if_then_else_ <*> a <*> b <*> c

Idiom brackets also support none or multiple applications. If the applicative functor has an additional binary operation

_<|>_ : ∀ {A B} → F A → F A → F A

then idiom brackets support multiple applications separated by a vertical bar |, i.e.

(| e₁ a₁ .. aₙ | e₂ a₁ .. aₘ | .. | eₖ a₁ .. aₗ |)

which expands to (assuming right associative _<|>_)

(pure e₁ <*> a₁ <*> .. <*> aₙ) <|> ((pure e₂ <*> a₁ <*> .. <*> aₘ) <|> (pure eₖ <*> a₁ <*> .. <*> aₗ))

Idiom brackets without any application (|) or ⦇⦈ expend to empty if

empty :  ∀ {A} → F A

is in scope. An applicative functor with empty and _<|>_ is typically called Alternative.

Note that pure, _<*>_, and _<|>_ need not be in scope to use (|).

Limitations:

• Binding syntax and operator sections cannot appear immediately inside idiom brackets.

• The top-level application inside idiom brackets cannot include implicit applications, so

  (| foo {x = e} a b |)

  is illegal. In case the e is pure you can write

  (| (foo {x = e}) a b |)

  which desugars to

  pure (foo {x = e}) <*> a <*> b