I attempted to use div operator on natural numbers exported from Data.Type.Nat module,but I got this error:
src\RandomAccessList.hs:54:37: error:
Not in scope: ‘Data.Nat.div’
Perhaps you meant one of these:
data constructor ‘Data.Nat.S’ (imported from Data.Nat),
data constructor ‘Data.Nat.Z’ (imported from Data.Nat)
Module ‘Data.Nat’ does not export ‘div’.
|
54 | where m = n Data.Nat.div 2
| ^^^^^^^^^^^^
Full source code:
module RandomAccessList() where
import Data.Type.Nat
import qualified Data.Nat
data Tree a = Leaf a | Node Nat (Tree a) (Tree a)
size :: Tree a -> Nat
size (Leaf x) = 1
size (Node n _ _) = n
node ::Tree a -> Tree a -> Tree a
node t1 t2 = Node (size t1 + size t2) t1 t2
data Digit a = Zero | One (Tree a)
type RAList a = [Digit a] --a list of Digit a
fromRA::RAList a -> [a]
{--
[ Zero,
One (Node 2 (Leaf 'a') (Leaf 'b')),
One (Node 4 (Node 2 (Leaf 'c') (Leaf 'd'))
(Node 2 (Leaf 'e') (Leaf 'f')))]
--}
fromRA = concatMap from
where from Zero =[]
from (One t) = fromT t
fromT ::Tree a -> [a]
fromT (Leaf x) =[x]
fromT (Node _ t1 t2) = fromT t1 ++ fromT t2
fetchRA::Nat -> RAList a -> a
fetchRA k (Zero:xs) = fetchRA k xs
fetchRA k (One t :xs) = if k < size t
then fetchT k t else fetchRA (k - size t) xs
fetchT ::Nat -> Tree a -> a
fetchT 0 (Leaf x) = x
fetchT k (Node n t1 t2) =
if k < m
then fetchT k t1 else fetchT (k - m) t2
where m = n Data.Nat.div 2
If I just use div without any qualifier,I would get this error: