Irrelevant instance predicate NonNull for List, Vec, ...

[jamesmckinna]

Proposal: we already have in Data.List.Base

null : List A → Bool
null [] = true
null _ = false

so is it time to add (cf. #1538 etc.)

NonNull : List A → Set _
NonNull = T ∘ not ∘ null

etc.
with eg

instance
  nonNull⇒nonZero[length] : {{ _ : NonNull xs }} → NonZero (length xs)
  nonNull⇒nonZero[length] {xs = _ ∷ _} = _

etc.
together with some structure proxying for the type class for having a null method and a NonNull predicate... etc.

[jamesmckinna]

Re: #1538 and the choice of a record-based definition to avoid explicit import of Data.Unit:
the only reason to explicitly import would be to have the name tt in scope...
... but AFAIU, Agda will happily do (forced) argument inference on any sub-term of type ⊤ without ever having to explicitly mention either ⊤ or tt, because of eta for records... so _ ALWAYS suffices?

I think that's why I used vanilla T in #2000, and in the above fragments, because instances will likewise ALWAYS be given by _... so no imports necessary, and the error messages don't really seem to be better for having the record wrapper (or are they?).

Is this understanding correct? If so, could we refactor NonZero to be the Nat instance of the Null typeclass, for the obvious null = _≡ᵇ 0 implementation?

[jamesmckinna]

See my refinement+null branch for an initial improved sketch towards a PR. Not quite the panacea I'd hoped, even for scanr...

UPDATED: see #2103 , and now (specialised to) #2260

(Comment carried over from #2260 )
This latter PR 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 on Nat, but IMHO that's a purely contingent state of affairs, ... cf. the #2258, 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...

[jamesmckinna]

Six months on, and having closed #2260 already, I'll close this for lack of any positive take-up.