Copyright  (C) 2016 University of Twente 

License  BSD2 (see the file LICENSE) 
Maintainer  Christiaan Baaij <christiaan.baaij@gmail.com> 
Safe Haskell  Trustworthy 
Language  Haskell2010 
Synopsis
 data RTree :: Nat > * > * where
 treplicate :: forall d a. SNat d > a > RTree d a
 trepeat :: KnownNat d => a > RTree d a
 indexTree :: (KnownNat d, Enum i) => RTree d a > i > a
 tindices :: forall d. KnownNat d => RTree d (Index (2 ^ d))
 replaceTree :: (KnownNat d, Enum i) => i > a > RTree d a > RTree d a
 tmap :: forall d a b. KnownNat d => (a > b) > RTree d a > RTree d b
 tzipWith :: forall a b c d. KnownNat d => (a > b > c) > RTree d a > RTree d b > RTree d c
 tzip :: KnownNat d => RTree d a > RTree d b > RTree d (a, b)
 tunzip :: forall d a b. KnownNat d => RTree d (a, b) > (RTree d a, RTree d b)
 tfold :: forall d a b. KnownNat d => (a > b) > (b > b > b) > RTree d a > b
 tdfold :: forall p k a. KnownNat k => Proxy (p :: TyFun Nat * > *) > (a > p @@ 0) > (forall l. SNat l > (p @@ l) > (p @@ l) > p @@ (l + 1)) > RTree k a > p @@ k
 v2t :: forall d a. KnownNat d => Vec (2 ^ d) a > RTree d a
 t2v :: forall d a. KnownNat d => RTree d a > Vec (2 ^ d) a
 lazyT :: KnownNat d => RTree d a > RTree d a
RTree
data type
data RTree :: Nat > * > * where Source #
Perfect depth binary tree.
 Only has elements at the leaf of the tree
 A tree of depth d has 2^d elements.
pattern LR :: a > RTree 0 a  Leaf of a perfect depth tree
Can be used as a pattern:

pattern BR :: RTree d a > RTree d a > RTree (d + 1) a  Branch of a perfect depth tree
Case be used a pattern:

Instances
Construction
treplicate :: forall d a. SNat d > a > RTree d a Source #
"treplicate
d a
" returns a tree of depth d, and has 2^d copies
of a.
>>>
treplicate (SNat :: SNat 3) 6
<<<6,6>,<6,6>>,<<6,6>,<6,6>>>>>>
treplicate d3 6
<<<6,6>,<6,6>>,<<6,6>,<6,6>>>
trepeat :: KnownNat d => a > RTree d a Source #
"trepeat
a
" creates a tree with as many copies of a as demanded by
the context.
>>>
trepeat 6 :: RTree 2 Int
<<6,6>,<6,6>>
Accessors
Indexing
indexTree :: (KnownNat d, Enum i) => RTree d a > i > a Source #
"indexTree
t n
" returns the n'th element of t.
The bottomleft leaf had index 0, and the bottomright leaf has index 2^d1, where d is the depth of the tree
>>>
indexTree (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4))) 0
1>>>
indexTree (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4))) 2
3>>>
indexTree (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4))) 14
*** Exception: Clash.Sized.Vector.(!!): index 14 is larger than maximum index 3 ...
tindices :: forall d. KnownNat d => RTree d (Index (2 ^ d)) Source #
Generate a tree of indices, where the depth of the tree is determined by the context.
>>>
tindices :: RTree 3 (Index 8)
<<<0,1>,<2,3>>,<<4,5>,<6,7>>>
Modifying trees
replaceTree :: (KnownNat d, Enum i) => i > a > RTree d a > RTree d a Source #
"replaceTree
n a t
" returns the tree t where the n'th element is
replaced by a.
The bottomleft leaf had index 0, and the bottomright leaf has index 2^d1, where d is the depth of the tree
>>>
replaceTree 0 5 (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<<5,2>,<3,4>>>>>
replaceTree 2 7 (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<<1,2>,<7,4>>>>>
replaceTree 9 6 (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<<1,2>,<3,*** Exception: Clash.Sized.Vector.replace: index 9 is larger than maximum index 3 ...
Elementwise operations
Mapping
tmap :: forall d a b. KnownNat d => (a > b) > RTree d a > RTree d b Source #
"tmap
f t
" is the tree obtained by apply f to each element of t,
i.e.,
tmap f (BR (LR a) (LR b)) == BR (LR (f a)) (LR (f b))
tzipWith :: forall a b c d. KnownNat d => (a > b > c) > RTree d a > RTree d b > RTree d c Source #
Zipping
tzip :: KnownNat d => RTree d a > RTree d b > RTree d (a, b) Source #
tzip
takes two trees and returns a tree of corresponding pairs.
Unzipping
tunzip :: forall d a b. KnownNat d => RTree d (a, b) > (RTree d a, RTree d b) Source #
tunzip
transforms a tree of pairs into a tree of first components and a
tree of second components.
Folding
:: KnownNat d  
=> (a > b)  Function to apply to the leaves 
> (b > b > b)  Function to combine the results of the reduction of two branches 
> RTree d a  Tree to fold reduce 
> b 
Reduce a tree to a single element
Specialised folds
:: KnownNat k  
=> Proxy (p :: TyFun Nat * > *)  The motive 
> (a > p @@ 0)  Function to apply to the elements on the leafs 
> (forall l. SNat l > (p @@ l) > (p @@ l) > p @@ (l + 1))  Function to fold the branches with. NB: 
> RTree k a  Tree to fold over. 
> p @@ k 
A dependently typed fold over trees.
As an example of when you might want to use dtfold
we will build a
population counter: a circuit that counts the number of bits set to '1' in
a BitVector
. Given a vector of n bits, we only need we need a data type
that can represent the number n: Index
(n+1)
. Index
k
has a range
of [0 .. k1]
(using ceil(log2(k))
bits), hence we need Index
n+1
.
As an initial attempt we will use tfold
, because it gives a nice (log2(n)
)
treestructure of adders:
populationCount :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1)) => BitVector (2^d) > Index (2^d+1) populationCount = tfold fromIntegral (+) . v2t . bv2v
The "problem" with this description is that all adders have the same bitwidth, i.e. all adders are of the type:
(+) ::Index
(2^d+1) >Index
(2^d+1) >Index
(2^d+1).
This is a "problem" because we could have a more efficient structure: one where each layer of adders is precisely wide enough to count the number of bits at that layer. That is, at height d we want the adder to be of type:
Index
((2^d)+1) >Index
((2^d)+1) >Index
((2^(d+1))+1)
We have such an adder in the form of the plus
function, as
defined in the instance ExtendingNum
instance of Index
.
However, we cannot simply use fold
to create a treestructure of
plus
es:
>>>
:{
let populationCount' :: (KnownNat (2^d), KnownNat d, KnownNat (2^d+1)) => BitVector (2^d) > Index (2^d+1) populationCount' = tfold fromIntegral plus . v2t . bv2v :} <interactive>:... • Couldn't match type ‘(((2 ^ d) + 1) + ((2 ^ d) + 1))  1’ with ‘(2 ^ d) + 1’ Expected type: Index ((2 ^ d) + 1) > Index ((2 ^ d) + 1) > Index ((2 ^ d) + 1) Actual type: Index ((2 ^ d) + 1) > Index ((2 ^ d) + 1) > AResult (Index ((2 ^ d) + 1)) (Index ((2 ^ d) + 1)) • In the second argument of ‘tfold’, namely ‘plus’ In the first argument of ‘(.)’, namely ‘tfold fromIntegral plus’ In the expression: tfold fromIntegral plus . v2t . bv2v • Relevant bindings include populationCount' :: BitVector (2 ^ d) > Index ((2 ^ d) + 1) (bound at ...)
because tfold
expects a function of type "b > b > b
", i.e. a function
where the arguments and result all have exactly the same type.
In order to accommodate the type of our plus
, where the
result is larger than the arguments, we must use a dependently typed fold in
the form of dtfold
:
{# LANGUAGE UndecidableInstances #} import Data.Singletons.Prelude import Data.Proxy data IIndex (f ::TyFun
Nat *) :: * type instanceApply
IIndex l =Index
((2^l)+1) populationCount' :: (KnownNat k, KnownNat (2^k)) => BitVector (2^k) > Index ((2^k)+1) populationCount' bv =tdfold
(Proxy @IIndex) fromIntegral (\_ x y >plus
x y) (v2t
(bv2v
bv))
And we can test that it works:
>>>
:t populationCount' (7 :: BitVector 16)
populationCount' (7 :: BitVector 16) :: Index 17>>>
populationCount' (7 :: BitVector 16)
3
Conversions
v2t :: forall d a. KnownNat d => Vec (2 ^ d) a > RTree d a Source #
Convert a vector with 2^d elements to a tree of depth d.
>>>
(1:>2:>3:>4:>Nil)
<1,2,3,4>>>>
v2t (1:>2:>3:>4:>Nil)
<<1,2>,<3,4>>
t2v :: forall d a. KnownNat d => RTree d a > Vec (2 ^ d) a Source #
Convert a tree of depth d to a vector of 2^d elements
>>>
(BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<<1,2>,<3,4>>>>>
t2v (BR (BR (LR 1) (LR 2)) (BR (LR 3) (LR 4)))
<1,2,3,4>