search

mstksg / typelits-witnesses

Existential witnesses, singletons, and classes for operations on GHC TypeLits
http://hackage.haskell.org/package/typelits-witnesses
MIT License
10 stars 13 forks source link

Behavior for negative results with subtraction #1

Closed mstksg closed 5 years ago

mstksg commented 8 years ago

It's not clear what the proper behavior under (%-) should be. If we follow the conventions of Numeric.Natural, it'll be a runtime error. Two other potential behaviors would be to have a (%-) equivalent, but where the result is a Maybe (Dict (KnownNat (n - m))) instead of just the Dict. This wouldn't work as nicely as an operator, and it wouldn't be usable with withNatOp, but it might be a more disciplined option.

Another option is just to truncate at 0, but this is probably also pretty unexpected, and you also lose distributivity.

mstksg commented 5 years ago

Issue is more or less resolved by offering unsafe and safe options.