Inductive type definitions on Nat
If you define your own type-level natural numbers by promoting
data Nat = Zero | Successor Nat
you can then define both data and type families inductively, for example
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
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.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.3 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |