From d22f298356c6f759e106a1484fb2b8a58274d87a Mon Sep 17 00:00:00 2001 From: rnhmjoj Date: Sun, 4 Dec 2016 04:16:07 +0100 Subject: [PATCH] flip Vec arguments to allow a Functor instance --- src/Data/TypeClass.hs | 9 ++- src/Data/Vec.hs | 125 +++++++++++++++++++++++------------------- 2 files changed, 76 insertions(+), 58 deletions(-) diff --git a/src/Data/TypeClass.hs b/src/Data/TypeClass.hs index ce8a8ae..f88e0b7 100644 --- a/src/Data/TypeClass.hs +++ b/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 diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs index b4191e8..ecc2088 100644 --- a/src/Data/Vec.hs +++ b/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 - Nil ∷ Vec a Z -- ^ empty 'Vec', length 0 - (:-) ∷ a → Vec a n → Vec a (S n) -- ^ "cons" operator +data Vec ∷ ℕ → Type → Type where + Nil ∷ Vec Z a -- ^ empty 'Vec', length 0 + (:-) ∷ 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 - type Item (Vec a n) = a +instance SingI n ⇒ IsList (Vec n a) where + 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,42 +70,42 @@ 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 - f SZ _ = Nil - f (SS n) (x:xs) = x :- f n xs + where f ∷ Sℕ n → [a] → Vec n a + f SZ [] = Nil + f (SS n) (x:xs) = x :- f n xs -- * 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