/
weak.linf
47 lines (43 loc) · 1.63 KB
/
weak.linf
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
type Unit === forall A. A -> A in
let unit : Unit === fun (type A) x -> x in
type Pair A B === forall K. (A -> B -> K) -> K in
let pair (type A) (type B) (a : A) (b : B) : Pair A B ===
fun (type K) k -> k a b in
type Garbage === forall K. (forall A. A -> K) -> K in
let empty : Garbage === fun (type K) k -> k (type Unit) unit in
let collect : forall A. A -> Garbage -> Garbage ===
fun (type A) x garbage ->
fun (type K) k -> k (type Pair A Garbage) (pair (type A) (type Garbage) x garbage) in
type Weak A === Garbage -> Pair A Garbage in
let pure : forall A. A -> Weak A ===
fun (type A) x ->
fun garbage -> pair (type A) (type Garbage) x garbage in
let weak : forall A. A -> Weak Unit ===
fun (type A) x ->
fun garbage -> (
pair (type Unit) (type Garbage) unit
(collect (type A) x garbage)
) in
let bind : forall A B. Weak A -> (A -> Weak B) -> Weak B ===
fun (type A) (type B) m f ->
fun garbage -> (
let value_and_garbage === m garbage in
value_and_garbage (type Pair B Garbage) (fun x garbage -> f x garbage)
) in
let map : forall A B. Weak A -> (A -> B) -> Weak B ===
fun (type A) (type B) m f ->
bind (type A) (type B) m (fun x -> pure (type B) (f x)) in
type Either A B === forall K. (A -> K) -> (B -> K) -> Weak K in
let left : forall A B. A -> Either A B ===
fun (type A) (type B) a ->
fun (type K) l r ->
map (type Unit) (type K)
(weak (type B -> K) r)
(fun unit -> unit (type K) (l a)) in
let right : forall A B. B -> Either A B ===
fun (type A) (type B) b ->
fun (type K) l r ->
map (type Unit) (type K)
(weak (type A -> K) l)
(fun unit -> unit (type K) (r b)) in
right