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-Na... [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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries