flip Vec arguments to allow a Functor instance

src/Data/TypeClass.hs

@@ -13,14 +13,21 @@ module Data.TypeClass
   , Read(..)
   , IsList(..)
   , IsString(..)
+  , Functor(..)
+  , Applicative(..)
+  , Monad(..)
   ) where
 
 import GHC.Enum
 import GHC.Show
 import GHC.Read
 import GHC.Num
+import GHC.Real
 import GHC.Exts
-import Prelude (Eq(..), Ord(..), Integral(..))
+import Data.Eq
+import Data.Ord
+import Data.Functor
+import Prelude (Monad(..), Applicative(..))
 
 -- * Aliases
 

src/Data/Vec.hs

@@ -23,7 +23,7 @@ import Data.Nat          hiding ((+), (-), (×), min, max)
 import Data.Bool
 import Data.Maybe        (Maybe(..))
 import Data.Char         (Char)
-import Data.Function     ((∘))
+import Data.Function     ((∘), flip)
 import Data.Singletons   (SingI, sing)
 
 import Data.TypeClass
@@ -32,34 +32,35 @@ import Data.TypeClass
 infixr 5 :-
 
 -- | The 'Vec' datatype
-data Vec ∷ Type → ℕ → Type where
+data Vec ∷ ℕ → Type → Type where
-  Nil  ∷ Vec a Z                   -- ^ empty 'Vec', length 0
+  Nil  ∷ Vec Z a                   -- ^ empty 'Vec', length 0
-  (:-) ∷ a → Vec a n → Vec a (S n) -- ^ "cons" operator
+  (:-) ∷ a → Vec n a → Vec (S n) a -- ^ "cons" operator
 
 
 -- | 'String' type alias for vector of characters
-type String n = Vec Char n
+type String n = Vec n Char
 
 
-deriving instance Eq a ⇒ Eq (Vec a n)
+deriving instance Eq a ⇒ Eq (Vec n a)
 
-instance Show a ⇒ Show (Vec a n) where
+instance Show a ⇒ Show (Vec n a) where
   showsPrec d = showsPrec d ∘ vecToList
 
-instance SingI n ⇒ IsList (Vec a n) where
+instance SingI n ⇒ IsList (Vec n a) where
-  type Item (Vec a n) = a
+  type Item (Vec n a) = a
   fromList = listToVec
   toList   = vecToList
 
 instance SingI n ⇒ IsString (String n) where
   fromString = fromList
 
-
+instance SingI n ⇒ Functor (Vec n) where
+  fmap = map
 
 -- * Conversions
 
 -- | Convert a 'Vec' into a List
-vecToList ∷ Vec a n → [a]
+vecToList ∷ Vec n a → [a]
 vecToList Nil = []
 vecToList (x :- xs) = x : vecToList xs
 
@@ -69,10 +70,10 @@ vecToList (x :- xs) = x : vecToList xs
 -- It's not possible to convert an infinite list to a vector
 -- as haskell does not permit constructing infinite type,
 -- which the resulting vector length would be.
-listToVec ∷ SingI n ⇒ [a] → Vec a n
+listToVec ∷ SingI n ⇒ [a] → Vec n a
 listToVec = f sing
-  where  f ∷ Sℕ n → [a] → Vec a n
+  where  f ∷ Sℕ n → [a] → Vec n a
-         f SZ     _      = Nil
+         f SZ     []      = Nil
          f (SS n) (x:xs)  = x :- f n xs
 
 
@@ -80,31 +81,31 @@ listToVec = f sing
 -- * Basic functions
 
 -- | Vector concatenation
-(⧺) ∷ Vec a n → Vec a m → Vec a (n :+ m)
+(⧺) ∷ Vec n a → Vec m a → Vec (n :+ m) a
 (⧺) (x :- xs) ys = x :- xs ⧺ ys
 (⧺) Nil       ys = ys
 
 
 -- | Extracts the 'head' (ie the first element) of a nonempty 'Vec'.
