Recursion on TypeNats
Locked
 
|
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 [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
|
|
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 <[hidden email]> wrote: If you define your own type level naturals by promoting _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
|
|
In reply to this post by Barney Hilken
because you haven't helped write a patch change it yet :) -Carter On Sat, Oct 25, 2014 at 9:53 AM, Barney Hilken <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
|
|
In reply to this post by Carter Schonwald
> 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 [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
|
|
In reply to this post by Carter Schonwald
>
> 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 [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
|
|
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 <[hidden email]> wrote: > _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Re: Recursion on TypeNats
|
|
In reply to this post by Barney Hilken
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 <[hidden email]> 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
|
|
> 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 [hidden email] 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 <[hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
|
|
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 [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
|
|
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 <[hidden email]> wrote: Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731 _______________________________________________ Glasgow-haskell-users mailing list [hidden email] 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:
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 <[hidden email]> wrote:
_______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
«
Return to Haskell - Glasgow-haskell-users
|
1 view|%1 views
| Free forum by Nabble | Edit this page |