[GHC] #9731: Inductive type definitions on Nat

27 Oct 2014

      #9731: Inductive type definitions on Nat
-------------------------------------+-------------------------------------
       Reporter:  barney             |                   Owner:
           Type:  feature request    |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler           |                 Version:  7.8.3
       Keywords:                     |        Operating System:
   Architecture:  Unknown/Multiple   |  Unknown/Multiple
     Difficulty:  Unknown            |         Type of failure:
     Blocked By:                     |  None/Unknown
Related Tickets:                     |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 If you define your own type-level natural numbers by promoting
 {{{#!hs
 data Nat = Zero | Successor Nat
 }}}
 you can then define both data and type families inductively, for example
 {{{#!hs
 data family Vector1 :: Nat -> * -> *
 data instance Vector1 Zero a = EmptyVector
 data instance Vector1 (Successor n) a = MkVector a (Vector1 n a)
 }}}
 Using the built-in Nat, there is no way to define inductive data families,
 and inductive type families such as
 {{{#!hs
 type family Vector2 :: Nat -> * -> * where
     Vector2 0 a = ()
     Vector2 n a = (a, (Vector2 (n-1) a))
 }}}
 require UndecidableInstances (and must be closed).

 This proposal is to add (n+k) patterns for Nat, so that the built-in
 naturals can be used in the same way that the user defined naturals can,
 to define type and data families inductively.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9731
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler