Combine efforts on Data.Parameterized.Map and Data.Parameterized.Sum

[Ericson2314]

Have you all seen http://hackage.haskell.org/package/dependent-map and http://hackage.haskell.org/package/dependent-sum ? We use and these a bunch at Obsidian and help maintain them. They ostensibly are the same as Data.Parameterized.Map Data.Parameterized.Sum. It probably makes sense to join efforts in maintaining just one version / see if either of us is missing any extra functionality the other might find useful.

After just a brief scroll, one difference is map equality---specifically the constraint on the values. Your EqF does not restrict the type parameter, whereas our http://hackage.haskell.org/package/constraints-extras/docs/Data-Constraint-Extras.html finitely enumerates the possible GADT indices. We are just switching to GHC 8.6, after which I hope it is possible to handle the countably infinite cases that arise in general (with indices and parameters) in that library with quantified constraints, yielding the best of both worlds. This is exactly the nice sort of insight that comes so much more readily from comparing two different implementations of the same idea.

[kquick]

Hi @Ericson2314 ,

Thanks for the heads-up about dependent-map and dependent-sum. It will be interesting to take a look at the similarities between these, but it's going to be something we will need to evaluate over a longer time period since we will need to evaluate the impact of any differences between the libraries.

Out of curiosity, were there aspects of parameterized-utils that were problematic and led you to these alternate libraries?

[Ericson2314]

Out of curiosity, were there aspects of parameterized-utils that were problematic and led you to these alternate libraries?

I think we just didn't know parameterized-utils existed. I myself just learned it was far older than I thought. That said, gap between your EqF and our Has Eq would cause problems with us. We often use (our equivalent of) MapF someK Identity, which isn't possible with yours as EqF Identity isn't inhabited.

It will be interesting to take a look at the similarities between these, but it's going to be something we will need to evaluate over a longer time period since we will need to evaluate the impact of any differences between the libraries.

Of course. Perhaps there is a "bottom up" way of doing this that could make the evaluation easier. For example a PR which leaves your map and just replaces some of the equality and ordering classes. Then if that looks good the Pair bits, then map, and so on.

[Ericson2314]

We are just switching to GHC 8.6, after which I hope it is possible to handle the countably infinite cases that arise in general (with indices and parameters) in that library with quantified constraints, yielding the best of both worlds.

Indeed it is possible. I made obsidiansystems/constraints-extras#17 to demonstrate that. That means our classes should work for the AST uses (like crucible) where you have infinitely many possible GADT indices.

[Ericson2314]

FYI some of this stuff is now been peeled off and upstreamed in the even more minimal https://github.com/phadej/some CC @phadej