Refinement types plus Null/NonNull

CHANGELOG.md

@@ -1048,6 +1048,19 @@ Major improvements
 * A new module `Algebra.Lattice.Bundles.Raw` is also introduced.
   * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module.
 
+### Generalised the definition of `NonZero` from `Data.Nat.Base` to `NonNull` based on:
+
+* A new module `Relation.Unary.Refinement` defining a general notion of refinement
+  of a type wrt a `Bool`-valued/`Decidable` predicate.
+
+* A new module `Relation.Unary.Null` defining being able to test for `null`ity,
+  based on a `Bool`-valued predicate `null`, using `Refinement`.
+
+* Instances `Data.{Nat|List}.Relation.Unary.Null` of `Null` for `Nat` and `List`.
+
+* Example uses in `README.Data.{Nat|List}.Relation.Unary.Null`
+
+
 * In `Relation.Binary.Reasoning.Base.Triple`, added a new parameter `<-irrefl : Irreflexive _≈_ _<_`
 
 Deprecated modules

README/Data/List/Relation/Unary/Null.agda

@@ -0,0 +1,140 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Illustration of the `NonNull predicate over `List`
+------------------------------------------------------------------------
+
+module README.Data.List.Relation.Unary.Null where
+
+open import Data.List.Base using (List; []; _∷_; head)
+open import Data.List.Relation.Unary.Null
+open import Data.Product.Base using (Σ; _,_; proj₁; proj₂; ∃₂; _×_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Unary.Null
+open import Relation.Unary.Refinement
+
+private
+  variable
+
+    a b   : Level
+    A     : Set a
+    B     : Set b
+    x     : A
+    xs zs : List A
+
+------------------------------------------------------------------------
+-- Example deployment: a safe head function
+
+safe-head : (xs  : List A) → .{{NonNull xs}} → A
+safe-head (x ∷ _) = x
+
+safe-head-≡ : (eq : x ∷ xs ≡ zs) →
+              let instance _ = subst NonNull eq _ in x ≡ safe-head zs
+safe-head-≡ refl = refl
+
+------------------------------------------------------------------------
+-- Example deployments: scans
+
+-- ScanL
+
+module ScanL (f : A → B → A) where
+
+  scanl : A → List B → List A
+  scanl e []       = e ∷ []
+  scanl e (x ∷ xs) = e ∷ scanl (f e x) xs
+
+  instance scanlNonNull : {e : A} {xs : List B} → NonNull (scanl e xs)
+  scanlNonNull {xs = []}     = _
+  scanlNonNull {xs = x ∷ xs} = _
+
+  scanl⁺ : A → List B → [ List A ]⁺
+  scanl⁺ e xs = refine⁺ (scanl e xs)
+
+
+-- ScanR
+
+module ScanRΣ (f : A → B → B) (e : B) where
+
+-- design pattern: refinement types via Σ-types
+
+  scanrΣ        : List A → Σ (List B) NonNull
+  scanrΣ []                                       =     e ∷ [] , _
+  scanrΣ (x ∷ xs) with ys@(y ∷ _) , _ ← scanrΣ xs = f x y ∷ ys , _
+
+  scanr         : List A → List B
+  scanr xs = proj₁ (scanrΣ xs)
+
+  instance scanrNonNull : {xs : List A} → NonNull (scanr xs)
+  scanrNonNull {xs = xs} = proj₂ (scanrΣ xs)
+
+  unfold-scanr-∷ : ∀ xs → let instance _ = scanrNonNull {xs = xs} in
+                   scanr (x ∷ xs) ≡ f x (safe-head (scanr xs)) ∷ scanr xs
+  unfold-scanr-∷ xs with ys@(y ∷ _) , _ ← scanrΣ xs = refl
+
+
+module ScanR (f : A → B → B) (e : B) where
+
+-- design pattern: refinement types via mutual recursion
+
+-- to simulate the refinement type { xs : List A | NonNull xs }
+-- define two functions by mutual recursion:
+-- `f`         : the bare, 'extracted' underlying function
+-- `fNonNull` : the (irrelevant instance) witness to the refinement predicate
+
+-- but for now, again we seem to have to go via a third function
+-- essentially `scanrΣ` but with an irrelevant instance field instead
+
+  scanr⁺ : List A → [ List B ]⁺
+  scanr⁺ []                                                    =     e ∷⁺ []
+  scanr⁺ (x ∷ xs) with refine⁺ ys ← scanr⁺ xs with y ∷ _  ← ys = f x y ∷⁺ ys
+
+  scanr : List A → List B
+  scanr xs = refine⁻ (scanr⁺ xs)
+
+  instance scanrNonNull : {xs : List A} → NonNull (scanr xs)
+  scanrNonNull {xs = xs} with refine⁺ ys ← scanr⁺ xs with y ∷ _  ← ys = _
+
+  unfold-scanr-∷ : ∀ xs → let instance _ = scanrNonNull {xs = xs} in
+                   scanr (x ∷ xs) ≡ f x (safe-head (scanr xs)) ∷ scanr xs
+  unfold-scanr-∷ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _  ← ys = refl
+
+  unfold-scanr-∷≡ : ∀ xs → let ys = scanr xs in
+                    ∃₂ λ y ys′ → ys ≡ y ∷ ys′ × scanr (x ∷ xs) ≡ f x y ∷ ys
+  unfold-scanr-∷≡ xs with refine⁺ ys ← scanr⁺ xs with y ∷ _  ← ys
+    = y , _ , refl , refl
+
+
+module ScanR′ (f : A → B → B) (e : B) where
+
+-- design pattern: refinement types via mutual recursion, using `nonNull-[_]⁻`
+
+-- to simulate the refinement type { xs : List A | NonNull xs }
+-- define two functions by mutual recursion:
+-- `f`         : the bare, 'extracted' underlying function
+-- `fNonNull` : the (irrelevant instance) witness to the refinement predicate
+
+-- but still using a `helper` function
+
+  scanr : List A → List B
+  instance scanrNonNull : {xs : List A} → NonNull (scanr xs)
+
+  private
+    helper : (xs : List A) → ∃₂ λ y ys → scanr xs ≡ y ∷ ys
+    helper xs = nonNull-[ scanr xs ]⁻ {{scanrNonNull {xs = xs}}}
+
+  scanr []       = e ∷ []
+  scanr (x ∷ xs) with y , _ ← helper xs = f x y ∷ scanr xs
+
+  scanrNonNull {xs = []}     = _
+  scanrNonNull {xs = x ∷ xs} with _ ← helper xs = _
+
+  unfold-scanr-∷ : ∀ xs → let instance _ = scanrNonNull {xs = xs} in
+                   scanr (x ∷ xs) ≡ f x (safe-head (scanr xs)) ∷ (scanr xs)
+  unfold-scanr-∷ xs with y , _ , eq ← helper xs
+    = cong (λ y → f _ y ∷ scanr xs) (safe-head-≡ (sym eq))
+
+  unfold-scanr-∷≡ : ∀ xs → let ys = scanr xs in
+                    ∃₂ λ y ys′ → ys ≡ y ∷ ys′ × scanr (x ∷ xs) ≡ f x y ∷ ys
+  unfold-scanr-∷≡ xs with y , _ , eq ← helper xs = y , _ , eq , refl
+

README/Data/Nat/Relation/Unary/Null.agda

@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Null instance for ℕ
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module README.Data.Nat.Relation.Unary.Null where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Nat.Relation.Unary.Null
+open import Relation.Unary using (Decidable)
+open import Relation.Unary.Null
+
+------------------------------------------------------------------------
+-- Properties of NonZero
+------------------------------------------------------------------------
+
+nonZero? : Decidable NonZero
+nonZero? = NonNull?
+
+------------------------------------------------------------------------
+-- Specimen reimplementation
+
+open import Agda.Builtin.Nat
+  using (div-helper; mod-helper)
+
+-- Division
+-- Note properties of these are in `Nat.DivMod` not `Nat.Properties`
+
+_/_ : (dividend divisor : ℕ) → .{{NonZero divisor}} → ℕ
+m / n@(suc n-1) = div-helper 0 n-1 m n-1
+
+-- Remainder/modulus
+-- Note properties of these are in `Nat.DivMod` not `Nat.Properties`
+
+_%_ : (dividend divisor : ℕ) → .{{NonZero divisor}} → ℕ
+m % n@(suc n-1) = mod-helper 0 n-1 m n-1

src/Data/List/Relation/Unary/Null.agda

@@ -0,0 +1,73 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Null instance for List
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.List.Relation.Unary.Null where
+
+open import Data.Nat.Base as Nat using (_>_; z<s)
+open import Data.List.Base as List using (List; []; _∷_; length)
+open import Data.Product.Base using (∃₂; _,_)
+open import Level
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Unary.Null
+open import Relation.Unary.Refinement
+
+private
+  variable
+    a  : Level
+    A  : Set a
+    x  : A
+    xs : List A
+
+
+------------------------------------------------------------------------
+-- Instance
+
+instance
+  nullList : Null (List A)
+  nullList = record { null = List.null }
+
+------------------------------------------------------------------------
+-- NonNull
+
+-- Instances
+
+instance
+  nonNull : NonNull (x ∷ xs)
+  nonNull = _
+
+-- Constructors
+
+≢-nonNull : xs ≢ [] → NonNull xs
+≢-nonNull {xs = []}    []≢[] = contradiction refl []≢[]
+≢-nonNull {xs = _ ∷ _} xs≢[] = _
+
+>-nonNull : length xs > 0 → NonNull xs
+>-nonNull {xs = _ ∷ _} _ = _
+
+-- Destructors
+
+≢-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → xs ≢ []
+≢-nonNull⁻¹ (_ ∷ _) ()
+
+>-nonNull⁻¹ : (xs : List A) → .{{NonNull xs}} → length xs > 0
+>-nonNull⁻¹ (_ ∷ _) = z<s
+
+-- Existentials
+
+nonNull-[_]⁻ : (xs : List A) → .{{NonNull xs}} → ∃₂ λ y ys → xs ≡ y ∷ ys
+nonNull-[ x ∷ xs ]⁻ = x , xs , refl
+
+[_]⁻ : (r : [ List A ]⁺) → ∃₂ λ y ys → refine⁻ r ≡ y ∷ ys
+[ refine⁺ xs ]⁻ = nonNull-[ xs ]⁻
+
+-- Smart constructor
+
+_∷⁺_ : A → List A → [ List A ]⁺
+_∷⁺_ x xs = refine⁺ (x ∷ xs) {{_}} where instance _ = nonNull
+

src/Data/Nat/Relation/Unary/Null.agda

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Null instance for ℕ
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Relation.Unary.Null where
+
+open import Data.Nat.Base using (ℕ; zero; suc; _≡ᵇ_; _>_; z<s)
+open import Relation.Binary.PropositionalEquality using (_≢_; refl)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Unary using (Pred)
+open import Relation.Unary.Null
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Instance
+
+instance
+
+  nullℕ : Null ℕ
+  nullℕ = record { null = _≡ᵇ 0 }
+
+NonZero : Pred ℕ _
+NonZero = NonNull
+
+------------------------------------------------------------------------
+-- Simple predicates
+
+-- Instances
+
+instance
+  nonZero : NonZero (suc n)
+  nonZero = _
+
+-- Constructors
+
+≢-nonZero : n ≢ 0 → NonZero n
+≢-nonZero {n = zero}  0≢0 = contradiction refl 0≢0
+≢-nonZero {n = suc _} n≢0 = _
+
+>-nonZero : n > 0 → NonZero n
+>-nonZero z<s = _
+
+-- Destructors
+
+≢-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n ≢ 0
+≢-nonZero⁻¹ (suc n) ()
+
+>-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0
+>-nonZero⁻¹ (suc n) = z<s
+

src/Relation/Unary/Null.agda

@@ -0,0 +1,51 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The predicate of being able to decide `null`ity
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Unary.Null where
+
+open import Data.Bool.Base using (Bool; not; T)
+open import Data.Bool.Properties using (T?)
+open import Function.Base using (_∘_)
+open import Level
+open import Relation.Unary using (Pred; Decidable)
+open import Relation.Unary.Refinement
+
+private
+  variable
+    a : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- Definition
+
+record Null (A : Set a) : Set a where
+
+  field
+
+    null : A → Bool
+
+  non-null = not ∘ null
+
+------------------------------------------------------------------------
+-- Type constructor
+
+[_]⁺ : (A : Set a) {{nullA : Null A}} → Set a
+[ A ]⁺ {{nullA}} = [ x ∈ A |ᵇ non-null x ] where open Null nullA
+
+------------------------------------------------------------------------
+-- Derived notions
+
+module _ {{nullA : Null A}} where
+
+  open Null nullA
+
+  NonNull : Pred A _
+  NonNull = T ∘ non-null
+
+  NonNull? : Decidable NonNull
+  NonNull? = T? ∘ non-null