From f348445975e4fec72f48b7ec3e06124378e801c8 Mon Sep 17 00:00:00 2001
From: nihonium <nihonium@rape.lol>
Date: Tue, 7 Mar 2023 19:29:14 +0300
Subject: [PATCH] zipList

---
 applicative/list.md | 71 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 71 insertions(+)
 create mode 100644 applicative/list.md

diff --git a/applicative/list.md b/applicative/list.md
new file mode 100644
index 0000000..3bae384
--- /dev/null
+++ b/applicative/list.md
@@ -0,0 +1,71 @@
+### Законы
+
+```
+--Identity
+pure id <*> x == x
+
+--2.Homomorphism
+pure f <*> pure x == pure (f x)
+
+--3.Interchange
+u <*> pure y == pure ($ y) <*> u
+
+--4.Composition
+u <*> (v <*> w) == pure (.) <*> u <*> v <*> w
+```
+
+## Доказательство
+
+### Identity
+
+```
+pure id <*> CustomList lst == 
+CustomList $ repeat id <*> CustomList lst ==
+CustomList $ zipWith ($) (repeat id) lst ==
+CustomList lst 
+```
+
+### 2.Homomorphism
+
+```
+pure f <*> pure x ==
+CustomList $ repeat f <*> CustomList $ repeat x ==
+CustomList $ zipWith ($) (repeat f) (repeat x) ==
+CustomList $ repeat (f x)
+```
+
+### 3.Interchange
+
+```
+u <*> pure y ==
+CustomList fs <*> CustomList $ repeat y ==
+CustomList $ zipWith ($) fs (repeat y) [1]
+
+pure ($ y) <*> u ==
+CustomList $ repeat ($ y) <*> CustomList fs ==
+CustomList $ zipWith ($) (repeat ($ y)) fs [2]
+
+Type of ($ y): (a -> b) -> b
+Type of ($): (a -> b) -> a -> b
+Type of ($) ($ y): (a -> b) -> b
+
+($) f x == ($) ($ x) f
+
+=> [1] == [2]
+```
+
+### 4.Composition
+
+```
+u <*> (v <*> w) == 
+CustomList fs2 <*> (CustomList fs1 <*> CustomList xs) ==
+CustomList fs2 <*> CustomList $ zipWith ($) fs1 xs ==
+CustomList fs2 <*> CustomList xs1 ==
+... ==
+CustomList xs12 (Длина xs12 - наименьшая из длин fs1, fs2 и xs)
+
+pure (.) <*> u <*> v <*> w ==
+pure (.) CustomList fs2 <*> CustomList fs1 <*> CustomList xs ==
+CustomList fs12 <*> Custom xs == (fs12 - список из композиций соответствующих функций, длина fs12 - наименьшая из длин fs1 и fs2)
+CustomList xs12 (длина xs12 - наименьшая из длин fs12 и xs)
+```