Safe Haskell	Trustworthy
Language	Haskell2010

Data.SOP.NP.DeFun

Contents

Append
Map
Concat
ConcatMap
Map2
Sequence
Foldr
Foldl
ZipWith
Reverse

Description

This module is designed to imported qualified:

import qualified Data.SOP.NP.DeFun as NP

Synopsis

type family Append (xs :: [a]) (ys :: [a]) :: [a] where ...
data AppendSym (xs :: FunKind [a] ([a] ~> [a]))
data AppendSym1 (xs :: [a]) (ys :: FunKind [a] [a])
append :: NP a xs -> NP a ys -> NP a (Append xs ys)
appendSym :: Lam2 (NP a) (NP a) (NP a) AppendSym
appendSym1 :: NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs)
type family Map (f :: a ~> b) (xs :: [a]) :: [b] where ...
data MapSym (f :: FunKind (a ~> b) ([a] ~> [b]))
data MapSym1 (f :: a ~> b) (xs :: FunKind [a] [b])
map :: Lam a b f -> NP a xs -> NP b (Map f xs)
mapSym :: Lam (a :~> b) (Lam (NP a) (NP b)) MapSym
mapSym1 :: Lam a b f -> Lam (NP a) (NP b) (MapSym1 f)
type family Concat (xss :: [[a]]) :: [a] where ...
data ConcatSym (xss :: FunKind [[a]] [a])
concat :: NP (NP a) xss -> NP a (Concat xss)
concatSym :: Lam (NP (NP a)) (NP a) ConcatSym
type family ConcatMap (f :: a ~> [b]) (xs :: [a]) :: [b] where ...
data ConcatMapSym (f :: FunKind (a ~> [b]) ([a] ~> [b]))
data ConcatMapSym1 (f :: a ~> [b]) (xs :: FunKind [a] [b])
concatMap :: Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMapSym :: Lam2 (a :~> NP b) (NP a) (NP b) ConcatMapSym
concatMapSym1 :: Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f)
type family Map2 (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]) :: [c] where ...
data Map2Sym (f :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])))
data Map2Sym1 (f :: a ~> (b ~> c)) (xs :: FunKind [a] ([b] ~> [c]))
data Map2Sym2 (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: FunKind [b] [c])
map2 :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2Sym :: Lam3 (a :~> (b :~> c)) (NP a) (NP b) (NP c) Map2Sym
map2Sym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f)
map2Sym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs)
type family Sequence (xss :: [[a]]) :: [[a]] where ...
data SequenceSym (xss :: FunKind [[a]] [[a]])
sequence :: NP (NP a) xss -> NP (NP a) (Sequence xss)
sequenceSym :: Lam (NP (NP a)) (NP (NP a)) SequenceSym
type family Foldr (f :: a ~> (b ~> b)) (z :: b) (xs :: [a]) :: b where ...
data FoldrSym (f :: FunKind (a ~> (b ~> b)) (b ~> ([a] ~> b)))
data FoldrSym1 (f :: a ~> (b ~> b)) (z :: FunKind b ([a] ~> b))
data FoldrSym2 (f :: a ~> (b ~> b)) (z :: b) (xs :: FunKind [a] b)
foldr :: Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldrSym :: Lam3 (a :~> (b :~> b)) b (NP a) b FoldrSym
foldrSym1 :: Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f)
foldrSym2 :: Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x)
type family Foldl (f :: b ~> (a ~> b)) (z :: b) (xs :: [a]) :: b where ...
data FoldlSym (f :: FunKind (b ~> (a ~> b)) (b ~> ([a] ~> b)))
data FoldlSym1 (f :: b ~> (a ~> b)) (z :: FunKind b ([a] ~> b))
data FoldlSym2 (f :: b ~> (a ~> b)) (z :: b) (xs :: FunKind [a] b)
foldl :: Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldlSym :: Lam3 (b :~> (a :~> b)) b (NP a) b FoldlSym
foldlSym1 :: Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f)
foldlSym2 :: Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x)
type family ZipWith (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]) :: [c] where ...
data ZipWithSym (f :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])))
data ZipWithSym1 (f :: a ~> (b ~> c)) (xs :: FunKind [a] ([b] ~> [c]))
data ZipWithSym2 (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: FunKind [b] [c])
zipWith :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWithSym :: Lam3 (a :~> (b :~> c)) (NP a) (NP b) (NP c) ZipWithSym
zipWithSym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f)
zipWithSym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs)
type family Reverse (xs :: [a]) :: [a] where ...
data ReverseSym (xs :: FunKind [a] [a])
reverse :: NP a xs -> NP a (Reverse xs)
reverseSym :: Lam (NP a) (NP a) ReverseSym

