New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

GCD of constants #1

Closed
dmcclean opened this Issue May 10, 2015 · 19 comments

Comments

Projects
None yet
3 participants
@dmcclean

dmcclean commented May 10, 2015

This library is pretty awesome, nicely done!

It would be awesome if it could solve GCDs, when both arguments are constants of course. Cases with one variable seem totally intractable, unless maybe the constant argument is 1 (and the possibility that the variable will end up being 0 means probably not even then).

This would help error messages and probably performance in my (unreleased, yet) library for type level rationals.

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb May 10, 2015

Contributor

Thanks for the praise. Could you elaborate in more details what kind of equalities the plugin should be able to solve? Adding more operations to the normal form will be difficult.

Contributor

christiaanb commented May 10, 2015

Thanks for the praise. Could you elaborate in more details what kind of equalities the plugin should be able to solve? Adding more operations to the normal form will be difficult.

@dmcclean

This comment has been minimized.

Show comment
Hide comment
@dmcclean

dmcclean May 10, 2015

Does it only have a chance through GHCs API to solve a ~ b style equations, or can it also simplify type family applications?

I was hoping it could simplify GCD 360 24 to 24 when it noticed that GCD was fully applied to literals or things like 3+2 (and not to type expressions involving type variables).

As such I'm not sure it is really related to the normal form, which is meant to help solve equations that do involve variables.

dmcclean commented May 10, 2015

Does it only have a chance through GHCs API to solve a ~ b style equations, or can it also simplify type family applications?

I was hoping it could simplify GCD 360 24 to 24 when it noticed that GCD was fully applied to literals or things like 3+2 (and not to type expressions involving type variables).

As such I'm not sure it is really related to the normal form, which is meant to help solve equations that do involve variables.

@dmcclean

This comment has been minimized.

Show comment
Hide comment
@dmcclean

dmcclean May 10, 2015

So in a sense it is simulating a type family, GCD, that is very tough to write instances for in haskell (or at least I haven't succeeded in figuring out how to write Euclid's algorithm as a closed type family) and that has an infinite number of instances if you only write literal instances.

dmcclean commented May 10, 2015

So in a sense it is simulating a type family, GCD, that is very tough to write instances for in haskell (or at least I haven't succeeded in figuring out how to write Euclid's algorithm as a closed type family) and that has an infinite number of instances if you only write literal instances.

@dmcclean

This comment has been minimized.

Show comment
Hide comment
@dmcclean

dmcclean May 10, 2015

I just had a brainstorm that perhaps I could write a time-limited version of Euclid's algorithm as a closed type family, using only expressions that your solver can already solve. I would have GCD a b be a type synonym for GCD' 100 a b where GCD' expands a single step of the algorithm and calls itself decrementing n until n reaches zero? This deals with the problem of not being able to branch on when the remainder becomes 0, and it works because you can keep adding more and more needless 0 steps at the end without changing the result.

For my target use case I only necessarily need a conservative approximation to the true GCD, and so having a modest finite limit on the number of rounds wouldn't really hurt me?

Do you think that has a chance?

Perhaps not, because as wikipedia says "The final nonzero remainder r is the greatest common divisor of a and b." which I don't see how you can pick that out until after your solver does its thing.

dmcclean commented May 10, 2015

I just had a brainstorm that perhaps I could write a time-limited version of Euclid's algorithm as a closed type family, using only expressions that your solver can already solve. I would have GCD a b be a type synonym for GCD' 100 a b where GCD' expands a single step of the algorithm and calls itself decrementing n until n reaches zero? This deals with the problem of not being able to branch on when the remainder becomes 0, and it works because you can keep adding more and more needless 0 steps at the end without changing the result.

For my target use case I only necessarily need a conservative approximation to the true GCD, and so having a modest finite limit on the number of rounds wouldn't really hurt me?

Do you think that has a chance?

Perhaps not, because as wikipedia says "The final nonzero remainder r is the greatest common divisor of a and b." which I don't see how you can pick that out until after your solver does its thing.

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb May 10, 2015

Contributor

Ah, so basically what you want to have is an empty closed type family GCD for which the plugin can prove equalities 'GCD x y ~ z".

