#14922: Add inductively-defined Nat to base -------------------------------------+------------------------------------- Reporter: chessai | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.2.2 Resolution: | Keywords: base Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by chessai: Old description:

The proposed addition is simple, add the following to base:

{{{#!hs data Nat = Zero | Succ Nat }}}

I will list the pros/cons I see below.

Pros: - Commonly defined throughout many packages, e.g. vinyl - The inductive definition of 'Nat' is useful for correctness (e.g. {{{#!hs safeHead :: Vec a (S n) -> a; safeHead (Cons a as) = a}}})

Cons: - '-XDependentHaskell' will most likely obviate any benefit brought about by type families involving Nat - Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange.

I am open to criticism concerning the usefulness of the idea or if anyone sees a Pro(s)/Con(s) that I am missing.

New description: The proposed addition is simple, add the following to base: {{{#!hs data Nat = Zero | Succ Nat }}} I will list the pros/cons I see below. Pros: - Commonly defined throughout many packages, e.g. vinyl - The inductive definition of 'Nat' is useful for correctness (e.g. {{{safeHead :: Vec a (S n) -> a; safeHead (Cons a as) = a}}}) Cons: - '-XDependentHaskell' will most likely obviate any benefit brought about by type families involving Nat - Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange. I am open to criticism concerning the usefulness of the idea or if anyone sees a Pro(s)/Con(s) that I am missing. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14922#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14922: Add inductively-defined Nat to base -------------------------------------+------------------------------------- Reporter: chessai | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: libraries/base | Version: 8.2.2 Resolution: | Keywords: base Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This is a feature request to add something to a core library, and as such, you should run this by the [https://mail.haskell.org/mailman/listinfo/libraries libraries mailing list] first to ensure that there is community consensus to do this. It's worth noting that there have been previous proposals for this in the past, one of which is [https://mail.haskell.org/pipermail/libraries/2016-January/026537.html this one] (from January 2016). That one ended with the consensus that this should //not// be added to `base`. Still, if you feel strongly otherwise, it might be worth bringing this up again—it's possible that public opinion has shifted since then. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14922#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler