ListSyntax

List Syntax in Agda

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