Recursion on TypeNats

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
12 messages Options
Reply | Threaded
Open this post in threaded view
|

Recursion on TypeNats

Barney Hilken
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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

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

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

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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Carter Schonwald
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:

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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Barney Hilken
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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Barney Hilken
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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Carter Schonwald
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:
>
> 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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Richard Eisenberg-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Barney Hilken
> 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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Richard Eisenberg-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Barney Hilken
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
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Iavor Diatchki
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

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


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Recursion on TypeNats

Richard Eisenberg-2
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 <[hidden email]> 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 <[hidden email]> 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
[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