From 934eda548d1f0260db095f2739b2211bd5157324 Mon Sep 17 00:00:00 2001
From: Joe Zhao <ztuowen@gmail.com>
Date: Wed, 25 Mar 2015 21:39:46 +0800
Subject: applicative h1

---
 applicative/h1.txt | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 applicative/h1.txt

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
-- 
cgit v1.2.3-70-g09d2