Libraries

Download

libraries@haskell.org

July 2020

12 participants
12 discussions

Proposal for removing separate `Nat` in favour of promoted `Natural` type.
by Rinat Stryungis 09 Jul '20

09 Jul '20

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.

2 2

Proposal: k ~ l => IsLabel k (Proxy l)
by Fumiaki Kinoshita 07 Jul '20

07 Jul '20

I propose adding an IsLabel instance to Proxy where fromLabel = Proxy This is the only reasonable instance I can think of, and AFAIK there's no plan which would conflict [0]. The proposed instance allows us to explore API designs involving type-level strings with much less syntactic noise ( #foo is easier to type than @"foo"). I admit that the motivation is weak, but I think it's nice to have. [0] https://gitlab.haskell.org/ghc/ghc/-/wikis/records/overloaded-record-fields…

2 1