Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Haskell.Data.List #396

Open
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

HeinrichApfelmus
Copy link
Contributor

The purpose of this pull request is to add some functions from the module Data.List. Specifically, we add

  • delete with a proof of a property prop-elem-delete
  • nub with a proof of a property prop-elem-nub
  • sort as a postulate

We also add Haskell.Data.Ord, this is needed for sortOn.

I quite like the property

prop-elem-nub
  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
      (x : a) (ys : List a)
   elem x (nub ys)
    ≡ elem x ys

as it expresses a logical equivalence in terms of , I think that this is only available for Bool, not for Prop / Set. The proof is also very succinct.

On the other hand, the proof for prop-elem-delete is somewhat lengthy, but I'm not sure that this can be avoided, as we have to use transitivity of == at crucial points in the proof. I am using the induction hypothesis prop-elem-delete x y zs in a with clause in order to avoid doing substitutions by hand via cong.

Copy link
Member

@jespercockx jespercockx left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the PR! I have a few minor nitpicks, but otherwise this looks very good.

lib/Haskell/Data/List.agda Outdated Show resolved Hide resolved
lib/Haskell/Data/List.agda Show resolved Hide resolved
with y == z in eqyz
... | True
with x == z in eqxz
with prop-elem-delete x y zs
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A minor nitpick, but perhaps you could use using (https://agda.readthedocs.io/en/v2.7.0.1/language/with-abstraction.html#left-hand-side-let-bindings) instead of with if all you want to do is give a name to the recursive call.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, but the induction hypothesis recurse has the type

prop-elem-delete x y zs
  : elem x (delete y zs)
    ≡ (if x == y then False else elem x zs)

and I need to rewrite x == y to True or False before I can use this on the right-hand side. The using keyword intentionally does not perform this step, I really need the with clause in order to get this rewriting.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, but it's still a bit strange that you'd need to abstract over the recursive call itself, no? It does not appear anywhere in the type after all. Perhaps it would work if you change the order of the with statements so with prop-elem-delete x y zs comes first?

Copy link
Contributor Author

@HeinrichApfelmus HeinrichApfelmus Jan 29, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, it appears that Agda accepts the syntax

prop-elem-delete x y (z ∷ zs)
  with recurse  prop-elem-delete x y zs
  […]

This will serve our goal of avoiding to name recurse multiple times.

Changing with to using will result in an error

if (_ Eq.== x) y then (λ ⦃ @0 _ ⦄ → False) else
(λ ⦃ @0 _ ⦄ → Foldable.elem iFoldableList x zs)
!= False of type Bool
when checking that the expression recurse has type
Haskell.Prim.Foldable.foldMapList (_ Eq.== x)
(filter (λ x₁ → not ((_ Eq.== y) x₁)) zs)
≡ (if True then (λ ⦃ @0 _ ⦄ → False) else (λ ⦃ @0 _ ⦄ → True))

Comment on lines 28 to 31
nubBy : (a → a → Bool) → List a → List a
nubBy eq [] = []
nubBy eq (x ∷ xs) = x ∷ deleteBy eq x (nubBy eq xs)
-- inefficient, but better for proofs
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Darn, I just noticed that when eq is not an equivalence relation, there is a chance that this definition is not equivalent to the definition in Data.List. 🙈

For example, the Haskell report defines

nubBy            :: (a -> a -> Bool) -> [a] -> [a]
nubBy eq []      =  []
nubBy eq (x:xs)  =  x : nubBy eq (deleteBy eq xs)

but Agda's termination checker rejects this variant as it is not obvious that deleteBy does not enlarge the list. I did not think about it hard enough, but the result could be different from the definition given here for the inappropriate case where, say, eq = _<_. (No, don't do that. Yes, people complain about it.)

I think the best course of action is to define nubBy as a postulate and provide another postulate

prop-nub-cons
  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
      (x : a) (xs : List a)
   nub (x ∷ xs) ≡ x ∷ delete x (nub xs)

that reduces nub for lawful instances of Eq, but doesn't say anything about other uses. 🤔

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of a postulate, wouldn't it be easier to just give the definition as it is in Haskell and slap a {-# TERMINATING #-} pragma on top? There is little doubt that this definition is actually terminating, after all. You could then prove prop-nub-cons instead of postulating it too.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, the issue I perceive is that while the Haskell standard does give a definition of nubBy, it tacitly assumes that the predicate is an equivalence relation, and implementations do use other definitions of nubBy.

Specifically, the actual implementation in base-4.21.0.0 is

nubBy                   :: (a -> a -> Bool) -> [a] -> [a]
#if defined(USE_REPORT_PRELUDE)
nubBy eq []             =  []
nubBy eq (x:xs)         =  x : nubBy eq (filter (\ y -> not (eq x y)) xs)
#else
-- stolen from HBC
nubBy eq l              = nubBy' l []
  where
    nubBy' [] _         = []
    nubBy' (y:ys) xs
       | elem_by eq y xs = nubBy' ys xs
       | otherwise       = y : nubBy' ys (y:xs)

-- Not exported:
-- Note that we keep the call to `eq` with arguments in the
-- same order as in the reference (prelude) implementation,
-- and that this order is different from how `elem` calls (==).
-- See #2528, #3280 and #7913.
-- 'xs' is the list of things we've seen so far,
-- 'y' is the potential new element
elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
elem_by _  _ []         =  False
elem_by eq y (x:xs)     =  x `eq` y || elem_by eq y xs
#endif

I don't know whether the definition that was "stolen from HBC" has the same semantics as nubBy in the general case — and I'm not sure that this is a problem worth solving.

Hence my inclination to add postulates for nub that cannot be used without IsLawfulEq. In this way, we can do proofs for nub without saying anything about the semantics of nubBy eq when eq is not an equivalence relation. Given the implementations out there, I think that's actually a good way for how people should think about nubBy.


Hm. 🤔 On the matter of postulates for nub, it seems to me that adding a definition of nub with an erased IsLawfulEq constraint is probably a better choice. I would also remove nubBy for the time being, as I don't want to invest the time into formulating a proper preconditions right now.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like the approach of having nub be a defined function with a phantom IsLawfulEq constraint.

Copy link
Contributor Author

@HeinrichApfelmus HeinrichApfelmus Jan 29, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have removed nubBy and changed the definition of nub to

nub : ⦃ _ : Eq a ⦄  @0 ⦃ IsLawfulEq a ⦄  List a  List a
nub [] = []
nub (x ∷ xs) = x ∷ delete x (nub xs)

@HeinrichApfelmus HeinrichApfelmus force-pushed the HeinrichApfelmus/data-list branch from bbe636e to 2cf0f3d Compare January 29, 2025 22:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants