Safe Haskell	None

BundledPatterns

Synopsis

Documentation

data Vec :: Nat -> * -> * where #

Fixed size vectors.

Lists with their length encoded in their type
Vector elements have an ASCENDING subscript starting from 0 and ending at length - 1.

Constructors

Nil :: Vec 0 a

Bundled Patterns

pattern (:>) :: a -> Vec n a -> Vec (n + 1) a infixr 5

Add an element to the head of a vector.

>>> 3:>4:>5:>Nil
<3,4,5>
>>> let x = 3:>4:>5:>Nil
>>> :t x
x :: Num a => Vec 3 a

Can be used as a pattern:

>>> let f (x :> y :> _) = x + y
>>> :t f
f :: Num a => Vec ((n + 1) + 1) a -> a
>>> f (3:>4:>5:>6:>7:>Nil)
7

Also in conjunctions with (:<):

>>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
>>> :t g
g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
>>> g (1:>2:>3:>4:>5:>Nil)
12

data RTree :: Nat -> * -> * where #

Perfect depth binary tree.

Bundled Patterns

pattern LR :: a -> RTree 0 a

Leaf of a perfect depth tree

>>> LR 1
1
>>> let x = LR 1
>>> :t x
x :: Num a => RTree 0 a

Can be used as a pattern:

>>> let f (LR a) (LR b) = a + b
>>> :t f
f :: Num a => RTree 0 a -> RTree 0 a -> a
>>> f (LR 1) (LR 2)
3

pattern BR :: RTree d a -> RTree d a -> RTree (d + 1) a

Branch of a perfect depth tree

>>> BR (LR 1) (LR 2)
<1,2>
>>> let x = BR (LR 1) (LR 2)
>>> :t x
x :: Num a => RTree 1 a

Case be used a pattern:

>>> let f (BR (LR a) (LR b)) = LR (a + b)
>>> :t f
f :: Num a => RTree 1 a -> RTree 0 a
>>> f (BR (LR 1) (LR 2))
3