-head ∷ Vec a (S n) → a
+head ∷ Vec (S n) a → a
 head (x :- _) = x
 
 
 -- | Extracts the last element of a nonempty 'Vec'.
-last ∷ Vec a (S n) → a
+last ∷ Vec (S n) a → a
 last (x :- Nil)     = x
 last (x :- y :- ys) = last (y :- ys)
 
 
 -- | Applied to a nonempty 'Vec' returns everything but its first element.
 -- > x ≡ head x ⧺ tail x
-tail ∷ Vec a (S n) → Vec a n
+tail ∷ Vec (S n) a → Vec n a
 tail (_ :- xs) = xs
 
 
 -- | Applied to a nonempty 'Vec' returns everything but its last element.
 -- > x ≡ init x ⧺ last x
-init ∷ Vec a (S n) → Vec a n
+init ∷ Vec (S n) a → Vec n a
 init (x :- Nil)     = Nil
 init (x :- y :- ys) = x :- init (y :- ys)
 
@@ -112,23 +113,23 @@ init (x :- y :- ys) = x :- init (y :- ys)
 -- | Given a nonempty 'Vec' returns the first element
 -- and the rest of the vector in a tuple.
 -- > uncons x ≡ (head x, tail x)
-uncons ∷ Vec a (S n) → (a, Vec a n)
+uncons ∷ Vec (S n) a → (a, Vec n a)
 uncons (x :- xs) = (x, xs)
 
 
 -- | Test whether a 'Vec' has zero length.
-null ∷ Vec a n → 𝔹
+null ∷ Vec n a → 𝔹
 null Nil = T
 null _   = F
 
 
 -- | Returns the length (numbers of elements) of a 'Vec'.
-length ∷ Vec a n → ℕ
+length ∷ Vec n a → ℕ
 length Nil       = Z
 length (_ :- xs) = S (length xs)
 
 -- | Same as 'length' but produces a singleton type 'Sℕ'.
-sLength ∷ Vec a n → Sℕ n
+sLength ∷ Vec n a → Sℕ n
 sLength Nil       = SZ
 sLength (x :- xs) = SS (sLength xs)
 
@@ -137,14 +138,14 @@ sLength (x :- xs) = SS (sLength xs)
 -- * Transformations
 
 -- | Applies a function on every element of a 'Vec'.
-map ∷ (a → b) → Vec a n → Vec b n
+map ∷ (a → b) → Vec n a → Vec n b
 map _ Nil       = Nil
 map f (x :- xs) = f x :- map f xs
 
 
 -- | Reverse the order of the elements of a 'Vec'
 -- > reverse ∘ reverse = id
-reverse ∷ Vec a n → Vec a n
+reverse ∷ Vec n a → Vec n a
 reverse Nil       = Nil
 reverse (y :- ys) = gcastWith proof (reverse ys ⧺ (y :- Nil))
   where proof = succ_plus (sLength ys)
@@ -153,7 +154,7 @@ reverse (y :- ys) = gcastWith proof (reverse ys ⧺ (y :- Nil))
 -- | 'intersperse' @s@ takes a 'Vec' and produces one where
 -- @s@ is interspersed (ie inserted between) every two elements
 -- of the vector
-intersperse ∷ a → Vec a n → Vec a (n :+ Pred n)
+intersperse ∷ a → Vec n a → Vec (n :+ Pred n) a
 intersperse _ Nil        = Nil
 intersperse _ (x :- Nil) = x :- Nil
 intersperse s (x :- xs)  = gcastWith proof (x :- s :- intersperse s xs)
@@ -165,7 +166,7 @@ intersperse s (x :- xs)  = gcastWith proof (x :- s :- intersperse s xs)
 -- | 'intercalate' @xs xss@ is equivalent to
 -- @('concat' ('intersperse' xs xss))@. It inserts the vector @xs@
 -- in between the vectors in @xss@ and concatenates the result.
-intercalate ∷ Vec a n → Vec (Vec a n) m → Vec a ((m :+ Pred m) :× n)
+intercalate ∷ Vec n a → Vec  m (Vec n a) → Vec ((m :+ Pred m) :× n) a
 intercalate xs xss = concat (intersperse xs xss)
 
 
@@ -174,7 +175,7 @@ intercalate xs xss = concat (intersperse xs xss)
 --
 -- > transpose [[1,2,3],[4,5,6]] ≡ [[1,4],[2,5],[3,6]]
 --
-transpose ∷ SingI n ⇒ Vec (Vec a n) m → Vec (Vec a m) n
+transpose ∷ SingI n ⇒ Vec m (Vec n a) → Vec n (Vec m a)
 transpose Nil         = replicate Nil
 transpose (xs :- xss) = gcastWith proof (zipWith (:-) xs (transpose xss))
   where proof = min_self (sLength xs)
@@ -183,12 +184,12 @@ transpose (xs :- xss) = gcastWith proof (zipWith (:-) xs (transpose xss))
 -- | The 'permutations' function returns the vector of all permutations of the argument.
 --
 -- > permutations "abc" ≡ ["abc","bac","cba","bca","cab","acb"]
-permutations ∷ Vec a n → Vec (Vec a n) (Fact n)
+permutations ∷ Vec n a → Vec (Fact n) (Vec n a)
 permutations Nil       = Nil:-Nil
 permutations (x:-Nil)  = (x:-Nil):-Nil
 permutations xs@(_:-_) = concatMap (\(y,ys) → map (y:-) (permutations ys)) (select xs)
   where
-    select ∷ Vec a n → Vec (a, Vec a (Pred n)) n
+    select ∷ Vec n a → Vec n (a, Vec (Pred n) a)
     select Nil            = Nil
     select (x:-Nil)       = (x, Nil) :- Nil
     select (x:-xs@(_:-_)) = (x,xs) :- map (\(y,ys) → (y, x:-ys)) (select xs)
@@ -197,27 +198,27 @@ permutations xs@(_:-_) = concatMap (\(y,ys) → map (y:-) (permutations ys)) (se
 -- | 'foldl' applied to a binary operator, a starting value
 -- and a 'Vec' reduces the vector to a single value obtained
 -- by sequentially applying the operation from the left to the right.
-foldl ∷ (a → b → a) → a → Vec b n → a
+foldl ∷ (a → b → a) → a → Vec n b → a
 foldl  _  x Nil       = x
 foldl (⊗) x (y :- ys) = foldl (⊗) (x ⊗ y) ys
 
 
 -- | Same as "fold" but reduces the vector in the opposite
 -- direction: from the right to the left.
-foldr ∷ (a → b → b) → b → Vec a n → b
+foldr ∷ (a → b → b) → b → Vec n a → b
 foldr  _  x Nil     = x
 foldr (⊗) x (y:-ys) = y ⊗ (foldr (⊗) x ys)
 
 
 -- | Variant of 'foldl' which requires no starting value but
 -- applies only on nonempty 'Vec'
-foldl₁ ∷ (a → a → a) → Vec a (S n) → a
+foldl₁ ∷ (a → a → a) → Vec (S n) a → a
 foldl₁  _  (x :- Nil)     = x
 foldl₁ (⊗) (x :- y :- ys) = foldl₁ (⊗) (x ⊗ y :- ys)
 
 
 -- | As for 'foldl', a variant of 'foldr' with no starting point
-foldr₁ ∷ (a → a → a) → Vec a (S n) → a
+foldr₁ ∷ (a → a → a) → Vec (S n) a → a
 foldr₁  _  (x :- Nil)     = x
 foldr₁ (⊗) (x :- y :- ys) = x ⊗ (foldr₁ (⊗) (y :- ys))
 
@@ -226,7 +227,7 @@ foldr₁ (⊗) (x :- y :- ys) = x ⊗ (foldr₁ (⊗) (y :- ys))
 -- * Special folds
 
 -- | The concatenation of all the elements of a vector of vectors.
-concat ∷ Vec (Vec a n) m → Vec a (m :× n)
+concat ∷ Vec m (Vec n a) → Vec (m :× n) a
 concat Nil = Nil
 concat (xs :- xss) = gcastWith proof (xs ⧺ concat xss)
   where
@@ -237,61 +238,61 @@ concat (xs :- xss) = gcastWith proof (xs ⧺ concat xss)
 
 -- | Map a function over all the elements of a vector and concatenate
 -- the resulting vectors.
-concatMap ∷ (a → Vec b n) → Vec a m → Vec b (m :× n)
+concatMap ∷ (a → Vec n b) → Vec m a → Vec (m :× n) b
 concatMap f = concat ∘ map f
 
 
 -- | Applied to a a value produces a vector obtained by
 -- duplicating the value @n@ times.
-replicate ∷ ∀ a n. SingI n ⇒ a → Vec a n
+replicate ∷ ∀ a n. SingI n ⇒ a → Vec n a
 replicate = replicate' (sing ∷ Sℕ n)
 
 
 -- | 'replicate' variant with an explicit length argument.
-replicate' ∷ Sℕ n → a → Vec a n
+replicate' ∷ Sℕ n → a → Vec n a
 replicate' SZ     _ = Nil
 replicate' (SS n) a = a :- replicate' n a
 
 
 -- | 'and' returns the conjunction of a container of bools.
-and ∷ Vec 𝔹 (S n) → 𝔹
+and ∷ Vec (S n) 𝔹 → 𝔹
 and = foldr₁ (∧)
 
 
 -- | 'or' returns the disjunction of a container of bools.
-or ∷ Vec 𝔹 (S n) → 𝔹
+or ∷ Vec (S n) 𝔹 → 𝔹
 or = foldr₁ (∨)
 
 
 -- | Determines whether any element of the structure satisfies the predicate.
-any ∷ (a → 𝔹) → Vec a n → 𝔹
+any ∷ (a → 𝔹) → Vec n a → 𝔹
 any _ Nil       = F
 any p (x :- xs) = or (map p (x :- xs))
 
 
 -- | Determines whether all elements of the structure satisfy the predicate.
-all ∷ (a → 𝔹) → Vec a n → 𝔹
+all ∷ (a → 𝔹) → Vec n a → 𝔹
 all _ Nil       = T
 all p (x :- xs) = and (map p (x :- xs))
 
 
 -- | The least element of a vector.
-minimum ∷ Ord a ⇒ Vec a (S n) → a
+minimum ∷ Ord a ⇒ Vec (S n) a → a
 minimum = foldr₁ min
 
 
 -- | The largest element of a vector.
-maximum ∷ Ord a ⇒ Vec a (S n) → a
+maximum ∷ Ord a ⇒ Vec (S n) a → a
 maximum = foldr₁ max
 
 
 -- | The 'sum' function computes the sum of the numbers of a vector.
-sum ∷ Num a ⇒ Vec a n → a
+sum ∷ Num a ⇒ Vec n a → a
 sum = foldr (+) 0
 
 
 -- | The 'product' function computes the product of the numbers of a vector.
-product ∷ Num a ⇒ Vec a n → a
+product ∷ Num a ⇒ Vec n a → a
 product = foldr (×) 1
 
 
@@ -299,23 +300,23 @@ product = foldr (×) 1
 -- Extracting subvectors
 
 -- | 'take' returns the first @n@ element of the vector
-take ∷ ∀ a n m. SingI n ⇒ Vec a m → Vec a n
+take ∷ ∀ a n m. SingI n ⇒ Vec m a → Vec n a
 take = take' (sing ∷ Sℕ n)
 
 
 -- | Variant of 'take' with an explicit argument.
-take' ∷ Sℕ n → Vec a m → Vec a n
+take' ∷ Sℕ n → Vec m a → Vec n a
 take' SZ      _        = Nil
 take' (SS n) (x :- xs) = x :- take' n xs
 
 
 -- | 'drop' returns every element of the vector but the first @n@
-drop ∷ ∀ a n m. SingI n ⇒ Vec a m → Vec a (m :- n)
+drop ∷ ∀ a n m. SingI n ⇒ Vec m a → Vec (m :- n) a
 drop = drop' (sing ∷ Sℕ n)
 
 
 -- | Variant of 'drop' with an explicit argument.
-drop' ∷ Sℕ n → Vec a m → Vec a (m :- n)
+drop' ∷ Sℕ n → Vec m a → Vec (m :- n) a
 drop' SZ     x         = x
 drop' (SS n) (x :- xs) = drop' n xs
 
@@ -324,18 +325,28 @@ drop' (SS n) (x :- xs) = drop' n xs
 -- Searching by equality
 
 -- | Does the element occur in the structure?
-elem ∷ Eq a ⇒ Vec a n → a → 𝔹
+elem ∷ Eq a ⇒ Vec n a → a → 𝔹
 elem Nil       _ = F
 elem (x :- xs) y = (x ≡ y) ∨ (elem xs y)
 
 
+-- | Infix version of 'elem'
+(∈) ∷ Eq a ⇒ a → Vec n a → 𝔹
+(∈) = flip elem
+
+
 -- | 'notElem' is the negation of 'elem'.
-notElem ∷ Eq a ⇒ Vec a n → a → 𝔹
+notElem ∷ Eq a ⇒ Vec n a → a → 𝔹
 notElem xs = (¬) ∘ elem xs
 
 
+-- | Infix version of 'notElem'
+(∉) ∷ Eq a ⇒ a → Vec n a → 𝔹
+(∉) = flip notElem
+
+
 -- | 'lookup' key assocs looks up a key in an association vector.
-lookup ∷ Eq a ⇒ a → Vec (a, b) n → Maybe b
+lookup ∷ Eq a ⇒ a → Vec n (a, b) → Maybe b
 lookup t Nil          = Nothing
 lookup t ((k,v) :- x) =
   if t ≡ k
@@ -352,7 +363,7 @@ lookup t ((k,v) :- x) =
 -- 'zip' is right-lazy:
 --
 -- > zip Nil ⊥ ≡ Nil
-zip ∷ Vec a n → Vec b m → Vec (a, b) (Min n m)
+zip ∷ Vec n a → Vec m b → Vec (Min n m) (a, b)
 zip = zipWith (,)
 
 
@@ -364,7 +375,7 @@ zip = zipWith (,)
 -- 'zipWith' is right-lazy:
 --
 -- > zipWith f Nil ⊥ ≡ Nil
-zipWith ∷ (a → b → c) → Vec a n → Vec b m → Vec c (Min n m)
+zipWith ∷ (a → b → c) → Vec n a → Vec m b → Vec (Min n m) c
 zipWith _ Nil _ = Nil
 zipWith _ _ Nil = Nil
 zipWith (⊗) (x :- xs) (y :- ys) = x ⊗ y :- zipWith (⊗) xs ys
@@ -372,7 +383,7 @@ zipWith (⊗) (x :- xs) (y :- ys) = x ⊗ y :- zipWith (⊗) xs ys
 
 -- | 'unzip' transforms a vectors of pairs into a vector of first components
 -- and a vector of second components.
-unzip ∷ Vec (a, b) n → (Vec a n, Vec b n)
+unzip ∷ Vec n (a, b) → (Vec n a, Vec n b)
 unzip Nil             = (Nil, Nil)
 unzip ((x, y) :- xys) = (x :- xs, y :- ys)
   where (xs, ys) = unzip xys