List Syntax in Agda

Posted on April 20, 2019
Tags:

Just some silly examples of how to get a nice list syntax with mixfix operators in Agda.

Intro and Imports 
{-# OPTIONS --without-K --safe #-}

module ListSyntax where

open import Data.List as List using (List; _∷_; [])
open import Data.Product
open import Level using (_⊔_; Level)
open import Data.Nat using (ℕ; _+_; suc; zero)
open import Function

variable
  a b : Level
  A : Set a
  B : Set b

Approach 1:

With instance search.

module Instance where
  record ListSyntax {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
    field [_] : B → List A

  open ListSyntax ⦃ ... ⦄ public

  instance
    cons : ∀ {a b} {A : Set a} {B : Set b} ⦃ _ : ListSyntax A B ⦄
         →  ListSyntax A (A × B)
    [_] ⦃ cons ⦄ (x , xs) = x ∷ [ xs ]

  instance
    sing : ∀ {a} {A : Set a} → ListSyntax A A
    [_] ⦃ sing ⦄ = _∷ []

Advantages:

No type annotation needed for singleton list. 
--_ : List ℕ ← not needed
  _ = [ 1 ]
It can even work as a standalone function: 
  _ : List ℕ → _
  _ = List.map [_]
It uses a closed operator, so we don’t need parentheses to parse it: 
  _ = List.foldr _+_ 0 [ 1 , 2 , 3 ]
And it doesn’t clash with product: 
  _ : ℕ × ℕ
  _ = 1 , 2
It allows nesting: 
  _ : List (List ℕ)
  _ = [ [ 1 ] , [ 2 , 3 ] ]

Disadvantages

However, it needs type annotations when there is more than one item in the list and there’s no other way to guess the items. 
  _ : List ℕ
  _ = [ 1 , 2 , 3 ]

Approach 2: With a Datatype

module DataType where
  infixr 5 _]
  data ListBuilder {a} (A : Set a) : Set a where
    _,_ : A → ListBuilder A → ListBuilder A
    _] : A → ListBuilder A

  infixr 4 [_
  [_ : ListBuilder A → List A
  [ x , xs = x ∷ ([ xs)
  [ x ] = x ∷ []

Advantages:

Single and multi-item lists without type annotation: 
--_ : List ℕ ← not needed
  _ = [ 1 , 2 , 3 ]

--_ : List ℕ ← not needed
  _ = [ 1 ]

Doesn’t clash with product:

  _ : ℕ × ℕ
  _ = 1 , 2
Can choose different “list-like” type based on first bracket: 
  open import Data.Vec as Vec using (_∷_; []; Vec)

  len-1 : ListBuilder A → ℕ
  len-1 (x , xs) = suc (len-1 xs)
  len-1 (x ]) = 0

  infixr 4 v[_
  v[_ : (xs : ListBuilder A) → Vec A (suc (len-1 xs))
  v[ (x , xs) = x ∷ (v[ xs)
  v[ x ] = x ∷ []

  _ : Vec ℕ 3
  _ = v[ 1 , 2 , 3 ]

Disadvantages

Not a closed operator, so need parens:

  _ = List.foldr _+_ 0 ([ 1 , 2 , 3 ])
Singleton isn’t a function 
--_ = [_]
Doesn’t nest 
--_ = [ [ 1 ] , [ 2 , 3 ] ]