Proposal: add integer division to GHC.TypeLits

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Proposal: add integer division to GHC.TypeLits

Alexey Vagarenko
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Proposal: add integer division to GHC.TypeLits

David Feuer
Yes please! +1

On Jun 6, 2017 7:33 PM, "Alexey Vagarenko" <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Proposal: add integer division to GHC.TypeLits

Ryan Scott
In reply to this post by Alexey Vagarenko
+1 from me as well.

Ryan S.

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Proposal: add integer division to GHC.TypeLits

Oleg Grenrus
In reply to this post by Alexey Vagarenko
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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Proposal: add integer division to GHC.TypeLits

Ryan Scott
In reply to this post by Alexey Vagarenko
To be clear, I don't think Alexey is proposing that we implement
inductive definitions of Div/Mod/DivMod to base (which, as you note,
would require implementing type-level Fst and Snd as well). One of the
motivations for this proposal is that we _did_ implement and inductive
DivMod in the singletons library [1], and it is horribly slow. What I
believe Alexey wants is a built-in type family that leverages machine
instructions to perform the div/mod calculations behind the hood, much
like we currently do for other type-level arithmetic operators, such
as (+), (-), and (*).

> Yet, how about the rest of families in `Data.Constraint.Nat`

Obviously, adding more built-in type families is perhaps not an ideal
solution, and there are certainly many more things we _could_ add. But
I think integer division is a common-enough use case that it makes
sense to support it in base. We need not bog down this proposal with
whataboutism.

> Note: If we add them, let's only add them to GHC.TypeNats.

Agreed.

> Note: current type families form decidable system, which
> `ghc-typelits-natnormalize` can solve. Adding division complicates
> that story.

Sure, but then again, there are many type families that you could
throw into this system that this particular GHC plugin couldn't reason
about. I don't see how Div/Mod are unique in that regard.

> What would be the semantics, especially what
>
>     Div n 0
>
> would reduce to: `TypeError` or be irreducible i.e. be stuck?

I would propose that it would be stuck. There is precedent for this
already: (2 - 3) is a stuck type, for instance. This is also the
approach that the ghc-typelits-extra plugin takes.

Ryan S.
-----
[1] https://github.com/goldfirere/singletons/blob/75dae57bbe06b21b3adbb82158c4767ebd695d14/src/Data/Singletons/Prelude/Show.hs#L201-L214
[2] http://hackage.haskell.org/package/ghc-typelits-extra
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Loading...