CODEWITHSUNDEEP
agda
Marko Grdinić
Marko Grdinić

Reputation: 4062

Is there an associative list in the standard library?

I am not confident enough to try proving properties about the AVL tree that is there, so I want to try something simpler. I could implement it on my own, but do not want to spend time doing that if it is already hiding in the library somewhere.

Upvotes: 1

Views: 101

Answers (1)

gallais
gallais

Reputation: 12113

You could use a list of pairs and the notion of membership can then be encoded via Any.

Bits of a very basic library:

open import Data.List.Base using (List)
open import Data.List.Relation.Unary.Any
open import Data.Maybe
open import Data.Product
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

AssocList : Set → Set → Set
AssocList A B = List (A × B)

private
  variable
    A B : Set

_∈_ : A → AssocList A B → Set
a ∈ abs = Any ((a ≡_) ∘ proj₁) abs

module Decidable {A : Set} (_≟_ : Decidable {A = A} _≡_) where

  _∈?_ : Decidable (_∈_ {A} {B})
  a ∈? abs = any ((a ≟_) ∘ proj₁) abs

  _‼_ : (abs : AssocList A B) (a : A) → Maybe B
  abs ‼ a with a ∈? abs
  ... | yes p = just (proj₂ (lookup p))
  ... | no ¬p = nothing

Upvotes: 2

Related Questions