Proposal: add integer division to GHC.TypeLits

[Oleg Grenrus]

What would be the semantics, especially what

    Div n 0

would reduce to: `TypeError` or be irreducible i.e. be stuck?

I'm quite neutral about adding `Div` and `Mod` (after all, I added
`AppendSymbol` :),
-1 for `DivMod` (we need `Fst` and `Snd`in `base` too).
Yet, how about the rest of families in `Data.Constraint.Nat` [1] ?

1. Note: If we add them, let's only add them to GHC.TypeNats.
2. Note: current type families form decidable system, which
`ghc-typelits-natnormalize` [2] can solve. Adding division complicates
that story.

Cheers, Oleg.

[1]:
http://hackage.haskell.org/package/constraints-0.9.1/docs/Data-Constraint-Nat.html
[2]: https://hackage.haskell.org/package/ghc-typelits-natnormalise


On 07.06.2017 02:32, Alexey Vagarenko wrote:
> I'd like to propose adding Div, Mod and DivMod type families to
> GHC.TypeLits, 
> which would be promoted versions of methods of Integral class.
>
> type family Div :: Nat -> Nat -> Nat
> type family Mod :: Nat -> Nat -> Nat
> type family DivMod :: Nat -> Nat -> (Nat, Nat)
>
> I've made trac ticket for this
> https://ghc.haskell.org/trac/ghc/ticket/13652
> some time ago, but it hasn't got much attention.
>
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170608/3fde9235/attachment.sig>