blob: 42d2c0e278910001c2706f801df0bdba746cc810 (
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
32
|
Prove: pure f <*> x = pure (flip ($)) <*> x <*> pure f
$ : (a -> b) -> a -> b
flip : (a -> b -> c) -> b -> a -> c
flip ($) : a -> (a -> b) -> b
(.) : (b -> c) -> (a -> b) -> a -> c
(. (flip ($))) (((a->b)->b) -> c) -> a -> c
f : x -> y
$ f : ((x -> y) -> b) -> b
(($ f). (flip ($))) x -> y
idea: Any expression built from the Applicative combinators can be transformed to a canonical form
pure (flip ($)) <*> x <*> pure f
= pure ($ f) <*> (pure (flip ($)) <*> x)
= pure (.) <*> pure ($ f) <*> pure (flip ($)) <*> x
= pure (($ f).(flip ($))) <*> x
= pure f <*> x
$ : f -> v -> f(v)
flip ($) : v -> f -> f(v)
($ f).(flip ($))
=>
(f' -> f'(f)) . (v -> f'' -> f''(v))
=>
(v -> f'(f)) where f' = f'' -> f''(v)
=> v -> f(v)
=> f
|
