zipList
This commit is contained in:
		
							parent
							
								
									6354df0b0c
								
							
						
					
					
						commit
						f348445975
					
				
					 1 changed files with 71 additions and 0 deletions
				
			
		
							
								
								
									
										71
									
								
								applicative/list.md
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										71
									
								
								applicative/list.md
									
										
									
									
									
										Normal file
									
								
							|  | @ -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) | ||||||
|  | ``` | ||||||
		Reference in a new issue