Addresses issue agda#2092

Author: jamesmckinna

CHANGELOG.md

@@ -985,6 +985,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 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.List.Relation.Unary.Null`
+
+
 Deprecated modules
 ------------------
 

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

@@ -0,0 +1,108 @@
+------------------------------------------------------------------------
+-- 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  : List A
+    ys  : List B
+
+------------------------------------------------------------------------
+-- Example deployment: a safe head function
+
+safe-head : (xs  : List A) → .{{NonNull xs}} → A
+safe-head (x ∷ _) = x
+
+------------------------------------------------------------------------
+-- 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 ys = scanr xs in
+                   let instance _ = scanrNonNull {xs = xs} in
+                   scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys
+  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 ]⁺
+
+  refine⁻ (scanr⁺ []) = e ∷ []
+  refined (scanr⁺ []) = _
+  
+  scanr⁺ (x ∷ xs) with refine⁺ ys ← scanr⁺ xs with y ∷ _  ← ys
+    = refine⁺ (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 ys = scanr xs in
+                   let instance _ = scanrNonNull {xs = xs} in
+                   scanr (x ∷ xs) ≡ f x (safe-head ys) ∷ ys
+  unfold-scanr-∷ xs  with refine⁺ ys ← scanr⁺ xs with y ∷ _  ← ys = refl
+
+
+
+

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

@@ -0,0 +1,57 @@
+------------------------------------------------------------------------
+-- 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 Level
+open import Relation.Binary.PropositionalEquality using (_≢_; refl)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Unary.Null
+
+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

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

@@ -0,0 +1,54 @@
+------------------------------------------------------------------------
+-- 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 Level using (Level)
+open import Relation.Binary.PropositionalEquality using (_≢_; refl)
+open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Unary.Null
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Instance
+
+instance 
+
+  nullℕ : Null ℕ
+  nullℕ = record { null = _≡ᵇ 0 }
+
+------------------------------------------------------------------------
+-- Simple predicates
+
+-- Instances
+
+instance
+  nonZero : NonNull (suc n)
+  nonZero = _
+
+-- Constructors
+
+≢-nonZero : n ≢ 0 → NonNull n
+≢-nonZero {n = zero}  0≢0 = contradiction refl 0≢0
+≢-nonZero {n = suc _} n≢0 = _
+
+>-nonZero : n > 0 → NonNull n
+>-nonZero z<s = _
+
+-- Destructors
+
+≢-nonZero⁻¹ : ∀ n → .{{NonNull n}} → n ≢ 0
+≢-nonZero⁻¹ (suc n) ()
+
+>-nonZero⁻¹ : ∀ n → .{{NonNull n}} → n > 0
+>-nonZero⁻¹ (suc n) = z<s
+

src/Relation/Unary/Null.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- 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 Function.Base using (_∘_)
+open import Level
+open import Relation.Unary using (Pred)
+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
+
+  not-null = not ∘ null
+
+NonNull : {{Null A}} → Pred A _
+NonNull {{nullA}} = T ∘ not-null where open Null nullA
+
+[_]⁺ : (A : Set a) → {{nA : Null A}} → Set a
+[ A ]⁺ {{nullA}} =  [ x ∈ A || not-null x ] where open Null nullA
+  

src/Relation/Unary/Refinement.agda

@@ -0,0 +1,42 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Design pattern: refinement types
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Unary.Refinement where
+
+open import Data.Bool.Base using (Bool; T)
+open import Level
+
+private
+  variable
+    a : Level
+
+------------------------------------------------------------------------
+-- Refinement type [ x ∈ A || p ]: like Σ-type, but with irrelevant proj₂
+
+record Refinement {A : Set a} (p : A → Bool) : Set a where
+
+  constructor refine⁺
+
+  field
+
+    refine⁻      : A
+    .{{refined}} : T (p refine⁻)
+
+infix 2 RefinementSyntax
+
+RefinementSyntax : (A : Set a) (p : A → Bool) → Set a
+RefinementSyntax A p = Refinement p
+
+syntax RefinementSyntax A (λ x → p) = [ x ∈ A || p ]
+
+------------------------------------------------------------------------
+-- Export
+
+open Refinement public
+
+