Proposal for removing separate `Nat` in favour of promoted `Natural` type.

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Proposal for removing separate `Nat` in favour of promoted `Natural` type.

Rinat Stryungis
Hello, libraries!

I want to present a proposal for changes in the `Base` library.
The changes in my proposal partially solve the following issue:
    https://gitlab.haskell.org/ghc/ghc/-/issues/10776
and remove the separate built-in kind `Nat` in favor of promoted type `Natural`.

It means that previously one can't directly promote a data type with Natural fields:

    data MyPointN = PointN Natural Natural -- could not be promoted
    data MyPointP = PointP Nat Nat         -- could be promoted, but uninhabited in terms

    type M = PointP 1 10  

but now one could promote the `Natural` data type:

    data MyPoint = Point Natural Natural
    type MyTLPoint1 = Point 1 10

The proposed changes both simplify the internals of the GHC by removing
separate kind and related things and make using of the type-level
naturals more convenient for users.

Also new type synonym

    type Nat = Natural

appeared in the Data.Type.TypeNats in the name of backward compatibility.

I've opened a new MR with the patch. In the patch with the already implemented promotion of Naturals, one could find new and updated tests and docs.

Also, I want to say about the breakages:  

1. One must enable `TypeSynonymInstances` in order to define instances for `Nat`.
2. Different instances for `Nat` and `Natural` won't type check anymore.
3. Type checker plugins that work with the natural numbers now
   should use `naturalTy` kind instead of removed `typeNatKind`

Anyone interested is welcome to look at the MR and discuss the proposal and its implementation.

https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583

The latter is very short and easy, thanks to the recently merged patch with a new `ghc-bignum` library. It greatly simplified my work.

Thanks and best regards.
Rinat Stryungis. 

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

Re: Proposal for removing separate `Nat` in favour of promoted `Natural` type.

Oleg Grenrus

There is an old GHC issue https://gitlab.haskell.org/ghc/ghc/-/issues/10776 which got recently a PR https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583

- Oleg

On 9.7.2020 12.59, Rinat Stryungis wrote:
Hello, libraries!

I want to present a proposal for changes in the `Base` library.
The changes in my proposal partially solve the following issue:
    https://gitlab.haskell.org/ghc/ghc/-/issues/10776
and remove the separate built-in kind `Nat` in favor of promoted type `Natural`.

It means that previously one can't directly promote a data type with Natural fields:

    data MyPointN = PointN Natural Natural -- could not be promoted
    data MyPointP = PointP Nat Nat         -- could be promoted, but uninhabited in terms

    type M = PointP 1 10  

but now one could promote the `Natural` data type:

    data MyPoint = Point Natural Natural
    type MyTLPoint1 = Point 1 10

The proposed changes both simplify the internals of the GHC by removing
separate kind and related things and make using of the type-level
naturals more convenient for users.

Also new type synonym

    type Nat = Natural

appeared in the Data.Type.TypeNats in the name of backward compatibility.

I've opened a new MR with the patch. In the patch with the already implemented promotion of Naturals, one could find new and updated tests and docs.

Also, I want to say about the breakages:  

1. One must enable `TypeSynonymInstances` in order to define instances for `Nat`.
2. Different instances for `Nat` and `Natural` won't type check anymore.
3. Type checker plugins that work with the natural numbers now
   should use `naturalTy` kind instead of removed `typeNatKind`

Anyone interested is welcome to look at the MR and discuss the proposal and its implementation.

https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583

The latter is very short and easy, thanks to the recently merged patch with a new `ghc-bignum` library. It greatly simplified my work.

Thanks and best regards.
Rinat Stryungis. 

_______________________________________________
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
|

Re: Proposal for removing separate `Nat` in favour of promoted `Natural` type.

Oleg Grenrus

I should have read the whole email before replying... Sorry for the noise.

On 9.7.2020 15.09, Oleg Grenrus wrote:

There is an old GHC issue https://gitlab.haskell.org/ghc/ghc/-/issues/10776 which got recently a PR https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583

- Oleg

On 9.7.2020 12.59, Rinat Stryungis wrote:
Hello, libraries!

I want to present a proposal for changes in the `Base` library.
The changes in my proposal partially solve the following issue:
    https://gitlab.haskell.org/ghc/ghc/-/issues/10776
and remove the separate built-in kind `Nat` in favor of promoted type `Natural`.

It means that previously one can't directly promote a data type with Natural fields:

    data MyPointN = PointN Natural Natural -- could not be promoted
    data MyPointP = PointP Nat Nat         -- could be promoted, but uninhabited in terms

    type M = PointP 1 10  

but now one could promote the `Natural` data type:

    data MyPoint = Point Natural Natural
    type MyTLPoint1 = Point 1 10

The proposed changes both simplify the internals of the GHC by removing
separate kind and related things and make using of the type-level
naturals more convenient for users.

Also new type synonym

    type Nat = Natural

appeared in the Data.Type.TypeNats in the name of backward compatibility.

I've opened a new MR with the patch. In the patch with the already implemented promotion of Naturals, one could find new and updated tests and docs.

Also, I want to say about the breakages:  

1. One must enable `TypeSynonymInstances` in order to define instances for `Nat`.
2. Different instances for `Nat` and `Natural` won't type check anymore.
3. Type checker plugins that work with the natural numbers now
   should use `naturalTy` kind instead of removed `typeNatKind`

Anyone interested is welcome to look at the MR and discuss the proposal and its implementation.

https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3583

The latter is very short and easy, thanks to the recently merged patch with a new `ghc-bignum` library. It greatly simplified my work.

Thanks and best regards.
Rinat Stryungis. 

_______________________________________________
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

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