add transpose

This commit is contained in:
rnhmjoj 2016-11-16 01:03:51 +01:00
parent 8abcc2f1f1
commit 2c4ab33bc4
No known key found for this signature in database
GPG Key ID: 362BB82B7E496B7C
2 changed files with 27 additions and 12 deletions

View File

@ -4,12 +4,13 @@ let
inherit (nixpkgs) pkgs;
f = { mkDerivation, base, singletons, stdenv }:
f = { mkDerivation, base, integer-gmp, singletons, stdenv }:
mkDerivation {
pname = "Interlude";
version = "0.1.0.0";
src = ./.;
libraryHaskellDepends = [ base singletons ];
libraryHaskellDepends = [ base integer-gmp singletons ];
description = "My take on Prelude";
license = stdenv.lib.licenses.gpl3;
};

View File

@ -168,6 +168,16 @@ intercalate ∷ Vec a n → Vec (Vec a n) m → Vec a ((m :+ Pred m) :× n)
intercalate xs xss = concat (intersperse xs xss)
-- | The 'transpose' function transposes the rows and columns of its argument.
-- For example,
--
-- > 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 Nil = replicate Nil
transpose (xs :- xss) = zipWith (:-) xs (transpose xss)
-- | '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.
@ -214,11 +224,16 @@ concatMap ∷ (a → Vec b n) → Vec a m → Vec b (m :× n)
concatMap f = concat map f
-- | Applied to a singleton natural @n@ and a value produces
-- a vector obtained by duplicating the value @n@ times
replicate S n a Vec a n
replicate SZ _ = Nil
replicate (SS n) a = a :- replicate n a
-- | 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 = replicate' (sing S n)
-- | 'replicate' variant with an explicit length argument.
replicate' S n a Vec a n
replicate' SZ _ = Nil
replicate' (SS n) a = a :- replicate' n a
-- | 'and' returns the conjunction of a container of bools.
@ -233,14 +248,14 @@ or = foldr₁ ()
-- | Determines whether any element of the structure satisfies the predicate.
any (a 𝔹) Vec a n 𝔹
any _ Nil = T
any p xs = or (map p xs)
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 _ Nil = T
all p xs = and (map p xs)
all p (x :- xs) = and (map p (x :- xs))
-- | The 'sum' function computes the sum of the numbers of a vector.
@ -266,4 +281,3 @@ drop ∷ S n → Vec a m → Vec a (m :- n)
drop SZ x = x
drop (SS n) (x :- xs) = drop n xs