Make sorted data structures in standard library depend of `Ord k`

iacore commented 2 years ago

Summary

Currently, a term of SortedMap hides the term of Ord k it depends on. I suggest that sorted data types should depend on Ord k at type level, to help better reasoning of sorted data types in proofs.

Motivation

Data.SortedMap.merge

Merge two maps using the Semigroup (and by extension, Monoid) operation. Uses mergeWith internally, so the ordering of the left map is kept.

This is horror. If somebody uses merge to merge maps with different ordering, it's probably unintended.

Data.SortedMap.Dependent.SortedDMap

The two constructors of SortedDMap can have seperate Ord k. As a result,

insert : (x : k) -> v x -> SortedDMap k v -> SortedDMap k v

-may change the ordering of the map. There is no way to prove the ordering is preserved since it is not available to the outsider.

The proposal

Make sorted data types depend of Ord k.

Data.SortedSet.SortedSet
Data.SortedMap.SortedMap
Data.SortedMap.Dependent.SortedDMap

Examples

before:

data SortedSet : Type -> Type

after:

data SortedSet : {auto ord: Ord a} -> (a: Type) -> Type

Technical implementation

Left as an exercise to the reader.

Alternatives considered

N/A to this issue.

Conclusion

See Summary

buzden commented 2 years ago

The problems with this I see:

this ord implicit parameter will appear explicitly each time you have two or more sets in a signature; like, union : SortedSet {ord} a -> SortedSet {ord} a -> SortedSet {ord} a. Why, then, not to consider it to be an explicit parameter? Its auto nature is really needed in functions, not in a type (see also below on this)

your signatures in some cases either would not allow user to decide ordering, or would require pretty hairy signatures; like

-- fixes particular ordering of pairs
cartesian : SortedSet {ord=ordA} a -> SortedSet {ord=ordB} b -> SortedSet (a, b)

-- hairy and fragile signature
cartesian : (ordP : Ord a => Ord b => Ord (a, b)} -> SortedSet {ord=ordA} a -> SortedSet {ord=ordB} b -> SortedSet {ord=ordP} (a, b)

you can get an ambiguities, especially in signatures

f : Ord a => SortedSet a -> (x, y : a) -> So (x < y) -> Whatever
   --                                       ^^^^^ ambiguity

when you return a set, you may need to return it with a dependent pair or, again, hairy signatures with early propagation of orderings:
```
analyseStruct : Struct -> (ord ** SortedSet {ord} Part)
-- or --
analyseStruct' : (ord : Ord Part) => Struct -> SortedSet {ord} Part
```
When the implementation builds the resulting set non-trivially, the second type can become
```
analyseStruct' : Ord SubPart1 => Ord SubPart2 => Struct -> (ord ** SortedSet {ord} Part)
```

This all is not meant to say that this idea is bad. I mean that in some cases it's good to have an ordering on a type and in some cases it's not. Maybe, we should consider an implementation with oderings in signatures and their mirrors without ones (implemented through first ones).

Anyway, implementations with orderings in a signature should have variants which take sets with different orderings and produces a set with, say, an ordering of the left one, just because this sometimes is what exactly is needed (say, when you get a set from somewhere and use it to build your own set and care only about elements, not about ordering).

iacore commented 2 years ago

Anyway, implementations with orderings in a signature should have variants which take sets with different orderings and produces a set with, say, an ordering of the left one, just because this sometimes is what exactly is needed (say, when you get a set from somewhere and use it to build your own set and care only about elements, not about ordering).

This could be a function to merge any two Foldable a.

I'll try to write an implementation now.

idris-lang / Idris2