Hi in a recent project of mine, the difference between Nat and Natural was a serious hurdle in using dependentish types, so I am in favor. (Text and Symbol was the other, so this would not have unblocked me, but still). Cheers, Joachim Am Donnerstag, den 01.10.2020, 12:02 +0200 schrieb Alejandro Serrano Mena:

Dear all, I recommend that we accept this proposal. The only problematic (read, not backwards-compatible) bit is the case of a type class having instances for both `Nat` and `Natural`, but that seems very unlikely.

Something which I thought about was whether any of `Nat` or `Natural` were implementing something akin to Peano naturals (so we could have inductive instances working on Zero and (Succ n)), both none of both do, so the alignment seems correct to me.

Regards, Alejandro

El vie., 25 sept. 2020 a las 16:06, Joachim Breitner () escribió:

...

Dear Committee,

this is your secretary speaking:

Unify Nat and Natural has been proposed by Richard https://github.com/ghc-proposals/ghc-proposals/pull/364 https://github.com/goldfirere/ghc-proposals/blob/natural/proposals/0000-unif...

I’ll propose Alejandro as the shepherd.

Please guide us to a conclusion as outlined in https://github.com/ghc-proposals/ghc-proposals#committee-process

Thanks, Joachim _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

I fail to find a downside as well. I would still like to insist on the motivation section to feature an illustrative example before we merge the proposal, though. But the rest is good with me. On Thu, Oct 1, 2020 at 12:11 PM Simon Peyton Jones via ghc-steering-committee wrote:

Aye. Tidies this up, and I see no downside.

Simon

*From:* ghc-steering-committee *On Behalf Of *Alejandro Serrano Mena *Sent:* 01 October 2020 11:02 *To:* Joachim Breitner *Cc:* ghc-steering-committee@haskell.org *Subject:* [ghc-steering-committee] #364: Unify Nat and Natural, recommendation: accept

Dear all,

I recommend that we accept this proposal. The only problematic (read, not backwards-compatible) bit is the case of a type class having instances for both `Nat` and `Natural`, but that seems very unlikely.

Something which I thought about was whether any of `Nat` or `Natural` were implementing something akin to Peano naturals (so we could have inductive instances working on Zero and (Succ n)), both none of both do, so the alignment seems correct to me.

Regards,

Alejandro

El vie., 25 sept. 2020 a las 16:06, Joachim Breitner (< mail@joachim-breitner.de>) escribió:

Dear Committee,

this is your secretary speaking:

Unify Nat and Natural has been proposed by Richard https://github.com/ghc-proposals/ghc-proposals/pull/364 https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F364&data=02%7C01%7Csimonpj%40microsoft.com%7Ccf838f8219a74bf4c26608d865f11f20%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637371434494036876&sdata=JSTuh5g4KrmxgwJRsQ9m8QXa0TnGxGVr%2FZUrbK7a%2FLA%3D&reserved=0

https://github.com/goldfirere/ghc-proposals/blob/natural/proposals/0000-unif... https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fnatural%2Fproposals%2F0000-unify-natural.rst&data=02%7C01%7Csimonpj%40microsoft.com%7Ccf838f8219a74bf4c26608d865f11f20%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637371434494036876&sdata=KYno%2B%2FA4WGYaDt5oV5VxCH7vWDn2QAU%2FSUjyR%2FZ6Yao%3D&reserved=0

I’ll propose Alejandro as the shepherd.

Please guide us to a conclusion as outlined in https://github.com/ghc-proposals/ghc-proposals#committee-process https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%23committee-process&data=02%7C01%7Csimonpj%40microsoft.com%7Ccf838f8219a74bf4c26608d865f11f20%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637371434494036876&sdata=%2F%2BKk8v8%2Fe6W15doiLm0Z2FM0BaL0KVtUlwZZlzws9sM%3D&reserved=0

Thanks, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/ https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ccf838f8219a74bf4c26608d865f11f20%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637371434494046841&sdata=JejYCscHAtZenQNNO0vru0WP%2BCPIPEo3%2Bj%2Fq76wJKMI%3D&reserved=0

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&data=02%7C01%7Csimonpj%40microsoft.com%7Ccf838f8219a74bf4c26608d865f11f20%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637371434494046841&sdata=KMmToVSXLW9cGxucsfLoELO8Eda6YakAKtZDk%2BAnSzU%3D&reserved=0

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi, Am Donnerstag, den 01.10.2020, 09:14 -0700 schrieb Iavor Diatchki:

Joachim, I'd be curious to see an example of the hurdle you run into, if there is a simple example illustrating it.

I wanted to use a datatype (that describes an typed AST) both as values (where I needed Text or String) and as types (where needed Symbol). I resorted to a hack like data FieldName = N Symbol -- ^ a properly named field | N' T.Text -- ^ Use this in terms (usually not needed) | H Nat -- ^ a field hash. Should fit in 32 bit. Also used for tuples | H' Word32 -- ^ Use this in terms (mostly internal) data SFieldName (n :: FieldName) where SN :: KnownSymbol s => Proxy s -> SFieldName ('N s) SH :: KnownNat n => Proxy n -> SFieldName ('H n) fromSFieldName :: SFieldName n -> FieldName fromSFieldName (SN p) = N' (T.pack (symbolVal p)) fromSFieldName (SH p) = H' (fromIntegral (natVal p)) class Typeable fn => KnownFieldName (fn :: FieldName) where fieldName :: SFieldName fn instance KnownSymbol s => KnownFieldName ('N s) where fieldName = SN (Proxy @s) instance KnownNat s => KnownFieldName ('H s) where fieldName = SH (Proxy @s) Fullcode at https://github.com/nomeata/haskell-candid/blob/2feb0cdbdbfa74f3e4373066b1d58... Eventually I just used less type-level computation (and otherwise greatly restructued that code, so don’t worry too much about helping here). Maybe using a library like singleton might have made that easier, or maybe there are tricks that I missed, and I did it all wrong. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Hi, I support the recommendation to accept this proposal. Vitaly чт, 1 окт. 2020 г. в 13:02, Alejandro Serrano Mena :

Dear all, I recommend that we accept this proposal. The only problematic (read, not backwards-compatible) bit is the case of a type class having instances for both `Nat` and `Natural`, but that seems very unlikely.

Something which I thought about was whether any of `Nat` or `Natural` were implementing something akin to Peano naturals (so we could have inductive instances working on Zero and (Succ n)), both none of both do, so the alignment seems correct to me.

Regards, Alejandro

El vie., 25 sept. 2020 a las 16:06, Joachim Breitner (< mail@joachim-breitner.de>) escribió:

...

Dear Committee,

this is your secretary speaking:

Unify Nat and Natural has been proposed by Richard https://github.com/ghc-proposals/ghc-proposals/pull/364

https://github.com/goldfirere/ghc-proposals/blob/natural/proposals/0000-unif...

I’ll propose Alejandro as the shepherd.

Please guide us to a conclusion as outlined in https://github.com/ghc-proposals/ghc-proposals#committee-process

Thanks, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee