applicative h1

1 files changed, 32 insertions, 0 deletions

diff --git a/applicative/h1.txt b/applicative/h1.txt
new file mode 100644
index 0000000..42d2c0e
--- /dev/null
+++ b/applicative/h1.txt
@@ -0,0 +1,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