## List Syntax in Agda

Posted on April 20, 2019

Tags: 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 , 2It 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 , 2Can 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 ] ]