[x] 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.
Summary
Given the function
Data.Vect.nubBy
, I propose to lift its local functionnubBy'
into the global scope, rename it tonubByImpl
and give it thepublic 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 functionnubBy
is marked aspublic export
, nothing can actually be proven about it. This is because it immediately calls a local function, which is:public export
The proposal
Given the current definition of
Data.Vect.nub
:I propose to move the local function
nubBy'
to the global scope, rename it tonubByImpl
and mark it aspublic export
.Examples
The function
Data.Vect.foldr
faces a similar situation; in order to make proofs about it in thecontrib
library, its inner function has been moved to the global scope asfoldrImpl
and been markedpublic export
. Without this, the proofs in contrib'sData.Vect.Properties.Foldr
module would not be possible.Technical implementation
Alternatives considered
The local function could also be defined inside a namespace:
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 markedpublic 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.