hs-to-coq
hs-to-coq copied to clipboard
antalsz
Wrong Key for IntSet?
In examples/containers/module-edits/Data/IntSet/Internal/edits, there is the following line right at the top:
rename type GHC.Types.Int = Coq.Numbers.BinNums.N
Shouldn't that be rename type GHC.Types.Int = Coq.Numbers.BinNums.Zinstead?
No, unfortunately IntSet's do not work for Z; only for types that are finite width or non-negative. We chose to implement it using N; see Section 5.5 of https://arxiv.org/abs/1803.06960 for a bit more details.
This is problematic though if one is using IntSet/IntMap in Haskell code. I have some Haskell code using these and I have to add conversions in these places. One can of course easily use a bijection between N and Z, but one still has to manually insert that everywhere.
I'm not sure what the best solution would be for that. Is there an edit feature that would allow one to specify such a bijection?
Yeah, I feel your pain.
Well, either the numbers in your Haskell code are always non-negative anyways. In that case, you can simply map Int to N and get “better” types in GHC.
Or the numbers in your Haskell code may actually be negative, i.e. use all of Z. In that case IntSet is not usable in Coq anyways (the algorithms do not work for unbounded integers).
Luckily, my numbers are never negative. In the paper it is mentioned that eventually you intend to use a 64-bit integer type. Is that anywhere on the horizon? (just out of curiosity)
It might happen that in the future we actually have an issue where we'd like to get some commercial support. Is there someone who would be available for that?
I have a branch where I started using 64 bit integers: https://github.com/antalsz/hs-to-coq/tree/int64 It’s doable, but turned out to be pretty tedious, and not ”academically worthwhile” at the moment.
Commercial support might be possible, but I can’t make promises at the moment. Depends on how far in the future we are talking about :-). But just ask us then again.