Append

type family Append (xs :: [a]) (ys :: [a]) :: [a] where ... #

List append.

>>> :kind! Append [1, 2, 3] [4, 5, 6]
Append [1, 2, 3] [4, 5, 6] :: [Natural]
= [1, 2, 3, 4, 5, 6]

Equations

Append ('[] :: [a]) (ys :: [a]) = ys
Append (x ': xs :: [a]) (ys :: [a]) = x ': Append xs ys

data AppendSym (xs :: FunKind [a] ([a] ~> [a])) #

Instances

Instances details

type App (AppendSym :: FunKind [a] ([a] ~> [a]) -> Type) (xs :: [a])
Instance details Defined in DeFun.List type App (AppendSym :: FunKind [a] ([a] ~> [a]) -> Type) (xs :: [a]) = AppendSym1 xs

data AppendSym1 (xs :: [a]) (ys :: FunKind [a] [a]) #

Instances

Instances details

type App (AppendSym1 xs :: FunKind [a] [a] -> Type) (ys :: [a])
Instance details Defined in DeFun.List type App (AppendSym1 xs :: FunKind [a] [a] -> Type) (ys :: [a]) = Append xs ys

append :: NP a xs -> NP a ys -> NP a (Append xs ys) Source #

appendSym :: Lam2 (NP a) (NP a) (NP a) AppendSym Source #

appendSym1 :: NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs) Source #

Map

type family Map (f :: a ~> b) (xs :: [a]) :: [b] where ... #

List map

>>> :kind! Map NotSym [True, False]
Map NotSym [True, False] :: [Bool]
= [False, True]

>>> :kind! Map (Con1 Just) [1, 2, 3]
Map (Con1 Just) [1, 2, 3] :: [Maybe Natural]
= [Just 1, Just 2, Just 3]

Equations

Map (f :: a ~> b) ('[] :: [a]) = '[] :: [b]
Map (f :: a ~> b) (x ': xs :: [a]) = (f @@ x) ': Map f xs

data MapSym (f :: FunKind (a ~> b) ([a] ~> [b])) #

Instances

Instances details

type App (MapSym :: FunKind (a ~> b) ([a] ~> [b]) -> Type) (f :: a ~> b)
Instance details Defined in DeFun.List type App (MapSym :: FunKind (a ~> b) ([a] ~> [b]) -> Type) (f :: a ~> b) = MapSym1 f

data MapSym1 (f :: a ~> b) (xs :: FunKind [a] [b]) #

Instances

Instances details

type App (MapSym1 f :: FunKind [a] [b] -> Type) (xs :: [a])
Instance details Defined in DeFun.List type App (MapSym1 f :: FunKind [a] [b] -> Type) (xs :: [a]) = Map f xs

map :: Lam a b f -> NP a xs -> NP b (Map f xs) Source #

mapSym :: Lam (a :~> b) (Lam (NP a) (NP b)) MapSym Source #

mapSym1 :: Lam a b f -> Lam (NP a) (NP b) (MapSym1 f) Source #

Concat

type family Concat (xss :: [[a]]) :: [a] where ... #

List concat

>>> :kind! Concat [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]
Concat [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ] :: [Natural]
= [1, 2, 3, 4, 5, 6, 7, 8, 9]

Equations

Concat ('[] :: [[a]]) = '[] :: [a]
Concat (xs ': xss :: [[a]]) = Append xs (Concat xss)

data ConcatSym (xss :: FunKind [[a]] [a]) #

Instances

Instances details

type App (ConcatSym :: FunKind [[a]] [a] -> Type) (xss :: [[a]])
Instance details Defined in DeFun.List type App (ConcatSym :: FunKind [[a]] [a] -> Type) (xss :: [[a]]) = Concat xss

concat :: NP (NP a) xss -> NP a (Concat xss) Source #

concatSym :: Lam (NP (NP a)) (NP a) ConcatSym Source #

ConcatMap

type family ConcatMap (f :: a ~> [b]) (xs :: [a]) :: [b] where ... #

List concatMap

Equations

ConcatMap (f :: a ~> [b]) ('[] :: [a]) = '[] :: [b]
ConcatMap (f :: a ~> [b]) (x ': xs :: [a]) = Append (f @@ x) (ConcatMap f xs)

data ConcatMapSym (f :: FunKind (a ~> [b]) ([a] ~> [b])) #

Instances

Instances details

type App (ConcatMapSym :: FunKind (a ~> [b]) ([a] ~> [b]) -> Type) (f :: a ~> [b])
Instance details Defined in DeFun.List type App (ConcatMapSym :: FunKind (a ~> [b]) ([a] ~> [b]) -> Type) (f :: a ~> [b]) = ConcatMapSym1 f

data ConcatMapSym1 (f :: a ~> [b]) (xs :: FunKind [a] [b]) #

Instances

Instances details

type App (ConcatMapSym1 f :: FunKind [a] [b] -> Type) (xs :: [a])
Instance details Defined in DeFun.List type App (ConcatMapSym1 f :: FunKind [a] [b] -> Type) (xs :: [a]) = ConcatMap f xs

concatMap :: Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs) Source #

concatMapSym :: Lam2 (a :~> NP b) (NP a) (NP b) ConcatMapSym Source #

concatMapSym1 :: Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f) Source #

Map2

type family Map2 (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]) :: [c] where ... #

List binary map. I.e. liftA2 for lists.

Note: this is not ZipWith.

>>> :kind! Map2 (Con2 '(,)) [1, 2, 3] ['x', 'y']
Map2 (Con2 '(,)) [1, 2, 3] ['x', 'y'] :: [(Natural, Char)]
= ['(1, 'x'), '(1, 'y'), '(2, 'x'), '(2, 'y'), '(3, 'x'), '(3, 'y')]

This function is a good example to highlight how to defunctionalize definitions with anonymous functions.

The simple definition can be written using concatMap and map from Prelude:

>>> import Prelude as P (concatMap, map, (.), flip)
>>> let map2 f xs ys = P.concatMap (\x -> P.map (f x) ys) xs
>>> map2 (,) "abc" "xy"
[('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]

However, to make it easier (arguably) to defunctionalize, the concatMap argument lambda can be written in point-free form using combinators:

>>> let map2 f xs ys = P.concatMap (P.flip P.map ys P.. f) xs
>>> map2 (,) "abc" "xy"
[('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]

Alternatively, we could define a new "top-level" function

>>> let map2Aux f ys x = P.map (f x) ys

and use it to define @map2:

>>> let map2 f xs ys = P.concatMap (map2Aux f ys) xs
>>> map2 (,) "abc" "xy"
[('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]

Equations

Map2 (f :: a1 ~> (a2 ~> b)) (xs :: [a1]) (ys :: [a2]) = ConcatMap (CompSym2 (FlipSym2 (MapSym :: FunKind (a2 ~> b) ([a2] ~> [b]) -> Type) ys) f) xs

data Map2Sym (f :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c]))) #

Instances

Instances details

type App (Map2Sym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c))
Instance details Defined in DeFun.List type App (Map2Sym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) = Map2Sym1 f

data Map2Sym1 (f :: a ~> (b ~> c)) (xs :: FunKind [a] ([b] ~> [c])) #

Instances

Instances details

type App (Map2Sym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a])
Instance details Defined in DeFun.List type App (Map2Sym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) = Map2Sym2 f xs

data Map2Sym2 (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: FunKind [b] [c]) #

Instances

Instances details

type App (Map2Sym2 f xs :: FunKind [b] [c] -> Type) (ys :: [b])
Instance details Defined in DeFun.List type App (Map2Sym2 f xs :: FunKind [b] [c] -> Type) (ys :: [b]) = Map2 f xs ys

map2 :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys) Source #

map2Sym :: Lam3 (a :~> (b :~> c)) (NP a) (NP b) (NP c) Map2Sym Source #

map2Sym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f) Source #

map2Sym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs) Source #

Sequence

type family Sequence (xss :: [[a]]) :: [[a]] where ... #

List sequence

>>> :kind! Sequence [[1,2,3],[4,5,6]]
Sequence [[1,2,3],[4,5,6]] :: [[Natural]]
= [[1, 4], [1, 5], [1, 6], [2, 4], [2, 5], [2, 6], [3, 4], [3, 5], [3, 6]]

Equations

Sequence ('[] :: [[a]]) = '['[] :: [a]]
Sequence (xs ': xss :: [[a]]) = Map2 (Con2 ('(:) :: a -> [a] -> [a])) xs (Sequence xss)

data SequenceSym (xss :: FunKind [[a]] [[a]]) #

Instances

Instances details

type App (SequenceSym :: FunKind [[a]] [[a]] -> Type) (xss :: [[a]])
Instance details Defined in DeFun.List type App (SequenceSym :: FunKind [[a]] [[a]] -> Type) (xss :: [[a]]) = Sequence xss

sequence :: NP (NP a) xss -> NP (NP a) (Sequence xss) Source #

sequenceSym :: Lam (NP (NP a)) (NP (NP a)) SequenceSym Source #

Foldr

type family Foldr (f :: a ~> (b ~> b)) (z :: b) (xs :: [a]) :: b where ... #

List right fold

Using Foldr we can define a Curry type family:

>>> type Curry args res = Foldr (Con2 (->)) args res
>>> :kind! Curry String [Int, Bool]
Curry String [Int, Bool] :: *
= Int -> Bool -> [Char]

Equations

Foldr (f :: a ~> (b ~> b)) (z :: b) ('[] :: [a]) = z
Foldr (f :: a ~> (b ~> b)) (z :: b) (x ': xs :: [a]) = (f @@ x) @@ Foldr f z xs

data FoldrSym (f :: FunKind (a ~> (b ~> b)) (b ~> ([a] ~> b))) #

Instances

Instances details

type App (FoldrSym :: FunKind (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: a ~> (b ~> b))
Instance details Defined in DeFun.List type App (FoldrSym :: FunKind (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: a ~> (b ~> b)) = FoldrSym1 f

data FoldrSym1 (f :: a ~> (b ~> b)) (z :: FunKind b ([a] ~> b)) #

Instances

Instances details

type App (FoldrSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b)
Instance details Defined in DeFun.List type App (FoldrSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) = FoldrSym2 f z

data FoldrSym2 (f :: a ~> (b ~> b)) (z :: b) (xs :: FunKind [a] b) #

Instances

Instances details

type App (FoldrSym2 f z :: FunKind [a] b -> Type) (xs :: [a])
Instance details Defined in DeFun.List type App (FoldrSym2 f z :: FunKind [a] b -> Type) (xs :: [a]) = Foldr f z xs

foldr :: Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys) Source #

foldrSym :: Lam3 (a :~> (b :~> b)) b (NP a) b FoldrSym Source #

foldrSym1 :: Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f) Source #

foldrSym2 :: Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x) Source #

Foldl

type family Foldl (f :: b ~> (a ~> b)) (z :: b) (xs :: [a]) :: b where ... #

List left fold

Equations

Foldl (f :: b ~> (a ~> b)) (z :: b) ('[] :: [a]) = z
Foldl (f :: k ~> (a ~> k)) (z :: k) (x ': xs :: [a]) = Foldl f ((f @@ z) @@ x) xs

data FoldlSym (f :: FunKind (b ~> (a ~> b)) (b ~> ([a] ~> b))) #

Instances

Instances details

type App (FoldlSym :: FunKind (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: b ~> (a ~> b))
Instance details Defined in DeFun.List type App (FoldlSym :: FunKind (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type) (f :: b ~> (a ~> b)) = FoldlSym1 f

data FoldlSym1 (f :: b ~> (a ~> b)) (z :: FunKind b ([a] ~> b)) #

Instances

Instances details

type App (FoldlSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b)
Instance details Defined in DeFun.List type App (FoldlSym1 f :: FunKind b ([a] ~> b) -> Type) (z :: b) = FoldlSym2 f z

data FoldlSym2 (f :: b ~> (a ~> b)) (z :: b) (xs :: FunKind [a] b) #

Instances

Instances details

type App (FoldlSym2 f z :: FunKind [a] b -> Type) (xs :: [a])
Instance details Defined in DeFun.List type App (FoldlSym2 f z :: FunKind [a] b -> Type) (xs :: [a]) = Foldl f z xs

foldl :: Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys) Source #

foldlSym :: Lam3 (b :~> (a :~> b)) b (NP a) b FoldlSym Source #

foldlSym1 :: Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f) Source #

foldlSym2 :: Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x) Source #

ZipWith

type family ZipWith (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]) :: [c] where ... #

Zip with

>>> :kind! ZipWith (Con2 '(,)) [1, 2, 3] ['x', 'y']
ZipWith (Con2 '(,)) [1, 2, 3] ['x', 'y'] :: [(Natural, Char)]
= ['(1, 'x'), '(2, 'y')]

Equations

ZipWith (f :: a ~> (b ~> c)) ('[] :: [a]) (ys :: [b]) = '[] :: [c]
ZipWith (f :: a ~> (b ~> c)) (x ': xs :: [a]) ('[] :: [b]) = '[] :: [c]
ZipWith (f :: a ~> (b ~> c)) (x ': xs :: [a]) (y ': ys :: [b]) = ((f @@ x) @@ y) ': ZipWith f xs ys

data ZipWithSym (f :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c]))) #

Instances

Instances details

type App (ZipWithSym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c))
Instance details Defined in DeFun.List type App (ZipWithSym :: FunKind (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type) (f :: a ~> (b ~> c)) = ZipWithSym1 f

data ZipWithSym1 (f :: a ~> (b ~> c)) (xs :: FunKind [a] ([b] ~> [c])) #

Instances

Instances details

type App (ZipWithSym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a])
Instance details Defined in DeFun.List type App (ZipWithSym1 f :: FunKind [a] ([b] ~> [c]) -> Type) (xs :: [a]) = ZipWithSym2 f xs

data ZipWithSym2 (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: FunKind [b] [c]) #

Instances

Instances details

type App (ZipWithSym2 f xs :: FunKind [b] [c] -> Type) (ys :: [b])
Instance details Defined in DeFun.List type App (ZipWithSym2 f xs :: FunKind [b] [c] -> Type) (ys :: [b]) = ZipWith f xs ys

zipWith :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys) Source #

zipWithSym :: Lam3 (a :~> (b :~> c)) (NP a) (NP b) (NP c) ZipWithSym Source #

zipWithSym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f) Source #

zipWithSym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs) Source #

Reverse

type family Reverse (xs :: [a]) :: [a] where ... #

Reverse list

>>> :kind! Reverse [1,2,3,4]
Reverse [1,2,3,4] :: [Natural]
= [4, 3, 2, 1]

Equations

Reverse (xs :: [a]) = Foldl (FlipSym1 (Con2 ('(:) :: a -> [a] -> [a]))) ('[] :: [a]) xs

data ReverseSym (xs :: FunKind [a] [a]) #

Instances

Instances details

type App (ReverseSym :: FunKind [a] [a] -> Type) (xs :: [a])
Instance details Defined in DeFun.List type App (ReverseSym :: FunKind [a] [a] -> Type) (xs :: [a]) = Reverse xs

reverse :: NP a xs -> NP a (Reverse xs) Source #

>>> reverse (SZ :* SS SZ :* SS (SS SZ) :* Nil)
SS (SS SZ) :* SS SZ :* SZ :* Nil

reverseSym :: Lam (NP a) (NP a) ReverseSym Source #