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.

Sign up for GitHub

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

Jump to bottom

Mimer implementation has Ord instances not compatible with Eq #7638

Open
andreasabel opened this issue Dec 4, 2024 · 0 comments
Open

Mimer implementation has Ord instances not compatible with Eq #7638

andreasabel opened this issue Dec 4, 2024 · 0 comments
Labels
style Haskell coding style (not in changelog)

Comments

@andreasabel
Copy link
Member

While reading the Mimer sources, I found with @oskeri that some Ord instances violate the laws of Ord, in particular this law:

x == y = compare x y == EQ

Source: https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-Ord.html#t:Ord

One instance violating this is SearchBranch:

agda/src/full/Agda/Mimer/Mimer.hs

Lines 156 to 162 in 7b3b899

-- | NOTE: Equality is only on the fields `sbCost` and `sbGoals`
instance Eq SearchBranch where
sb1 == sb2 = sbCost sb1 == sbCost sb2 && sbGoals sb1 == sbGoals sb2
-- TODO: Explain
instance Ord SearchBranch where
compare = compare `on` sbCost

SearchBranches are organized in a prio-queue, e.g. here:

agda/src/full/Agda/Mimer/Mimer.hs

Lines 817 to 819 in 7b3b899

let go :: Int -> Int -> MinQueue SearchBranch -> SM ([MimerResult], Int)
go 0 n _ = pure ([], n)
go need n branchQueue = case Q.minView branchQueue of

This queue is 3rd party (package pqueue).
The package docs do not state how these queues handle duplicates.
Looking at the source, duplicates seem to be allowed. However, there is no contract guaranteeing this, so future versions might deviate from the currently implemented behavior.

In general, it feels risky to have invalid Ord instances. At least, that puts the author in the obligation of giving arguments why such unlawful instances are ok. In the current code, there are no arguments written out. (There is just a "TODO: Explain").

Ord Component also violates this law:

agda/src/full/Agda/Mimer/Mimer.hs

Lines 199 to 215 in 7b3b899

data Component = Component
{ compId :: CompId -- ^ Unique id for the component. Used for the cache.
, compName :: Maybe Name -- ^ Used for keeping track of how many times a component has been used
, compPars :: Nat -- ^ How many arguments should be dropped (e.g. constructor parameters)
, compTerm :: Term
, compType :: Type
, compRec :: Bool -- ^ Is this a recursive call
, compMetas :: [MetaId]
, compCost :: Cost
}
deriving (Eq, Generic)
instance NFData Component
-- TODO: Is this reasonable?
instance Ord Component where
compare = compare `on` compId

@andreasabel andreasabel added the style Haskell coding style (not in changelog) label Dec 4, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
style Haskell coding style (not in changelog)
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@andreasabel