module Data.List
export
{ singleton; replicate;
enumFromTo; append; concat;
length;
head;
tail; tail1;
last; index;
lookupBy; find;
reverse;
map; mapS; for;
forS;
zipWith; zipWithS;
foldl; foldlS; sum; prod;
foldr; foldrS;
scanl;
filter; filterS;
any;
}
import Data.Numeric.Nat
import Data.Numeric.Bool
import Data.Tuple
import Data.Maybe
import Data.Function
import Class.Functor
import Class.Monad
where
-- | Standard Cons-lists.
data List (a: Data) where
Nil : List a
Cons : a -> List a -> List a
-- Constructors ---------------------------------------------------------------
-- | Construct a list containing a single element.
singleton (x: a): List a
= Cons x Nil
-- | Construct a list of the given length where all elements are'
-- the same value.
replicate (n: Nat) (x: a): List a
| n == 0 = Nil
| otherwise = Cons x (replicate (n - 1) x)
-- | Construct a range of values.
enumFromTo (start: Nat) (end: Nat): List Nat
| start >= end = singleton start
| otherwise = Cons start (enumFromTo (start + 1) end)
-- | Append two lists.
append (xx yy: List a): List a
= case xx of
Nil -> yy
Cons x xs -> Cons x (append xs yy)
-- | Concatenate a list of lists.
concat (xss0: List (List a)): List a
= case xss0 of
Nil -> Nil
Cons xs xss1 -> go xs xss1
where
go Nil Nil = Nil
go Nil (Cons xs' xss') = go xs' xss'
go (Cons x xs) xss = Cons x (go xs xss)
-- | Generate a list of the given length by repeatedly
-- applying a stateful function.
unfold (s0: s) (f: s -> Maybe (Tup2 a s)): List a
= case f s0 of
Nothing -> Nil
Just (T2 a s1) -> Cons a (unfold s1 f)
generate (len: Nat) (f: Nat -> a): List a
= unfold 0
$ (\ix -> if ix >= len
then Nothing
else Just (T2 (f ix) (ix + 1)))
-- Projections ----------------------------------------------------------------
-- | Take the length of a list.
length (xx: List a): Nat
= case xx of
Nil -> 0
Cons x xs -> 1 + length xs
-- | Take the head of a list, if there is one.
head (def: a) (xx: List a): a
= case xx of
Nil -> def
Cons x xs -> x
-- | Take the tail of a list, if there is one.
tail (def: List a) (xx: List a): List a
= case xx of
Nil -> def
Cons x xs -> xs
-- | Like `tail`, but if there is only one element then keep it.
tail1 (def: a) (xx: List a): List a
= case xx of
Nil -> singleton def
Cons x Nil -> singleton x
Cons _ xs -> xs
-- | Take the last element of a list, if there is one.
last (def: a) (xx: List a): a
= case xx of
Nil -> def
Cons x Nil -> x
Cons x (Cons y ys) -> last def (Cons y ys)
index (def: a) (n: Nat) (xx: List a): a
= case xx of
Nil -> def
Cons x xs
-> case n of
0 -> x
_ -> index def (n - 1) xs
-- Searches -------------------------------------------------------------------
-- | Given a list of key value pairs, lookup the first
-- value whose key is selected by the given predicate.
lookupBy (f: a -> Bool) (xx: List (Tup2 a b)): Maybe b
= case xx of
Nil -> Nothing
Cons (T2 x y) xs
| f x -> Just y
| otherwise -> lookupBy f xs
-- | Find the first element in a list that matches the given predicate.
find (f: a -> Bool) (xx: List a): Maybe a
= case xx of
Nil -> Nothing
Cons x xs
| f x -> Just x
| otherwise -> find f xs
-- Transforms -----------------------------------------------------------------
-- | Reverse the elements of a list.
-- This is a naive O(n^2) version for testing purposes.
reverse (xx: List a): List a
= case xx of
Nil -> Nil
Cons x xs -> append (reverse xs) (singleton x)
-- Maps -----------------------------------------------------------------------
-- | Apply a worker function to every element of a list, yielding a new list.
map (f: a -> b) (xx: List a): List b
= case xx of
Nil -> Nil
Cons x xs -> Cons (f x) (map f xs)
-- | Like `map`, but with the arguments swapped.
for (xx: List a) (f: a -> b): List b
= case xx of
Nil -> Nil
Cons x xs -> Cons (f x) (for xs f)
-- | Functor instance for List.
functor_list
= Functor map
-- | Apply a stateful worker function to every element of a list,
-- yielding a new list.
-- The worker is applied to the source elements left-to-right.
mapS (f: a -> S e b) (xx: List a): S e (List b)
= case xx of
Nil -> Nil
Cons x xs -> Cons (f x) (mapS f xs)
-- | Apply a function to all elements of a list, yielding nothing.
forS (xx: List a) (f: a -> S e Unit): S e Unit
= case xx of
Nil -> ()
Cons x xs
-> do f x
forS xs f
-- | Monadic map.
mapM (dMonad: Monad m)
(f: a -> m b) (xx: List a): m (List b)
= case xx of
Nil
-> return dMonad Nil
Cons x xs
-> bind dMonad (f x) $ λx'
-> bind dMonad (mapM dMonad f xs) $ λxs'
-> return dMonad (Cons x' xs')
-- Zips -----------------------------------------------------------------------
zipWith (f: a -> b -> c)
(xx: List a) (yy: List b): List c
= case T2 xx yy of
T2 Nil _ -> Nil
T2 (Cons x xs) Nil -> Nil
T2 (Cons x xs) (Cons y ys)
-> Cons (f x y) (zipWith f xs ys)
-- | Stateful zipWith.
zipWithS (f: a -> b -> S e c)
(xx: List a) (yy: List b): S e (List c)
= case T2 xx yy of
T2 Nil _ -> Nil
T2 (Cons x xs) Nil -> Nil
T2 (Cons x xs) (Cons y ys)
-> Cons (f x y) (zipWithS f xs ys)
-- Folds ----------------------------------------------------------------------
-- | Reduce a list with a binary function and zero value,
-- from left to right.
foldl (f: b -> a -> b) (z: b) (xx: List a): b
= case xx of
Nil -> z
Cons x xs -> foldl f (f z x) xs
-- | Reduce a list with a stateful binary function and zero value,
-- from left to right.
foldlS (f: b -> a -> S e b) (z: b) (xx: List a): S e b
= case xx of
Nil -> z
Cons x xs -> foldlS f (f z x) xs
-- | Reduce a list with a binary function and zero value,
-- from right to left.
foldr (f: a -> b -> b) (z: b) (xx: List a): b
= case xx of
Nil -> z
Cons x xs -> f x (foldr f z xs)
-- | Reduce a list with a stateful binary function and zero value,
-- from right to left.
foldrS (f: a -> b -> S e b) (z: b) (xx: List a): S e b
= case xx of
Nil -> z
Cons x xs -> f x (foldrS f z xs)
-- | Take the sum of a list of Nats.
sum (xs: List Nat): Nat
= foldl (+) 0 xs
-- | Take the product of a list of Nats.
prod (xs: List Nat): Nat
= foldl (*) 1 xs
-- | Monadic sequence.
sequence (dMonad: Monad m) (xs: List (m a)): m (List a)
= mapM dMonad id xs
-- Scans ----------------------------------------------------------------------
scanl (f: b -> a -> b) (acc: b) (xx: List a): List b
= case xx of
Nil
-> Cons acc Nil
Cons x xs
-> let acc' = f acc x
in Cons acc (scanl f acc' xs)
-- Filters --------------------------------------------------------------------
-- | Keep only those elements that match the given predicate.
filter (p: a -> Bool) (xx: List a): List a
= case xx of
Nil -> Nil
Cons x xs
| p x -> Cons x (filter p xs)
| otherwise -> filter p xs
-- | Keep only those elements that match the given stateful predicate.
-- The predicate is applied to the list elements from left to right.
filterS (p: a -> S e Bool) (xx: List a): S e (List a)
= case xx of
Nil -> Nil
Cons x xs
| p x -> Cons x (filterS p xs)
| otherwise -> filterS p xs
-- | Check if any of the members of the list match the given predicate.
any (p: a -> Bool) (xx: List a): Bool
= case xx of
Nil -> False
Cons x xs
| p x -> True
| otherwise -> any p xs