# Syntactic Sugar¶

## 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¶

Statement Sugar Desugars to
Simple bind
```do x ← m
m'
```
```m >>= λ x →
m'
```
Pattern bind
```do p ← m
where pᵢ → mᵢ
m'
```
```m >>= λ where
p  → m'
pᵢ → mᵢ
```
Non-binding statement
```do m
m'
```
```m >>
m'
```
Let
```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 mechaincally 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
```

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
```