Add NonNull to Data.List.Relation.Unary.NonNull on the model of Data.Nat.Base.NonZero

[jamesmckinna]

This is a cherry-picked/revised version of #2092 / #2103 specialised to List only, prompted by the discussion in
this stackoverflow question

Outstanding issues:

• only the specimen applications to head and tail are defined; (so also: naming)
• UPDATED no properties added to Data.List.Properties; but perhaps the constructors/destructors should move there to Data.List.Relation.Unary.NonNull.Properties;
• no (additional) examples added to README.*;
• no refactoring/deprecation of (any, or all) of Data.List.NonEmpty;
• ...

Yields the following solution to the above stackoverflow problem:

module ScanrNonNull (f : A → B → B) (e : B) where

  scanr-nonNull : ∀ xs → NonNull (scanr f e xs)
  scanr-nonNull [] = _
  scanr-nonNull (x ∷ xs)
    with _ ← scanr-nonNull xs
    with y ∷ ys ← scanr f e xs = _

  scanr-head : (xs : List A) → B
  scanr-head xs = nonNull-head (scanr f e xs)
    where instance _ = scanr-nonNull xs

  scanr-head-unfold : ∀ x xs → scanr-head (x ∷ xs) ≡ f x (scanr-head xs)
  scanr-head-unfold x xs
    with _ ← scanr-nonNull xs
    with y ∷ ys ← scanr f e xs = refl

Coupled with the redefinition of scanr in #2258 , this solution then simplifies further to:

  scanr-nonNull : ∀ xs → NonNull (scanr xs)
  scanr-nonNull xs = _

  scanr-head : (xs : List A) → B
  scanr-head xs = nonNull-head (scanr xs)

  scanr-head-unfold : ∀ x xs → scanr-head (x ∷ xs) ≡ f x (scanr-head xs)
  scanr-head-unfold x xs
    with _ ← scanr-nonNull xs
    with y ∷ ys ← scanr xs = refl

[JacquesCarette]

I am strongly against this addition to Data.List.Base. This feels like a 'bad smell' coming from non-dependently-typed programming where you don't want to say that you know your list is non-null but want to defer this to proof search instead.

Can NonNull exist in stdlib in some module that I personally will never import? Sure!

[jamesmckinna]

@JacquesCarette Ouch! OK...

... easy enough, I guess, to punt this to Data.List.Relation.Unary.NonNull?

But as the PR makes clear, this began as a simple-minded emulation of the compromise we already make in Data.Nat.Base to admit NonZero and NonTrivial as unary predicates, and the (binary) ordering relations as well. So a 'principled' solution might be... quite drastic in its knock-on consequences, were we also to take them seriously for Nat, cf. #1925 .

Here, not so much, because we don't have the same commitment to NonNull reasoning on List as we do to NonZero/NonTrivial reasoning onNat, but IMHO that's a purely contingent state of affairs, ... cf. the scanr PR, exposing that we might want to take NonNull reasoning more seriously in general. And as that PR demonstrates, the type-based analysis trading off between List and List⁺ is not entirely without wrinkles itself...

(meta: Maybe these last two paragraphs belong on the issue #2092, but no-one has commented on that since I posted it... DONE)

[JacquesCarette]

That punt definitely would make me happy.

I agree that this is analogical (in design) to NonZero and NonTrivial. And indeed, we had a lot of equivalent-to-NonZero reasoning already in place. (And I agree, those two paragraphs should be duplicated in the issue.)

I feel like we have not explore the full design space of principled solutions for nonnull reasoning. To me, the conclusion that I draw from the scanr experiment is that its output type should be List⁺ !

[jamesmckinna]

Have resolved the merge conflict wrt CHANGELOG, but there doesn't seem to be sufficient enthusiasm for this, so closing. Will maybe re-open at a later date if there were to be further (positive!?) discussion of #2092 ...