Implement Div, Mod, and Log for type-level nats.
ClosedPublic

Authored by yav on Sep 20 2017, 5:40 PM.

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
yav created this revision.Sep 20 2017, 5:40 PM
bgamari requested changes to this revision.Sep 20 2017, 8:03 PM
bgamari added inline comments.
libraries/base/GHC/TypeNats.hs
143

The fact that this is base-2 is slightly surprising given that the value-level log function is a natural logarithm. Perhaps Log2 would be a more appropriate name?

This revision now requires changes to proceed.Sep 20 2017, 8:03 PM
adamgundry added inline comments.
libraries/base/GHC/TypeNats.hs
134

Does "undefined" mean "does not reduce", "reduces to a type error" or "might crash the compiler"? My guess is the first of these, but the comment should say so.

yav updated this revision to Diff 14141.Sep 26 2017, 3:07 PM
yav edited edge metadata.
  • Rename Log to Log2 on bgamari's request.
  • Clarify the documentation, as requested by agundry.
yav added a comment.Sep 26 2017, 3:08 PM

Ok, I made the requested changes. @adamgundry as you'd guessed the partial functions are not reduced. I haden't thought of making them reduce to a type-error, that's a nice idea, maybe I'll give it a try.

dfeuer added a subscriber: dfeuer.Sep 28 2017, 12:33 AM
In D4002#112822, @yav wrote:
  • Rename Log to Log2 on bgamari's request.
  • Clarify the documentation, as requested by agundry.

Some packages seem to call this integerLog2 at the term level. I suppose the short version is probably fine here?

If you compromise a little, you can get Div x x = 1 and Mod x x = 0. I don't think that's likely to be dangerous, since 0/0 is more an indeterminate form than a flat-out error.

Out of curiosity, is this an attempt towards fixing Trac #13652? I ask since this comes really close—the only missing ingredient is DivMod (as well as Quot, Rem, and QuotRem, which could be simple synonyms for Div, Mod, and DivMod).

yav added a comment.Sep 28 2017, 3:08 PM

@RyanGlScott I didn't know about this ticket, but I'd seen something on the mailing lists about this, and Lennart Augustsson mentioned at ICFP that they'd find something like this useful, so I figured I'd implement it. Do we really need quot and rem? I though these only differ on -ve numbers, and here we are working with natural numbers. I did wonder about adding DivMod but figured that it would inconvenient to project from type-level pairs... Not sure. I know in Cryptol we find it useful to also have round-up division and modulus, as these are exactly what you need when chunking a sequence of something into fixed-size blocks, to compute the number of blocks and the padding respectively. Perhaps we could add these in the future.

In D4002#113163, @yav wrote:

Do we really need quot and rem? I though these only differ on -ve numbers, and here we are working with natural numbers.

Indeed, for Nat we would have Quot = Div, Rem = Mod, and QuotRem = DivMod. I was suggesting that perhaps we could define type Quot = Div (and similarly for the other two) for the sake of parity with the value-level versions that are offered. Then again, I suppose this would be easy enough for users to define, so perhaps it's not so important to define those in base. I'll leave it up to your discretion.

I did wonder about adding DivMod but figured that it would inconvenient to project from type-level pairs...

To be clear, I don't suggest implementing Div and Mod in terms of DivMod. For raw speed, I think it would be best to implement Div and Mod in terms of their value-level counterpats div and mod, and make DivMod its own thing (in terms of divMod). Then we wouldn't have to define, say, Fst and Snd to project out of it at the type level.

bgamari requested changes to this revision.Oct 3 2017, 10:35 AM

The only thing I see as remaining here is an entry in libraries/base/changelog.md.

This revision now requires changes to proceed.Oct 3 2017, 10:35 AM
yav updated this revision to Diff 14239.Oct 3 2017, 12:11 PM
  • Update changelog.md for `base.
bgamari accepted this revision.Oct 3 2017, 12:28 PM

Thanks @yav!

This revision is now accepted and ready to land.Oct 3 2017, 12:28 PM

I'll add the necessary @since annotations when I merge.

This revision was automatically updated to reflect the committed changes.