blob: da3bcc51670950dab4d00f99f4b4f98215a0eec4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
import prelude
import nat
data List : (_:Type) -> Type where
Nil : (A:Type) -> List A
Cons : (A:Type) -> A -> List A -> List A
size : (A:Type) -> List A -> Nat
size _ (Nil _) = Zero
size A (Cons _ x xs) = Succ (size A xs)
map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B
map _ B _ (Nil _) = Nil B
map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs)
append : (A:Type) -> (xs:List A) -> List A -> List A
append A xs ys = foldr A (List A) (Cons A) ys xs
concat : (A : Type) -> List (List A) -> List A
concat A = foldr (List A) (List A) (append A) (Nil A)
foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B
foldr _ _ _ x (Nil _) = x
foldr A B f x (Cons _ y ys) = f y (foldr A B f x ys)
-- Instances:
monad_List : Monad List
monad_list = rec return = \A -> \x -> Cons A x (Nil A)
bind = \A -> \B -> \m -> \k -> concat B (map A B k m)
|
