Recursion on TypeNats
If you define your own type level naturals by promoting data Nat = Z | S Nat you can define data families recursively, for example data family Power :: Nat -> * -> * data instance Power Z a = PowerZ data instance Power (S n) a = PowerS a (Power n a) But if you use the built-in type level Nat, I can find no way to do the same thing. You can define a closed type family type family Power (n :: Nat) a where Power 0 a = () Power n a = (a, Power (n-1) a) but this isn't the same thing (and requires UndecidableInstances). Have I missed something? The user guide page is pretty sparse, and not up to date anyway. If not, are there plans to add a "Successor" constructor to Nat? I would have thought this was the main point of using Nat rather than Int. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
you want the following (which doesnt require undediable instances) data Nat = Z | S Nat type family U (x :: Nat) where U 0 = Z U n = S (U (n-1)) this lets you convert type lits into your own peanos or whatever hat tip to richard eisenburg for showing me this trick on the mailing list a while ago On Sat, Oct 25, 2014 at 9:53 AM, Barney Hilken wrote: > If you define your own type level naturals by promoting > > data Nat = Z | S Nat > > you can define data families recursively, for example > > data family Power :: Nat -> * -> * > data instance Power Z a = PowerZ > data instance Power (S n) a = PowerS a (Power n a) > > But if you use the built-in type level Nat, I can find no way to do the > same thing. You can define a closed type family > > type family Power (n :: Nat) a where > Power 0 a = () > Power n a = (a, Power (n-1) a) > > but this isn't the same thing (and requires UndecidableInstances). > > Have I missed something? The user guide page is pretty sparse, and not up > to date anyway. > > If not, are there plans to add a "Successor" constructor to Nat? I would > have thought this was the main point of using Nat rather than Int. > > Barney. > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
because you haven't helped write a patch change it yet :) -Carter On Sat, Oct 25, 2014 at 9:53 AM, Barney Hilken wrote: > If you define your own type level naturals by promoting > data Nat = Z | S Nat > you can define data families recursively, for example > data family Power :: Nat -> * -> * > data instance Power Z a = PowerZ > data instance Power (S n) a = PowerS a (Power n a) > But if you use the built-in type level Nat, I can find no way to do the same > thing. You can define a closed type family > type family Power (n :: Nat) a where > Power 0 a = () > Power n a = (a, Power (n-1) a) > but this isn't the same thing (and requires UndecidableInstances). > Have I missed something? The user guide page is pretty sparse, and not up to > date anyway. > If not, are there plans to add a "Successor" constructor to Nat? I would have > thought this was the main point of using Nat rather than Int. > Barney. > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
> you want the following (which doesnt require undediable instances) > > data Nat = Z | S Nat > > type family U (x :: Nat) where > U 0 = Z > U n = S (U (n-1)) > > this lets you convert type lits into your own peanos or whatever Yes, you can do that, but why should you have to? Nat is already the natural numbers, so already has this structure. Why do we have to define it again, making our code that much less clear and readable? ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
> > because you haven't helped write a patch change it yet :) > > -Carter > Would this be possible with the new type checker plugins? btw, your example gives me Nested type family application in the type family application: U (n - 1) (Use UndecidableInstances to permit this) In the equations for closed type family ‘U’ In the type family declaration for ‘U’ Failed, modules loaded: none. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
derp, my bad https://github.com/wellposed/numerical/blob/master/src/Numerical/Nat.hs has a fuller implementation of this though, that i've been using for a few months as for the plugin question, i think about adding constraint solves to the type system... so i dont know if thats quite what you want though, On Sat, Oct 25, 2014 at 2:33 PM, Barney Hilken wrote: > > > > because you haven't helped write a patch change it yet :) > > > > -Carter > > > > Would this be possible with the new type checker plugins? > > btw, your example gives me > > Nested type family application > in the type family application: U (n - 1) > (Use UndecidableInstances to permit this) > In the equations for closed type family ‘U’ > In the type family declaration for ‘U’ > Failed, modules loaded: none. > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
No, there's not another way to do this with built-in Nats, and there probably won't ever be. There are two advantages to the built-in Nats over hand-rolled ones: 1) Better syntax / error messages. 2) Built-in Nats are much more efficient than hand-rolled ones, because the hand-rolled ones are unary and take up space linear in the value of the number. If you re-hash your proposal for a Successor constructor down to the term level, it looks juts like (n+k)-patterns, which were discarded as a bad idea. The reason that the type-level numbers are natural numbers and not integers is because natural numbers have a simpler theory to solve for. I'm personally hoping for proper type-level integers at some point, and the type-checker plugins approach may make that a reality sooner than later. I hope this helps! Richard On Oct 25, 2014, at 9:53 AM, Barney Hilken wrote: > If you define your own type level naturals by promoting > > data Nat = Z | S Nat > > you can define data families recursively, for example > > data family Power :: Nat -> * -> * > data instance Power Z a = PowerZ > data instance Power (S n) a = PowerS a (Power n a) > > But if you use the built-in type level Nat, I can find no way to do the same > thing. You can define a closed type family > > type family Power (n :: Nat) a where > Power 0 a = () > Power n a = (a, Power (n-1) a) > > but this isn't the same thing (and requires UndecidableInstances). > > Have I missed something? The user guide page is pretty sparse, and not up to > date anyway. > > If not, are there plans to add a "Successor" constructor to Nat? I would have > thought this was the main point of using Nat rather than Int. > > Barney. > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
> No, there's not another way to do this with built-in Nats, and there probably > won't ever be. I do hope you're wrong. > There are two advantages to the built-in Nats over hand-rolled ones: 1) > Better syntax / error messages. 2) Built-in Nats are much more efficient than > hand-rolled ones, because the hand-rolled ones are unary and take up space > linear in the value of the number. If you re-hash your proposal for a > Successor constructor down to the term level, it looks juts like > (n+k)-patterns, which were discarded as a bad idea. (n+k) patterns are clearly a bad idea on integers, because the integers don't have the inductive structure, but they're a good idea on natural numbers, which is why they were in the language originally. > The reason that the type-level numbers are natural numbers and not integers > is because natural numbers have a simpler theory to solve for. I'm personally > hoping for proper type-level integers at some point, and the type-checker > plugins approach may make that a reality sooner than later. Type-level integers could well be useful, but they shouldn't replace type-level naturals, because they have completely different uses. At the value level, you can fudge the differences, because you can always return bottom, but at the type level you have to take correctness much more seriously if your type system is to be any use at all. The fact that Carter (and I) are forced to define hand-rolled nats on top of the built in ones demonstrates a clear need for this feature. It seems to me a valuable extension, whether the syntax uses Successor or (n+k). Why can't we combine the advantages of built-in Nats and hand-rolled ones? Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
Your argument here is compelling. I have wanted type-level integers from the beginning and saw Nats as just a step toward integers. But, of course, this is silly -- you're right that Nats deserve their own place. Perhaps make a feature request for this. It may be related to type-level pattern synonyms, as proposed in #8828, comment:2. Richard On Oct 27, 2014, at 10:39 AM, Barney Hilken wrote: >> No, there's not another way to do this with built-in Nats, and there >> probably won't ever be. > > I do hope you're wrong. > >> There are two advantages to the built-in Nats over hand-rolled ones: 1) >> Better syntax / error messages. 2) Built-in Nats are much more efficient >> than hand-rolled ones, because the hand-rolled ones are unary and take up >> space linear in the value of the number. If you re-hash your proposal for a >> Successor constructor down to the term level, it looks juts like >> (n+k)-patterns, which were discarded as a bad idea. > > (n+k) patterns are clearly a bad idea on integers, because the integers don't > have the inductive structure, but they're a good idea on natural numbers, > which is why they were in the language originally. > >> The reason that the type-level numbers are natural numbers and not integers >> is because natural numbers have a simpler theory to solve for. I'm >> personally hoping for proper type-level integers at some point, and the >> type-checker plugins approach may make that a reality sooner than later. > > Type-level integers could well be useful, but they shouldn't replace > type-level naturals, because they have completely different uses. At the > value level, you can fudge the differences, because you can always return > bottom, but at the type level you have to take correctness much more > seriously if your type system is to be any use at all. > > The fact that Carter (and I) are forced to define hand-rolled nats on top of > the built in ones demonstrates a clear need for this feature. It seems to me > a valuable extension, whether the syntax uses Successor or (n+k). Why can't > we combine the advantages of built-in Nats and hand-rolled ones? > > Barney. > > > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731 Unfortunately I don't know enough about ghc internals to try implementing it. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
Hello, actually type-level integers are easier to work with than type-level naturals (e.g., one can cancel things by subtracting at will). I agree that ideally we want to have both integers and naturals (probably as separate kinds). I just don't know what notation to use to distinguish the two. -Iavor On Mon, Oct 27, 2014 at 2:13 PM, Barney Hilken wrote: > Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731 > > Unfortunately I don't know enough about ghc internals to try implementing > it. > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
I don't think we'll need notation to differentiate: just use overloaded literals, like we do in terms. Something that would operate vaguely like this: > type family 3 :: k where > 3 :: Nat = ... -- 3 as a Nat > 3 :: Integer = ... -- 3 as an Integer I'm not at all suggesting it be implemented this way, but we already have the ability to branch in type families based on result kind, so the mechanism is already around. Unfortunately, this would be unhelpful if the user asked for (3 :: Bool), which would kind-check but be stuck. Richard On Oct 28, 2014, at 8:24 PM, Iavor Diatchki wrote: > Hello, > > actually type-level integers are easier to work with than type-level naturals > (e.g., one can cancel things by subtracting at will). I agree that ideally > we want to have both integers and naturals (probably as separate kinds). I > just don't know what notation to use to distinguish the two. > > -Iavor > > > > On Mon, Oct 27, 2014 at 2:13 PM, Barney Hilken wrote: > Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731 > > Unfortunately I don't know enough about ghc internals to try implementing it. > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
