type-unary-0.2.19: Type-level and typed unary natural numbers, inequality proofs, vectors

Copyright(c) Conal Elliott 2009
LicenseBSD3
Maintainerconal@conal.net
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell98

TypeUnary.TyNat

Contents

Description

Type-level unary natural numbers

Synopsis

Type-level natural numbers

data Z Source

Type-level representation of zero

Instances

IsNat Z 
Typeable * Z 
Newtype (Vec Z a) () 
type n :-: Z = n 
type Z :*: b = Z 
type Z :+: b = b 

data S n Source

Type-level representation of successor

Instances

IsNat n => IsNat (S n) 
Typeable (* -> *) S 
Newtype (Vec (S n) a) (a, Vec n a) 
type (S a) :*: b = (:+:) b ((:*:) a b) 
type (S a) :+: b = S ((:+:) a b) 
type (S n) :-: (S m) = (:-:) n m 

type family a :+: b infixl 6 Source

Sum of type-level numbers

Instances

type Z :+: b = b 
type (S a) :+: b = S ((:+:) a b) 

type family a :*: b infixl 7 Source

Product of type-level numbers

Instances

type Z :*: b = Z 
type (S a) :*: b = (:+:) b ((:*:) a b) 

type family a :-: b infixl 6 Source

Instances

type n :-: Z = n 
type (S n) :-: (S m) = (:-:) n m 

type N0 = Z Source

type N1 = S N0 Source

type N2 = S N1 Source

type N3 = S N2 Source

type N4 = S N3 Source

type N5 = S N4 Source

type N6 = S N5 Source

type N7 = S N6 Source

type N8 = S N7 Source

type N9 = S N8 Source

type N10 = S N9 Source

type N11 = S N10 Source

type N12 = S N11 Source

type N13 = S N12 Source

type N14 = S N13 Source

type N15 = S N14 Source

type N16 = S N15 Source