#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