[fix] further zip-related tweaks

Author: bgavran

src/Data/Container/Applicative/Instances.idr

@@ -23,10 +23,6 @@ namespace ListApplicative
     pure = fromList . pure
     fs <*> vs = fromList $ toList fs <*> toList vs
 
-  public export
-  listZip' : List' a -> List' b -> List' (a, b)
-  listZip' l1 l2 = fromList $ listZip (toList l1) (toList l2)
-
   ||| Note that usually it is said that List has two applicative structures
   ||| one defined above, and another one defined by `zipList` (Section 3 of 
   ||| https://www.staff.city.ac.uk/~ross/papers/Constructors.pdf).
@@ -39,9 +35,11 @@ namespace ListApplicative
   ||| and we cannot lawfully make `List` an applicative functor in such a way.
   ||| For instance, this is not a valid applicative instance, because unital 
   ||| laws do not hold:
-  ||| Applicative List' where
-  |||   pure = fromList . pure
-  |||   fs <*> vs = fromList $ uncurry ($) <$> listZip (toList fs) (toList vs)
+  |||
+  ||| Applicative List where
+  |||   pure a = [a]
+  |||   fs <*> xs = uncurry ($) <$> listZip fs xs
+
 
 
 namespace BinTreeLeafApplicative

src/Data/Tree.idr

@@ -150,6 +150,7 @@ namespace BinaryTrees
 
     {--
     In general no applicative instance for a tree with values only on nodes.
+    Note that you can define the `pure` and `liftA2`, but they won't satisfy applicative laws.
     See https://www.reddit.com/r/haskell/comments/cb1j40/comment/etct1xk/
     --} 
 

src/Misc.idr

@@ -22,20 +22,6 @@ public export
 strength : Applicative f => a -> f b -> f (a, b)
 strength a fb = liftA2 (pure a) fb
 
-||| Prelude.Types already has one implementation of Applicative List
-||| This is the other one, which behaves like a zip
-namespace ListApplicative
-  public export
-  listZip : List a -> List b -> List (a, b)
-  listZip [] _ = []
-  listZip (x :: xs) [] = []
-  listZip (x :: xs) (y :: ys) = (x, y) :: listZip xs ys
-  
-  public export
-  [zipInstance] Applicative List where
-    pure a = [a]
-    fs <*> xs = uncurry ($) <$> listZip fs xs
-
 ||| Analogue of `(::)` for lists. 
 ||| Takes an element and prepends it to some 'vector' 
 public export
@@ -116,6 +102,11 @@ namespace List
   prod : Num a => List a -> a
   prod = foldr (*) (fromInteger 1)
 
+public export
+listZip : List a -> List b -> List (a, b)
+listZip (x :: xs) (y :: ys) = (x, y) :: listZip xs ys
+listZip _ _ = []
+
 public export
 maxInList : Ord a => List a -> Maybe a
 maxInList [] = Nothing
@@ -529,4 +520,16 @@ filter'' p (x :: xs) with (filter' p xs)
 {-
 Prelude.absurd : Uninhabited t => t -> a
 
- -}
+ -}
+
+h : {n : Nat} -> Vect n a -> Nat
+h xs = n
+
+
+g : {0 n : Nat} -> Vect n a -> Nat
+g [] = 0
+g (x :: xs) = 1 + (g xs)
+
+proof2 : (v : Vect n a) -> g v = n
+proof2 [] = Refl
+proof2 (x :: xs) = cong (1 +) (proof2 xs)