Sadly, I don't think empty closed type families are possible in GHC 7.10.1; they are in HEAD and hopefully also in 7.10.2. The second part is definately possible, though it is easiest and probably best if the GCD function is then also defined as part of the same package. I'm not exactly sure, however, whether this package should become an assortment of type-level functions and their custom solvers.

Contributor

christiaanb commented May 10, 2015

Ah, so basically what you want to have is an empty closed type family GCD for which the plugin can prove equalities 'GCD x y ~ z".

Sadly, I don't think empty closed type families are possible in GHC 7.10.1; they are in HEAD and hopefully also in 7.10.2. The second part is definately possible, though it is easiest and probably best if the GCD function is then also defined as part of the same package. I'm not exactly sure, however, whether this package should become an assortment of type-level functions and their custom solvers.

@dmcclean

This comment has been minimized.

Show comment
Hide comment
@dmcclean

dmcclean May 10, 2015

Could the lack of syntactically empty closed type families (which, I just checked, aren't allowed by 7.10.1) be evaded by giving one case?

This one is syntactically valid today, but I don't know if the fact that it isn't empty ruins the next step somehow?

type family GCD (a :: Nat) (b :: Nat) :: Nat where
  GCD 1 1 = 1

If I could lobby for and write a patch for adding the type family to GHC.TypeLits? Might also be of use to some crypto people or something.

dmcclean commented May 10, 2015

Could the lack of syntactically empty closed type families (which, I just checked, aren't allowed by 7.10.1) be evaded by giving one case?

This one is syntactically valid today, but I don't know if the fact that it isn't empty ruins the next step somehow?

type family GCD (a :: Nat) (b :: Nat) :: Nat where
  GCD 1 1 = 1

If I could lobby for and write a patch for adding the type family to GHC.TypeLits? Might also be of use to some crypto people or something.

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb May 10, 2015

Contributor

I guess you could leave the type family open as Adam does in his units of measure plugin at https://github.com/adamgundry/uom-plugin

I don't see a reason to add GCD to the base library. What is wrong to add it in a separate package? Something like ghc-typelits-extra, where we can add a myriad of type functions operating on kind Nat: GCD, LCM, log (both a ceiling and a flooring version), etc.

Contributor

christiaanb commented May 10, 2015

I guess you could leave the type family open as Adam does in his units of measure plugin at https://github.com/adamgundry/uom-plugin

I don't see a reason to add GCD to the base library. What is wrong to add it in a separate package? Something like ghc-typelits-extra, where we can add a myriad of type functions operating on kind Nat: GCD, LCM, log (both a ceiling and a flooring version), etc.

@dmcclean

This comment has been minimized.

Show comment
Hide comment
@dmcclean

dmcclean May 10, 2015

OK, good call. But then I need to figure out how to make my own solver, and how to get the two to interact so that they can ping pong. I need to do some reading.

Adam's work is nice. I'm biased but I think Bjorn Buckwalter and I might be on a more promising track for that with https://github.com/bjornbm/dimensional-dk. You get almost all the same functionality without needing a solver at all, only our linear algebra follow-on package needs a solver for abelian group unification (in the group of dimensions) to be maximally useful.

dmcclean commented May 10, 2015

OK, good call. But then I need to figure out how to make my own solver, and how to get the two to interact so that they can ping pong. I need to do some reading.

Adam's work is nice. I'm biased but I think Bjorn Buckwalter and I might be on a more promising track for that with https://github.com/bjornbm/dimensional-dk. You get almost all the same functionality without needing a solver at all, only our linear algebra follow-on package needs a solver for abelian group unification (in the group of dimensions) to be maximally useful.

@dmcclean

This comment has been minimized.

Show comment
Hide comment
@dmcclean

dmcclean May 10, 2015

(The arithmetic type families in GHC.TypeLits in 7.10 / base 4.8 are open too.)

dmcclean commented May 10, 2015

(The arithmetic type families in GHC.TypeLits in 7.10 / base 4.8 are open too.)

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb May 10, 2015

Contributor

I'm willing to (help) set up a new package containing the type-level operations and respective solvers. With regards to interactions: interactions between which two solvers? The ghc-typelits-extra and ghc-typelits-natnormailse? Or ghc-typelits-extras and your type-level rationals?
Anyhow, how it should work is that the one solver just assumes "GCD x y ~ z" is true when solving its own constraint and then at the end just add this constraint to the solver pipeline. It will then later be picked up by the GCD solver which either agrees or doesn't depending on whether "GCD x y" is really equal to 'z'.

Contributor

christiaanb commented May 10, 2015

I'm willing to (help) set up a new package containing the type-level operations and respective solvers. With regards to interactions: interactions between which two solvers? The ghc-typelits-extra and ghc-typelits-natnormailse? Or ghc-typelits-extras and your type-level rationals?
Anyhow, how it should work is that the one solver just assumes "GCD x y ~ z" is true when solving its own constraint and then at the end just add this constraint to the solver pipeline. It will then later be picked up by the GCD solver which either agrees or doesn't depending on whether "GCD x y" is really equal to 'z'.

@dmcclean

This comment has been minimized.

Show comment
Hide comment
@dmcclean

dmcclean May 11, 2015

Awesome, thanks! 😄 I will get all the preliminaries setup.
Would you object if I roll it in with the existing package numtype-dk which just went on hackage? It's got type-level integers and would be expanding to cover type-level rationals as well.

I'm still a bit confused about the interaction, because it seems to me that ghc-typelits-extras and ghc-typelits-natnormalise can both potentially benefit from information supplied by the other, so it isn't clear which to run first, and you might ideally want some sort of iterate-until-no-more-changes plan?

dmcclean commented May 11, 2015

Awesome, thanks! 😄 I will get all the preliminaries setup.
Would you object if I roll it in with the existing package numtype-dk which just went on hackage? It's got type-level integers and would be expanding to cover type-level rationals as well.

I'm still a bit confused about the interaction, because it seems to me that ghc-typelits-extras and ghc-typelits-natnormalise can both potentially benefit from information supplied by the other, so it isn't clear which to run first, and you might ideally want some sort of iterate-until-no-more-changes plan?

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb May 11, 2015

Contributor

Yeah sure, I wouldn't mind providing patches against your package instead of creating a new one.

With regards to interaction. It is my understanding of the ghc solver pipeline that it's default behavior is to run until nothing changes. I'll do some experiments

Contributor

christiaanb commented May 11, 2015

Yeah sure, I wouldn't mind providing patches against your package instead of creating a new one.

With regards to interaction. It is my understanding of the ghc solver pipeline that it's default behavior is to run until nothing changes. I'll do some experiments

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb May 17, 2015

Contributor

@dmcclean I just push an initial version of the solver at: https://github.com/christiaanb/ghc-typelits-extra

I've only tested it with: https://github.com/christiaanb/ghc-typelits-extra/blob/master/tests/Main.hs

Let me know how you would want to integrate this solver in your package. And could you maybe make a pull-request to update the tests/Main.hs with additional tests that are needed for your use case?

Contributor

christiaanb commented May 17, 2015

@dmcclean I just push an initial version of the solver at: https://github.com/christiaanb/ghc-typelits-extra

I've only tested it with: https://github.com/christiaanb/ghc-typelits-extra/blob/master/tests/Main.hs

Let me know how you would want to integrate this solver in your package. And could you maybe make a pull-request to update the tests/Main.hs with additional tests that are needed for your use case?

@adamgundry

This comment has been minimized.

Show comment
Hide comment
@adamgundry

adamgundry May 29, 2015

A scattering of thoughts, as I've just come upon this issue:

  • GCD should probably be an empty closed type family, but giving it one equation that is consistent with its plugin-defined behaviour should also work fine. Open type families (as in uom-plugin) are not really safe, because the user might define family instances that are inconsistent with the plugin.
  • We're discussing better support for defining type families in plugins. It should really be possible to define GCD more directly than by solving equations of the form GCD x y ~ z.
  • In principle, the plugin solver pipeline is indeed designed to permit multiple plugins to cooperate by iteration, but this isn't very well tested yet. I've tried to explain it to some extent in this paper. Feedback on how well this works in practice is very welcome!

adamgundry commented May 29, 2015

A scattering of thoughts, as I've just come upon this issue:

  • GCD should probably be an empty closed type family, but giving it one equation that is consistent with its plugin-defined behaviour should also work fine. Open type families (as in uom-plugin) are not really safe, because the user might define family instances that are inconsistent with the plugin.
  • We're discussing better support for defining type families in plugins. It should really be possible to define GCD more directly than by solving equations of the form GCD x y ~ z.
  • In principle, the plugin solver pipeline is indeed designed to permit multiple plugins to cooperate by iteration, but this isn't very well tested yet. I've tried to explain it to some extent in this paper. Feedback on how well this works in practice is very welcome!
@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb May 29, 2015

Contributor

With regards to interacting plugins:

Suppose I have:

[W] GCD 6 8 + x ~ x + GCD 6 9

What I would like for ghc-typelits-natnormalise to be able to do is create the EvTerm

EvCoercion (TcCoercion (AxiomRuleCo "plusCommutesCo" [x] [CoVarCo gcdEvVar]))

Where "plusCommutesCo" is the proof the that (x + co ~ co + x), given that co is a proven constraint, and gcdEvVar is the EvVar of the [W]anted constraint I discharge. So ghc-typelits-natnormalise would return:

TcPluginOK [(EvCoercion (TcCoercion (AxiomRuleCo "plusCommutesCo" [x] [CoVarCo gcdEvVar])), [W] GCD 6 8 + x ~ x + GCD 6 9)] [[W] GCD 6 8 ~ GCD 6 9]

Then I let the the constraint solver do it's thing: let another plugin try to solve the new wanted. ghc-typelits-natnormalise doesn't care which plugin that is. It has produced its conditional evidence. Now ghc-typelits-extra comes along and disproves [W] GCD 6 8 ~ GCD 6 9 and everything would fail as intented.

However, as CoAxiomRule is currently not serialisable, I'm forced to use UnivCo instead of AxiomRuleCo, meaning there is no way to generate conditional evidence as far as I can see. So yes, I think in theory plugins should be able to cooperate by iteration, but currently not in practice.

Contributor

christiaanb commented May 29, 2015

With regards to interacting plugins:

Suppose I have:

[W] GCD 6 8 + x ~ x + GCD 6 9

What I would like for ghc-typelits-natnormalise to be able to do is create the EvTerm

EvCoercion (TcCoercion (AxiomRuleCo "plusCommutesCo" [x] [CoVarCo gcdEvVar]))

Where "plusCommutesCo" is the proof the that (x + co ~ co + x), given that co is a proven constraint, and gcdEvVar is the EvVar of the [W]anted constraint I discharge. So ghc-typelits-natnormalise would return:

TcPluginOK [(EvCoercion (TcCoercion (AxiomRuleCo "plusCommutesCo" [x] [CoVarCo gcdEvVar])), [W] GCD 6 8 + x ~ x + GCD 6 9)] [[W] GCD 6 8 ~ GCD 6 9]

Then I let the the constraint solver do it's thing: let another plugin try to solve the new wanted. ghc-typelits-natnormalise doesn't care which plugin that is. It has produced its conditional evidence. Now ghc-typelits-extra comes along and disproves [W] GCD 6 8 ~ GCD 6 9 and everything would fail as intented.

However, as CoAxiomRule is currently not serialisable, I'm forced to use UnivCo instead of AxiomRuleCo, meaning there is no way to generate conditional evidence as far as I can see. So yes, I think in theory plugins should be able to cooperate by iteration, but currently not in practice.

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb May 29, 2015

Contributor

@adamgundry As you probably know from our email discussion on interacting plugins: being unable to generate this conditional evidence, I've added newWantedWithProvenance and failWithProvenace in the yet-to-be-releaded ghc-tcplugins-extra package.

Those two function together implement the hack to bring down a stack of conditional evidence implemented in terms of UnivCo by tracking the provenance of discharged [W]anted constraints.

Contributor

christiaanb commented May 29, 2015

@adamgundry As you probably know from our email discussion on interacting plugins: being unable to generate this conditional evidence, I've added newWantedWithProvenance and failWithProvenace in the yet-to-be-releaded ghc-tcplugins-extra package.

Those two function together implement the hack to bring down a stack of conditional evidence implemented in terms of UnivCo by tracking the provenance of discharged [W]anted constraints.

@adamgundry

This comment has been minimized.

Show comment
Hide comment
@adamgundry

adamgundry Jun 1, 2015

@christiaanb thanks for clearly explaining how the forms of evidence you can generate affect interaction between multiple plugins. I hadn't appreciated this before.

Thinking about this some more, can't you prove GCD 6 8 + x ~ x + GCD 6 9 by doing something like this (apologies for made-up notation)?

g1 :: GCD 6 8 + x ~ x + GCD 6 8
g1 = mkUnivCo "commutativity" Nominal (forall x y . y + x) (forall x y . x + y)
        `mkInstCo` x `mkInstCo` (GCD 6 8)

gcdEvVar :: GCD 6 8 ~ GCD 6 9

g2 :: x + GCD 6 8 ~ x + GCD 6 9
g2 = mkTyConAppCo Nominal (+) (mkReflCo Nominal x) (mkCoVarCo gcdEvVar)

g3 :: GCD 6 8 + x ~ x + GCD 6 9
g3 = g1 `mkTransCo` g2

That is, I think UnivCo can be used to simulate axioms like commutativity, which don't really have any premises. Of course, one might well want to go beyond this... Also, I'm not sure whether the Coercion/TcCoercion distinction gets in the way, as TcCoercion doesn't seem to have coercion instantiation.

adamgundry commented Jun 1, 2015

@christiaanb thanks for clearly explaining how the forms of evidence you can generate affect interaction between multiple plugins. I hadn't appreciated this before.

Thinking about this some more, can't you prove GCD 6 8 + x ~ x + GCD 6 9 by doing something like this (apologies for made-up notation)?

g1 :: GCD 6 8 + x ~ x + GCD 6 8
g1 = mkUnivCo "commutativity" Nominal (forall x y . y + x) (forall x y . x + y)
        `mkInstCo` x `mkInstCo` (GCD 6 8)

gcdEvVar :: GCD 6 8 ~ GCD 6 9

g2 :: x + GCD 6 8 ~ x + GCD 6 9
g2 = mkTyConAppCo Nominal (+) (mkReflCo Nominal x) (mkCoVarCo gcdEvVar)

g3 :: GCD 6 8 + x ~ x + GCD 6 9
g3 = g1 `mkTransCo` g2

That is, I think UnivCo can be used to simulate axioms like commutativity, which don't really have any premises. Of course, one might well want to go beyond this... Also, I'm not sure whether the Coercion/TcCoercion distinction gets in the way, as TcCoercion doesn't seem to have coercion instantiation.

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb Jun 1, 2015

Contributor

@adamgundry Thanks for that suggestion, I'll try it out tomorrow. I hadn't thought of using UnivCo to create a coercion of quantified types.

Contributor

christiaanb commented Jun 1, 2015

@adamgundry Thanks for that suggestion, I'll try it out tomorrow. I hadn't thought of using UnivCo to create a coercion of quantified types.

@christiaanb

This comment has been minimized.

Show comment
Hide comment
@christiaanb

christiaanb Jan 22, 2016

Contributor

As shown by @Bodigrim on reddit, we can just implement GCD with the tools already available to us in GHC.TypeLits:

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy
import GHC.TypeLits

type family Cmp123 (o :: Ordering) (x :: Nat) (y :: Nat) (z :: Nat) :: Nat where
  Cmp123 LT x y z = x
  Cmp123 EQ x y z = y
  Cmp123 GT x y z = z

type family GCD (x :: Nat) (y :: Nat) :: Nat where
  GCD 0 x = x
  GCD x 0 = x
  GCD x y = Cmp123 (CmpNat x y) (GCD x (y - x)) x (GCD (x - y) y)

test :: Proxy (GCD 372 48) -> Proxy 12
test = id

I guess that means we can close this issue.

Contributor

christiaanb commented Jan 22, 2016

As shown by @Bodigrim on reddit, we can just implement GCD with the tools already available to us in GHC.TypeLits:

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy
import GHC.TypeLits

type family Cmp123 (o :: Ordering) (x :: Nat) (y :: Nat) (z :: Nat) :: Nat where
  Cmp123 LT x y z = x
  Cmp123 EQ x y z = y
  Cmp123 GT x y z = z

type family GCD (x :: Nat) (y :: Nat) :: Nat where
  GCD 0 x = x
  GCD x 0 = x
  GCD x y = Cmp123 (CmpNat x y) (GCD x (y - x)) x (GCD (x - y) y)

test :: Proxy (GCD 372 48) -> Proxy 12
test = id

I guess that means we can close this issue.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment