Skip to content

Fix unlawful instance Ord DL #22

@ninioArtillero

Description

@ninioArtillero

The following instance on Data.Algorithm.Diff is unlawful:

-- DL has fields poi and poj corresponding to the horizontal and vertical coordinates, respectively, of a node in a graph.
instance Ord DL
        where x <= y = if poi x == poi y
                then  poj x > poj y
                else poi x <= poi y

Because it violates reflexivity: x <= x is False for every x. Essentially, this happens due to the equal-poi branch comparing poj with a strict >. However, even if changed to >=, it is still not clear to me why the instance is defined like this. One lead is that this definition can be described as:

When poi values are equal, the instance prefers the DL node with on a higher /k-diagonal/.

Where a k-diagonal is the diagonal containing all edit graph nodes x such that poi x - poj x = k. For more details, look at #21.

This is harmless in the current context, since the only use of this instance is the max call in dstep, which always returns one of its arguments, and when both candidates occupy the same position, either choice is equivalent. Furthermore, in practice, competing candidates always share a k-diagonal, so equal poi implies equal poj.

This ticket is for making the instance law-abiding or removing it in favour of a local max-like helper. Either way, the intended semantics should be clarified (or, if found incorrect, fixed) and documented.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions