rnhmjoj/interlude
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Replace star with Type

Browse Source
This commit is contained in:
rnhmjoj 2016-11-27 20:17:27 +01:00
parent b9f249a9ff
commit 9d3ec1d2ad
No known key found for this signature in database
GPG Key ID: 362BB82B7E496B7C
1 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Data/Vec.hs
View File

@ -18,6 +18,7 @@
module Data.Vec where module Data.Vec where
import Relation.Equality (gcastWith) import Relation.Equality (gcastWith)
import Data.Kind (Type)
import Data.Nat import Data.Nat
import Data.Bool import Data.Bool
import Data.Char (Char) import Data.Char (Char)
@ -31,7 +32,7 @@ import qualified Data.TypeClass as T
infixr 5 :- infixr 5 :-
-- | The 'Vec' datatype -- | The 'Vec' datatype
data Vec ∷ ★ → ℕ → ★ where data Vec ∷ Type → ℕ → Type where
Nil ∷ Vec a Z -- ^ empty 'Vec', length 0 Nil ∷ Vec a Z -- ^ empty 'Vec', length 0
(:-) ∷ a → Vec a n → Vec a (S n) -- ^ "cons" operator (:-) ∷ a → Vec a n → Vec a (S n) -- ^ "cons" operator
@ -197,27 +198,27 @@ permutations xs@(_:-_) = concatMap (\(y,ys) → map (y:-) (permutations ys)) (se
-- and a 'Vec' reduces the vector to a single value obtained -- and a 'Vec' reduces the vector to a single value obtained
-- by sequentially applying the operation from the left to the right. -- 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 b n → a
foldl _ x Nil = x foldl _ x Nil = x
foldl (⊗) x (y :- ys) = foldl (⊗) (x ⊗ y) ys foldl (⊗) x (y :- ys) = foldl (⊗) (x ⊗ y) ys
-- | Same as "fold" but reduces the vector in the opposite -- | Same as "fold" but reduces the vector in the opposite
-- direction: from the right to the left. -- direction: from the right to the left.
foldr ∷ (a → b → b) → b → Vec a n → b foldr ∷ (a → b → b) → b → Vec a n → b
foldr _ x Nil = x foldr _ x Nil = x
foldr (⊗) x (y:-ys) = y ⊗ (foldr (⊗) x ys) foldr (⊗) x (y:-ys) = y ⊗ (foldr (⊗) x ys)
-- | Variant of 'foldl' which requires no starting value but -- | Variant of 'foldl' which requires no starting value but
-- applies only on nonempty 'Vec' -- applies only on nonempty 'Vec'
foldl₁ ∷ (a → a → a) → Vec a (S n) → a foldl₁ ∷ (a → a → a) → Vec a (S n) → a
foldl₁ _ (x :- Nil) = x foldl₁ _ (x :- Nil) = x
foldl₁ (⊗) (x :- y :- ys) = foldl₁ (⊗) (x ⊗ y :- ys) foldl₁ (⊗) (x :- y :- ys) = foldl₁ (⊗) (x ⊗ y :- ys)
-- | As for 'foldl', a variant of 'foldr' with no starting point -- | 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 a (S n) → a
foldr₁ _ (x :- Nil) = x foldr₁ _ (x :- Nil) = x
foldr₁ (⊗) (x :- y :- ys) = x ⊗ (foldr₁ (⊗) (y :- ys)) foldr₁ (⊗) (x :- y :- ys) = x ⊗ (foldr₁ (⊗) (y :- ys))