Open Data.Vect.nubBy for compile-time proofs

[troiganto]

• I have read CONTRIBUTING.md.
• I have checked that there is no existing PR/issue about my proposal.

Summary

Given the function Data.Vect.nubBy, I propose to lift its local function nubBy' into the global scope, rename it to nubByImpl and give it the public export visibility.

Motivation

For context, this has previously been discussed on Discord and I've been recommended to attempt a PR. The contribution guidelines recommended to open an issue first.

Partially for practice, partially as a hobby, I've recently been writing proofs about the various functions that act of Vect n a, proving e.g. statements about vectors in which no item occurs twice. Unfortunately, although the function nubBy is marked as public export, nothing can actually be proven about it. This is because it immediately calls a local function, which is:

• not public export
• not mentionable outside the function itself

The proposal

Given the current definition of Data.Vect.nub:

public export
nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
nubBy = nubBy' []
  where
    nubBy' : forall len . Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
    -- ...

public export
nub : Eq elem => Vect len elem -> (p ** Vect p elem)
nub = nubBy (==)

I propose to move the local function nubBy' to the global scope, rename it to nubByImpl and mark it as public export.

Examples

The function Data.Vect.foldr faces a similar situation; in order to make proofs about it in the contrib library, its inner function has been moved to the global scope as foldrImpl and been marked public export. Without this, the proofs in contrib's Data.Vect.Properties.Foldr module would not be possible.

Technical implementation

public export
nubByImpl : forall len . Vect m a -> (a -> a -> Bool) -> Vect len a -> (p ** Vect p a)
nubByImpl acc p []      = (_ ** [])
nubByImpl acc p (x::xs) with (elemBy p x acc)
  nubByImpl acc p (x :: xs) | True  = nubByImpl acc p xs
  nubByImpl acc p (x :: xs) | False with (nubByImpl (x::acc) p xs)
    nubByImpl acc p (x :: xs) | False | (_ ** tail) = (_ ** x::tail)

||| Make the elements of some vector unique by some test
|||
||| ```idris example
||| nubBy (==) (fromList [1,2,2,3,4,4])
||| ```
public export
nubBy : (a -> a -> Bool) -> Vect len a -> (p ** Vect p a)
nubBy = nubByImpl []

||| Make the elements of some vector unique by the default Boolean equality
|||
||| ```idris example
||| nub (fromList [1,2,2,3,4,4])
||| ```
public export
nub : Eq a => Vect len a -> (p ** Vect p a)
nub = Nub.nubBy (==)

Alternatives considered

The local function could also be defined inside a namespace:

public export
nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
nubBy = NubBy.impl []
  where
    namespace NubBy
      public export
      impl : forall len . Vect m elem -> (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
      -- ...

However, this would implicitly add all parameters of nubBy to its signature even though it has no need for them. The implementation would also have to change significantly to accommodate the changed signature.

Naming the local function outside of nubBy is not possible without a namespace, e.g. nubBy.nubBy' does not work. This is true even if the local function is marked public export.

Conclusion

Given the current language design, it seems that local functions cannot be used inside functions whose implementation is supposed to be public for the use of third-party compile-time proofs.

[gallais]

👍