Harpie.Shape

Functions for manipulating shape. The module tends to supply equivalent functionality at type-level and value-level with functions of the same name (except for capitalization).

Type-level Nat

data SNat (n :: Nat)

A value-level witness for a type-level natural number. This is commonly referred to as a singleton type, as for each n, there is a single value that inhabits the type SNat n (aside from bottom).

The definition of SNat is intentionally left abstract. To obtain an SNat value, use one of the following:

1. The natSing method of KnownNat.
2. The SNat pattern synonym.
3. The withSomeSNat function, which creates an SNat from a Natural number.

Since: base-4.18.0.0

Instances

TestCoercion SNat

Since: base-4.18.0.0

Defined in GHC.TypeNats

Methods

testCoercion :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (Coercion a b)

TestEquality SNat

Since: base-4.18.0.0

Defined in GHC.TypeNats

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

Show (SNat n)

Since: base-4.18.0.0

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

pattern SNat :: () => KnownNat n => SNat n

A explicitly bidirectional pattern synonym relating an SNat to a KnownNat constraint.

As an expression: Constructs an explicit SNat n value from an implicit KnownNat n constraint:

SNat @n :: KnownNat n => SNat n

As a pattern: Matches on an explicit SNat n value bringing an implicit KnownNat n constraint into scope:

f :: SNat n -> ..
f SNat = {- SNat n in scope -}

Since: base-4.18.0.0

valueOf :: forall n. KnownNat n => Int

Get the value of a type level Nat. Use with explicit type application

>>> valueOf @42
42

Type-level [Nat]

data SNats (ns :: [Nat])

A value-level witness for a type-level list of natural numbers.

Obtain an SNats value using:

• The natsSing method of KnownNats
• The SNats pattern
• The withSomeSNats function

>>> :t SNats @[2,3,4]
SNats @[2,3,4] :: KnownNats [2, 3, 4] => SNats [2, 3, 4]
>>> SNats @[2,3,4]
SNats @[2, 3, 4]

Instances

Show (SNats ns)

Matches GHC printing quirks.

Defined in Harpie.Shape

Methods

showsPrec :: Int -> SNats ns -> ShowS

show :: SNats ns -> String

showList :: [SNats ns] -> ShowS

Eq (SNats ns)

Defined in Harpie.Shape

Methods

(==) :: SNats ns -> SNats ns -> Bool

(/=) :: SNats ns -> SNats ns -> Bool

Ord (SNats ns)

Defined in Harpie.Shape

Methods

compare :: SNats ns -> SNats ns -> Ordering

(<) :: SNats ns -> SNats ns -> Bool

(<=) :: SNats ns -> SNats ns -> Bool

(>) :: SNats ns -> SNats ns -> Bool

(>=) :: SNats ns -> SNats ns -> Bool

max :: SNats ns -> SNats ns -> SNats ns

min :: SNats ns -> SNats ns -> SNats ns

pattern SNats :: forall ns. () => KnownNats ns => SNats ns

A explicitly bidirectional pattern synonym relating an SNats to a KnownNats constraint.

As an expression: Constructs an explicit SNats ns value from an implicit KnownNats ns constraint:

SNat @n :: KnownNat n => SNat n

As a pattern: Matches on an explicit SNats n value bringing an implicit KnownNats n constraint into scope:

f :: SNats ns -> ..
f SNat = {- KnownNats ns in scope -}

or, if you need to both bring the KnownNats into scope and reuse the SNats input:

f (SNats :: SNats s) = g (SNats @s)

fromSNats :: SNats s -> [Nat]

Return the value-level list of naturals in an SNats ns value.

>>> fromSNats (SNats @[2,3,4])
[2,3,4]

class KnownNats (ns :: [Nat]) where

Reflect a list of naturals.

>>> natsSing @'[2]
SNats @'[2]

Methods

natsSing :: SNats ns

Instances

KnownNats ('[] :: [Nat])

Defined in Harpie.Shape

Methods

natsSing :: SNats '[]

(KnownNat n, KnownNats s) => KnownNats (n ': s)

Defined in Harpie.Shape

Methods

natsSing :: SNats (n ': s)

natVals :: forall ns proxy. KnownNats ns => proxy ns -> [Nat]

Obtain a value-level list of naturals from a type-level proxy

>>> natVals (SNats @[2,3,4])
[2,3,4]

withKnownNats :: forall ns rep (r :: TYPE rep). SNats ns -> (KnownNats ns => r) -> r

Convert an explicit SNats ns value into an implicit KnownNats ns constraint.

data SomeNats

An unknown type-level list of naturals.

someNatVals :: [Nat] -> SomeNats

Promote a list of naturals to unknown type-level

withSomeSNats :: forall rep (r :: TYPE rep). [Nat] -> (forall s. SNats s -> r) -> r

Convert a list of naturals into an SNats ns value, where ns is a fresh type-level list of naturals.

Shape

valuesOf :: forall s. KnownNats s => [Int]

The value of a KnownNats.

>>> valuesOf @[2,3,4]
[2,3,4]

rankOf :: forall s. KnownNats s => Int

The rank (or length) of a KnownNats.

>>> rankOf @[2,3,4]
3

sizeOf :: forall s. KnownNats s => Int

The size (or product) of a KnownNats.

>>> sizeOf @[2,3,4]
24

newtype Fin s

Fin most often represents a (finite) zero-based index for a single dimension (of a multi-dimensioned hyper-rectangular array).

Constructors

UnsafeFin

Fields

• fromFin :: Int

Instances

Show (Fin n)

Defined in Harpie.Shape

Methods

showsPrec :: Int -> Fin n -> ShowS

show :: Fin n -> String

showList :: [Fin n] -> ShowS

Eq (Fin s)

Defined in Harpie.Shape

Methods

(==) :: Fin s -> Fin s -> Bool

(/=) :: Fin s -> Fin s -> Bool

Ord (Fin s)

Defined in Harpie.Shape

Methods

compare :: Fin s -> Fin s -> Ordering

(<) :: Fin s -> Fin s -> Bool

(<=) :: Fin s -> Fin s -> Bool

(>) :: Fin s -> Fin s -> Bool

(>=) :: Fin s -> Fin s -> Bool

max :: Fin s -> Fin s -> Fin s

min :: Fin s -> Fin s -> Fin s

fin :: forall n. KnownNat n => Int -> Fin n

Construct a Fin.

Errors on out-of-bounds

>>> fin @2 1
1

>>> fin @2 2
*** Exception: value outside bounds
...

safeFin :: forall n. KnownNat n => Int -> Maybe (Fin n)

Construct a Fin safely.

>>> safeFin 1 :: Maybe (Fin 2)
Just 1

>>> safeFin 2 :: Maybe (Fin 2)
Nothing

newtype Fins s

Fins most often represents (finite) indexes for multiple dimensions (of a multi-dimensioned hyper-rectangular array).

Constructors

UnsafeFins

Fields

• fromFins :: [Int]

Instances

Functor (Fins :: Type -> Type)

Defined in Harpie.Shape

Methods

fmap :: (a -> b) -> Fins a -> Fins b

(<$) :: a -> Fins b -> Fins a

Show (Fins n)

Defined in Harpie.Shape

Methods

showsPrec :: Int -> Fins n -> ShowS

show :: Fins n -> String

showList :: [Fins n] -> ShowS

Eq (Fins s)

Defined in Harpie.Shape

Methods

(==) :: Fins s -> Fins s -> Bool

(/=) :: Fins s -> Fins s -> Bool

Ord (Fins s)

Defined in Harpie.Shape

Methods

compare :: Fins s -> Fins s -> Ordering

(<) :: Fins s -> Fins s -> Bool

(<=) :: Fins s -> Fins s -> Bool

(>) :: Fins s -> Fins s -> Bool

(>=) :: Fins s -> Fins s -> Bool

max :: Fins s -> Fins s -> Fins s

min :: Fins s -> Fins s -> Fins s

fins :: forall s. KnownNats s => [Int] -> Fins s

Construct a Fins.

Errors on out-of-bounds

>>> fins @[2,3,4] [1,2,3]
[1,2,3]

>>> fins @[2,3,4] [1,2,5]
*** Exception: value outside bounds
...

safeFins :: forall s. KnownNats s => [Int] -> Maybe (Fins s)

Construct a Fins safely.

>>> safeFins [1,2,3] :: Maybe (Fins [2,3,4])
Just [1,2,3]

>>> safeFins [2] :: Maybe (Fins '[2])
Nothing

Shape Operators at value- and type- level.

rank :: [a] -> Int

Number of dimensions

>>> rank @Int [2,3,4]
3

data Rank :: [a] -> Exp Natural

Number of dimensions

>>> :k! Eval (Rank [2,3,4])
...
= 3

Instances

type Eval (Rank xs :: Natural -> Type)

Defined in Harpie.Shape

type Eval (Rank xs :: Natural -> Type) = Eval (Length xs)

range :: Int -> [Int]

Enumerate a range of rank n

>>> range 0
[]

>>> range 3
[0,1,2]

data Range :: Nat -> Exp [Nat]

Enumerate a range of rank n

>>> :k! Eval (Range 0)
...
= '[]

>>> :k! Eval (Range 3)
...
= [0, 1, 2]

Instances

type Eval (Range x :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (Range x :: [Nat] -> Type) = If (x == 0) ('[] :: [Nat]) (Eval (EnumFromTo 0 (Eval (x - 1))))

rerank :: Int -> [Int] -> [Int]

Create a new rank by adding ones to the left, if the new rank is greater, or combining dimensions (from left to right) into rows, if the new rank is lower.

>>> rerank 4 [2,3,4]
[1,2,3,4]
>>> rerank 2 [2,3,4]
[6,4]

data Rerank :: Nat -> [Nat] -> Exp [Nat]

Create a new rank by adding ones to the left, if the new rank is greater, or combining dimensions (from left to right) into rows, if the new rank is lower.

>>> :k! Eval (Rerank 4 [2,3,4])
...
= [1, 2, 3, 4]
>>> :k! Eval (Rerank 2 [2,3,4])
...
= [6, 4]

Instances

type Eval (Rerank r xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (Rerank r xs :: [Nat] -> Type) = If (Eval (r > Eval (Rank xs))) (Eval (Eval (Replicate (Eval (r - Eval (Rank xs))) 1) ++ xs)) (Eval ('[Eval (Size (Eval (Take (Eval (Eval (Eval (Rank xs) - r) + 1)) xs)))] ++ Eval (Drop (Eval (Eval (Eval (Rank xs) - r) + 1)) xs)))

dimsOf :: [Int] -> [Int]

Enumerate the dimensions of a shape.

dimsOf [2,3,4] [0,1,2]

data DimsOf :: [Nat] -> Exp [Nat]

Enumerate the dimensions of a shape.

>>> :k! Eval (DimsOf [2,3,4])
...
= [0, 1, 2]

Instances

type Eval (DimsOf xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DimsOf xs :: [Nat] -> Type) = Eval (Range =<< Rank xs)

endDimsOf :: [Int] -> [Int] -> [Int]

Enumerate the final dimensions of a shape.

>>> endDimsOf [1,0] [2,3,4]
[2,1]

data EndDimsOf :: [Nat] -> [Nat] -> Exp [Nat]

Enumerate the final dimensions of a shape.

>>> :k! Eval (EndDimsOf [1,0] [2,3,4])
...
= [2, 1]

Instances

type Eval (EndDimsOf xs s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (EndDimsOf xs s :: [Nat] -> Type) = Eval (LiftM2 (Take :: Nat -> [Nat] -> [Nat] -> Type) (Rank xs) ((Reverse :: [Nat] -> [Nat] -> Type) =<< DimsOf s))

size :: [Int] -> Int

Total number of elements (if the list is the shape of a hyper-rectangular array).

>>> size [2,3,4]
24

data Size :: [Nat] -> Exp Nat

Total number of elements (if the list is the shape of a hyper-rectangular array).

>>> :k! (Eval (Size [2,3,4]))
...
= 24

Instances

type Eval (Size xs :: Nat -> Type)

Defined in Harpie.Shape

type Eval (Size xs :: Nat -> Type) = Eval (Foldr * 1 xs)

flatten :: [Int] -> [Int] -> Int

Convert from a n-dimensional shape list index to a flat index, which, technically is the lexicographic position of the position in a row-major array.

>>> flatten [2,3,4] [1,1,1]
17

>>> flatten [] [1,1,1]
0

shapen :: [Int] -> Int -> [Int]

Convert from a flat index to a shape index.

>>> shapen [2,3,4] 17
[1,1,1]

asSingleton :: [Int] -> [Int]

Convert a scalar to a dimensioned shape

>>> asSingleton []
[1]
>>> asSingleton [2,3,4]
[2,3,4]

data AsSingleton :: [Nat] -> Exp [Nat]

Convert a scalar to a dimensioned shape >>> :k! Eval (AsSingleton '[]) ... = '[1] >>> :k! Eval (AsSingleton [2,3,4]) ... = [2, 3, 4]

Instances

type Eval (AsSingleton xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (AsSingleton xs :: [Nat] -> Type) = If (xs == ('[] :: [Nat])) '[1] xs

asScalar :: [Int] -> [Int]

Convert a (potentially) [1] dimensioned shape to a scalar shape

>>> asScalar [1]
[]
>>> asScalar [2,3,4]
[2,3,4]

data AsScalar :: [Nat] -> Exp [Nat]

Convert a (potentially) [1] dimensioned shape to a scalar shape >>> :k! Eval (AsScalar '[1]) ... = '[] >>> :k! Eval (AsScalar [2,3,4]) ... = [2, 3, 4]

Instances

type Eval (AsScalar xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (AsScalar xs :: [Nat] -> Type) = If (xs == '[1]) ('[] :: [Nat]) xs

isSubset :: [Int] -> [Int] -> Bool

Check if a shape is a subset (<=) another shape after reranking.

>>> isSubset [2,3,4] [2,3,4]
True

>>> isSubset [1,2] [2,3,4]
True

>>> isSubset [2,1] [1]
False

data IsSubset :: [Nat] -> [Nat] -> Exp Bool

Check if a shape is a subset (<=) another shape after reranking.

>>> :k! Eval (IsSubset [2,3,4] [2,3,4])
...
= True

>>> :k! Eval (IsSubset [1,2] [2,3,4])
...
= True

>>> :k! Eval (IsSubset [2,1] '[1])
...
= False

Instances

type Eval (IsSubset xs ys :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsSubset xs ys :: Bool -> Type)

exceptDims :: [Int] -> [Int] -> [Int]

Compute dimensions for a shape other than the supplied dimensions.

>>> exceptDims [1,2] [2,3,4]
[0]

data ExceptDims :: [Nat] -> [Nat] -> Exp [Nat]

Compute dimensions for a shape other than the supplied dimensions.

>>> :k! Eval (ExceptDims [1,2] [2,3,4])
...
= '[0]

Instances

type Eval (ExceptDims ds s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (ExceptDims ds s :: [Nat] -> Type) = Eval (DeleteDims ds =<< EnumFromTo 0 (Eval (Eval (Rank s) - 1)))

reorder :: [Int] -> [Int] -> [Int]

Reorder the dimensions of shape according to a list of positions.

>>> reorder [2,3,4] [2,0,1]
[4,2,3]

data Reorder :: [Nat] -> [Nat] -> Exp [Nat]

Reorder the dimensions of shape according to a list of positions.

>>> :k! Eval (Reorder [2,3,4] [2,0,1])
...
= [4, 2, 3]

Instances

type Eval (Reorder ds xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (Reorder ds xs :: [Nat] -> Type) = If (Eval (ReorderOk ds xs)) (Eval (Map (Flip GetDim ds) xs)) (TypeError ('Text "Reorder dimension indices out of bounds") :: [Nat])

data ReorderOk :: [Nat] -> [Nat] -> Exp Bool

Test if a Reorder is valid.

>>> :k! Eval (ReorderOk [2,3,4] [0,1])
...
= False

Instances

type Eval (ReorderOk ds xs :: Bool -> Type)

Defined in Harpie.Shape

type Eval (ReorderOk ds xs :: Bool -> Type) = Eval (TyEq (Eval (Rank ds)) (Eval (Rank xs))) && Eval ((And :: [Bool] -> Bool -> Type) =<< Map (Flip IsFin (Eval (Rank ds))) xs)

squeeze :: [Int] -> [Int]

remove 1's from a list

>>> squeeze [0,1,2,3]
[0,2,3]

data Squeeze :: [a] -> Exp [a]

Remove 1's from a list.

>>> :k! (Eval (Squeeze [0,1,2,3]))
...
= [0, 2, 3]

Instances

type Eval (Squeeze xs :: [a] -> Type)

Defined in Harpie.Shape

type Eval (Squeeze xs :: [a] -> Type) = Eval (Filter (Not <=< (TyEq 1 :: a -> Bool -> Type)) xs)

Primitives

data Min :: a -> a -> Exp a

Minimum of two type values.

>>> :k! Eval (Min 0 1)
...
= 0

Instances

type Eval (Min a b :: k -> Type)

Defined in Harpie.Shape

type Eval (Min a b :: k -> Type) = If (a <? b) a b

data Max :: a -> a -> Exp a

Maximum of two type values.

>>> :k! Eval (Max 0 1)
...
= 1

Instances

type Eval (Max a b :: k -> Type)

Defined in Harpie.Shape

type Eval (Max a b :: k -> Type) = If (a >? b) a b

minimum :: [Int] -> Int

minimum of a list

>>> S.minimum []
*** Exception: zero-ranked
...
>>> S.minimum [2,3,4]
2

data Minimum :: [a] -> Exp a

minimum of a list

>>> :k! Eval (Minimum '[])
...
= (TypeError ...)

>>> :k! Eval (Minimum [2,3,4])
...
= 2

Instances

type Eval (Minimum (x ': xs) :: a -> Type)

Defined in Harpie.Shape

type Eval (Minimum (x ': xs) :: a -> Type) = Eval (Foldr (Min :: a -> a -> a -> Type) x xs)

type Eval (Minimum ('[] :: [a]) :: a -> Type)

Defined in Harpie.Shape

type Eval (Minimum ('[] :: [a]) :: a -> Type) = TypeError ('Text "zero ranked") :: a

Position

isFin :: Int -> Int -> Bool

Check if i is a valid Fin (aka in-bounds index of a dimension)

>>> isFin 0 2
True
>>> isFin 2 2
False

data IsFin :: Nat -> Nat -> Exp Bool

Check if i is a valid Fin (aka in-bounds index of a dimension)

>>> :k! Eval (IsFin 0 2)
...
= True
>>> :k! Eval (IsFin 2 2)
...
= False

Instances

type Eval (IsFin x d :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsFin x d :: Bool -> Type) = x <? d

isFins :: [Int] -> [Int] -> Bool

Check if i is a valid Fins (aka in-bounds index of a Shape)

>>> isFins [0,1] [2,2]
True
>>> isFins [0,1] [2,1]
False

data IsFins :: [Nat] -> [Nat] -> Exp Bool

Check if i is a valid Fins (aka in-bounds index of a Shape)

>>> :k! Eval (IsFins [0,1] [2,2])
...
= True
>>> :k! Eval (IsFins [0,1] [2,1])
...
= False

Instances

type Eval (IsFins xs ds :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsFins xs ds :: Bool -> Type) = Eval (And (Eval (ZipWith IsFin xs ds))) && Eval (LiftM2 (TyEq :: Natural -> Natural -> Bool -> Type) (Rank xs) (Rank ds))

isDim :: Int -> [Int] -> Bool

Is a value a valid dimension of a shape.

>>> isDim 2 [2,3,4]
True
>>> isDim 0 []
True

data IsDim :: Nat -> [Nat] -> Exp Bool

Is a value a valid dimension of a shape.

>>> :k! Eval (IsDim 2 [2,3,4])
...
= True
>>> :k! Eval (IsDim 0 '[])
...
= True

Instances

type Eval (IsDim d s :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsDim d s :: Bool -> Type) = Eval (IsFin d =<< Rank s) || ((0 == d) && (s == ('[] :: [Nat])))

isDims :: [Int] -> [Int] -> Bool

Are values valid dimensions of a shape.

>>> isDims [2,1] [2,3,4]
True
>>> isDims [0] []
True

data IsDims :: [Nat] -> [Nat] -> Exp Bool

Are values valid dimensions of a shape.

>>> :k! Eval (IsDims [2,1] [2,3,4])
...
= True
>>> :k! Eval (IsDims '[0] '[])
...
= True

Instances

type Eval (IsDims ds s :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsDims ds s :: Bool -> Type) = Eval ((And :: [Bool] -> Bool -> Type) =<< Map (Flip IsDim s) ds)

lastPos :: Int -> [Int] -> Int

Get the last position of a dimension of a shape.

>>> lastPos 2 [2,3,4]
3
>>> lastPos 0 []
0

data LastPos :: Nat -> [Nat] -> Exp Nat

Get the last position of a dimension of a shape.

>>> :k! Eval (LastPos 2 [2,3,4])
...
= 3
>>> :k! Eval (LastPos 0 '[])
...
= 0

Instances

type Eval (LastPos d s :: Nat -> Type)

Defined in Harpie.Shape

type Eval (LastPos d s :: Nat -> Type) = If ((0 == d) && (s == ('[] :: [Nat]))) 0 (Eval (GetDim d s) - 1)

minDim :: [Int] -> [Int]

Get the minimum dimension as a singleton dimension.

>>> minDim [2,3,4]
[2]
>>> minDim []
[]

data MinDim :: [Nat] -> Exp [Nat]

Get the minimum dimension as a singleton dimension.

>>> :k! Eval (MinDim [2,3,4])
...
= '[2]
>>> :k! Eval (MinDim '[])
...
= '[]

Instances

type Eval (MinDim s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (MinDim s :: [Nat] -> Type) = If (s == ('[] :: [Nat])) ('[] :: [Nat]) '[Eval (Minimum s)]

combinators

data EnumFromTo :: Nat -> Nat -> Exp [Nat]

Enumerate between two Nats

>>> :k! Eval (EnumFromTo 0 3)
...
= [0, 1, 2, 3]

Instances

type Eval (EnumFromTo a b :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (EnumFromTo a b :: [Nat] -> Type)

data Foldl' :: (b -> a -> Exp b) -> b -> t a -> Exp b

Left fold.

>>> :k! Eval (Foldl' (Fcf.+) 0 [1,2,3])
...
= 6

Instances

type Eval (Foldl' f y (x ': xs) :: a1 -> Type)

Defined in Harpie.Shape

type Eval (Foldl' f y (x ': xs) :: a1 -> Type) = Eval (Foldl' f (Eval (f y x)) xs)

type Eval (Foldl' f y ('[] :: [a2]) :: a1 -> Type)

Defined in Harpie.Shape

type Eval (Foldl' f y ('[] :: [a2]) :: a1 -> Type) = y

single dimension

data GetIndex :: Nat -> [a] -> Exp (Maybe a)

Get an element at a given index.

>>> :kind! Eval (GetIndex 2 [2,3,4])
...
= Just 4

Instances

type Eval (GetIndex d xs :: Maybe k -> Type)

Defined in Harpie.Shape

type Eval (GetIndex d xs :: Maybe k -> Type)

data SetIndex (b :: Nat) (c :: a) (d :: [a]) (e :: [a])

Modify an element at a given index.

The list is unchanged if the index is out of bounds.

Example

>>> :kind! Eval (SetIndex 2 7 [1,2,3])
Eval (SetIndex 2 7 [1,2,3]) :: [Natural]
= [1, 2, 7]

Instances

type Eval (SetIndex n a' as :: [k] -> Type)

Defined in Fcf.Data.List

type Eval (SetIndex n a' as :: [k] -> Type) = SetIndexImpl n a' as

getDim :: Int -> [Int] -> Int

Get the dimension of a shape at the supplied index. Error if out-of-bounds.

>>> getDim 1 [2,3,4]
3
>>> getDim 3 [2,3,4]
*** Exception: getDim outside bounds
...
>>> getDim 0 []
1

data GetDim :: Nat -> [Nat] -> Exp Nat

Get the dimension of a shape at the supplied index. Error if out-of-bounds or non-computable (usually unknown to the compiler).

>>> :k! Eval (GetDim 1 [2,3,4])
...
= 3
>>> :k! Eval (GetDim 3 [2,3,4])
...
= (TypeError ...)
>>> :k! Eval (GetDim 0 '[])
...
= 1

Instances

type Eval (GetDim n xs :: Nat -> Type)

Defined in Harpie.Shape

type Eval (GetDim n xs :: Nat -> Type) = If (Eval (And '[Eval (TyEq n 0), Eval (TyEq xs ('[] :: [Nat]))])) 1 (Eval (FromMaybe (TypeError ((('Text "GetDim out of bounds or non-computable: " ':<>: 'ShowType n) ':<>: 'Text " ") ':<>: 'ShowType xs) :: Nat) (Eval (GetIndex n xs))))

modifyDim :: Int -> (Int -> Int) -> [Int] -> [Int]

modify an index at a specific dimension. Errors if out of bounds.

>>> modifyDim 0 (+1) [0,1,2]
[1,1,2]
>>> modifyDim 0 (+1) []
[2]

data ModifyDim :: Nat -> (Nat -> Exp Nat) -> [Nat] -> Exp [Nat]

modify an index at a specific dimension. Errors if out of bounds.

>>> :k! Eval (ModifyDim 0 ((Fcf.+) 1) [0,1,2])
...
= [1, 1, 2]

Instances

type Eval (ModifyDim d f s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (ModifyDim d f s :: [Nat] -> Type) = Eval (LiftM2 ((++) :: [Nat] -> [Nat] -> [Nat] -> Type) (Take d s) (LiftM2 (Cons :: Nat -> [Nat] -> [Nat] -> Type) (f =<< GetDim d s) (Drop (d + 1) s)))

incAt :: Int -> [Int] -> [Int]

Increment the index at a dimension of a shape by 1. Scalars turn into singletons.

>>> incAt 1 [2,3,4]
[2,4,4]
>>> incAt 0 []
[2]

data IncAt :: Nat -> [Nat] -> Exp [Nat]

Increment the index at a dimension of a shape by 1. Scalars turn into singletons.

>>> :k! Eval (IncAt 1 [2,3,4])
...
= [2, 4, 4]
>>> :k! Eval (IncAt 0 '[])
...
= '[2]

Instances

type Eval (IncAt d ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (IncAt d ds :: [Nat] -> Type) = Eval (ModifyDim d ((+) 1) (Eval (AsSingleton ds)))

decAt :: Int -> [Int] -> [Int]

Decrement the index at a dimension os a shape by 1.

>>> decAt 1 [2,3,4]
[2,2,4]

data DecAt :: Nat -> [Nat] -> Exp [Nat]

Decrement the index at a dimension of a shape by 1.

>>> :k! Eval (DecAt 1 [2,3,4])
...
= [2, 2, 4]

Instances

type Eval (DecAt d ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DecAt d ds :: [Nat] -> Type) = Eval (ModifyDim d (Flip (-) 1) ds)

setDim :: Int -> Int -> [Int] -> [Int]

replace an index at a specific dimension, or transform a scalar into being 1-dimensional.

>>> setDim 0 1 [2,3,4]
[1,3,4]
>>> setDim 0 3 []
[3]

data SetDim :: Nat -> Nat -> [Nat] -> Exp [Nat]

replace an index at a specific dimension.

>>> :k! Eval (SetDim 0 1 [2,3,4])
...
= [1, 3, 4]

Instances

type Eval (SetDim d x ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (SetDim d x ds :: [Nat] -> Type) = Eval (ModifyDim d (ConstFn x :: Nat -> Nat -> Type) ds)

takeDim :: Int -> Int -> [Int] -> [Int]

Take along a dimension.

>>> takeDim 0 1 [2,3,4]
[1,3,4]

data TakeDim :: Nat -> Nat -> [Nat] -> Exp [Nat]

Take along a dimension.

>>> :k! Eval (TakeDim 0 1 [2,3,4])
...
= [1, 3, 4]

Instances

type Eval (TakeDim d t s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (TakeDim d t s :: [Nat] -> Type) = Eval (ModifyDim d (Min t) s)

dropDim :: Int -> Int -> [Int] -> [Int]

Drop along a dimension.

>>> dropDim 2 1 [2,3,4]
[2,3,3]

data DropDim :: Nat -> Nat -> [Nat] -> Exp [Nat]

Drop along a dimension.

>>> :k! Eval (DropDim 2 1 [2,3,4])
...
= [2, 3, 3]

Instances

type Eval (DropDim d t s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DropDim d t s :: [Nat] -> Type) = Eval (ModifyDim d (Max 0 <=< Flip (-) t) s)

deleteDim :: Int -> [Int] -> [Int]

delete the i'th dimension. No effect on a scalar.

>>> deleteDim 1 [2, 3, 4]
[2,4]
>>> deleteDim 2 []
[]

data DeleteDim :: Nat -> [Nat] -> Exp [Nat]

delete the i'th dimension

>>> :k! Eval (DeleteDim 1 [2, 3, 4])
...
= [2, 4]
>>> :k! Eval (DeleteDim 1 '[])
...
= '[]

Instances

type Eval (DeleteDim i ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DeleteDim i ds :: [Nat] -> Type) = Eval (LiftM2 ((++) :: [Nat] -> [Nat] -> [Nat] -> Type) (Take i ds) (Drop (i + 1) ds))

insertDim :: Int -> Int -> [Int] -> [Int]

Insert a new dimension at a position (or at the end if > rank).

>>> insertDim 1 3 [2,4]
[2,3,4]
>>> insertDim 0 4 []
[4]

data InsertDim :: Nat -> Nat -> [Nat] -> Exp [Nat]

Insert a new dimension at a position (or at the end if > rank).

>>> :k! Eval (InsertDim 1 3 [2,4])
...
= [2, 3, 4]
>>> :k! Eval (InsertDim 0 4 '[])
...
= '[4]

Instances

type Eval (InsertDim d i ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (InsertDim d i ds :: [Nat] -> Type) = Eval (LiftM2 ((++) :: [Nat] -> [Nat] -> [Nat] -> Type) (Take d ds) (Cons i =<< Drop d ds))

data InsertOk :: Nat -> [Nat] -> [Nat] -> Exp Bool

Is a slice ok constraint.

>>> :k! Eval (InsertOk 2 [2,3,4] [2,3])
...
= True
>>> :k! Eval (InsertOk 0 '[] '[])
...
= True

Instances

type Eval (InsertOk d s si :: Bool -> Type)

Defined in Harpie.Shape

type Eval (InsertOk d s si :: Bool -> Type) = Eval (And '[Eval (IsDim d s), Eval (TyEq si (Eval (DeleteDim d s)))])

data SliceOk :: Nat -> Nat -> Nat -> [Nat] -> Exp Bool

Is a slice ok?

>>> :k! Eval (SliceOk 1 1 2 [2,3,4])
...
= True

Instances

type Eval (SliceOk d off l s :: Bool -> Type)

Defined in Harpie.Shape

type Eval (SliceOk d off l s :: Bool -> Type) = Eval (And '[Eval (IsFin off =<< GetDim d s), Eval ((<) l =<< GetDim d s), Eval ((off + l) < (Eval (GetDim d s) + 1)), Eval (IsDim d s)])

data SlicesOk :: [Nat] -> [Nat] -> [Nat] -> [Nat] -> Exp Bool

Are slices ok?

>>> :k! Eval (SlicesOk '[1] '[1] '[2] [2,3,4])
...
= True

Instances

type Eval (SlicesOk ds offs ls s :: Bool -> Type)

Defined in Harpie.Shape

type Eval (SlicesOk ds offs ls s :: Bool -> Type)

concatenate :: Int -> [Int] -> [Int] -> [Int]

concatenate two arrays at dimension i

Bespoke logic for scalars.

>>> concatenate 1 [2,3,4] [2,3,4]
[2,6,4]
>>> concatenate 0 [3] []
[4]
>>> concatenate 0 [] [3]
[4]
>>> concatenate 0 [] []
[2]

data Concatenate :: Nat -> [Nat] -> [Nat] -> Exp [Nat]

concatenate two arrays at dimension i

Bespoke logic for scalars.

>>> :k! Eval (Concatenate 1 [2,3,4] [2,3,4])
...
= [2, 6, 4]
>>> :k! Eval (Concatenate 0 '[3] '[])
...
= '[4]
>>> :k! Eval (Concatenate 0 '[] '[3])
...
= '[4]
>>> :k! Eval (Concatenate 0 '[] '[])
...
= '[2]

Instances

type Eval (Concatenate i s0 s1 :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (Concatenate i s0 s1 :: [Nat] -> Type) = If (Eval (ConcatenateOk i s0 s1)) (Eval (Eval (Take i s0) ++ ((Eval (GetDim i s0) + Eval (GetDim i s1)) ': Eval (Drop (i + 1) s0)))) (TypeError ('Text "Concatenate Mis-matched shapes.") :: [Nat])

data ConcatenateOk :: Nat -> [Nat] -> [Nat] -> Exp Bool

Concatenate is Ok if ranks are the same and the non-indexed portion of the shapes are the same.

Instances

type Eval (ConcatenateOk i s0 s1 :: Bool -> Type)

Defined in Harpie.Shape

type Eval (ConcatenateOk i s0 s1 :: Bool -> Type) = Eval (IsDim i s0) && (Eval (IsDim i s1) && (Eval (LiftM2 (TyEq :: [Nat] -> [Nat] -> Bool -> Type) (DeleteDim i s0) (DeleteDim i s1)) && Eval (LiftM2 (TyEq :: Natural -> Natural -> Bool -> Type) ((Rank :: [Nat] -> Natural -> Type) =<< AsSingleton s0) ((Rank :: [Nat] -> Natural -> Type) =<< AsSingleton s1))))

multiple dimension

getDims :: [Int] -> [Int] -> [Int]

Get dimensions of a shape.

>>> getDims [2,0] [2,3,4]
[4,2]
>>> getDims [2] []
[]

data GetDims :: [Nat] -> [Nat] -> Exp [Nat]

Get dimensions of a shape.

>>> :k! Eval (GetDims [2,0] [2,3,4])
...
= [4, 2]
>>> :k! Eval (GetDims '[2] '[])
...
= '[(TypeError ...)]

Instances

type Eval (GetDims xs ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (GetDims xs ds :: [Nat] -> Type) = Eval (Map (Flip GetDim ds) xs)

getLastPositions :: [Int] -> [Int] -> [Int]

Get the index of the last position in the selected dimensions of a shape. Errors on a 0-dimension.

>>> getLastPositions [2,0] [2,3,4]
[3,1]
>>> getLastPositions [0] [0]
[-1]

data GetLastPositions :: [Nat] -> [Nat] -> Exp [Nat]

Get the index of the last position in the selected dimensions of a shape. Errors on a 0-dimension.

>>> :k! Eval (GetLastPositions [2,0] [2,3,4])
...
= [3, 1]

Instances

type Eval (GetLastPositions ds s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (GetLastPositions ds s :: [Nat] -> Type) = Eval (Map (Flip (-) 1) (Eval (GetDims ds s)))

modifyDims :: [Int] -> [Int -> Int] -> [Int] -> [Int]

modify dimensions of a shape with (separate) functions.

>>> modifyDims [0,1] [(+1), (+5)] [2,3,4]
[3,8,4]

insertDims :: [Int] -> [Int] -> [Int] -> [Int]

Insert a list of dimensions according to dimensions and positions. Note that the list of positions references the final shape and not the initial shape.

>>> insertDims [0] [5] []
[5]
>>> insertDims [1,0] [3,2] [4]
[2,3,4]

data InsertDims :: [Nat] -> [Nat] -> [Nat] -> Exp [Nat]

insert a list of dimensions according to dimension,position tuple lists. Note that the list of positions references the final shape and not the initial shape.

>>> :k! Eval (InsertDims '[0] '[5] '[])
...
= '[5]
>>> :k! Eval (InsertDims [1,0] [3,2] '[4])
...
= [2, 3, 4]

Instances

type Eval (InsertDims ds xs s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (InsertDims ds xs s :: [Nat] -> Type)

preDeletePositions :: [Int] -> [Int]

Convert a list of positions that reference deletions according to a final shape to 1 that references deletions relative to an initial shape.

To delete the positions [1,2,5] from a list, for example, you need to delete position 1, (arriving at a 4 element list), then position 1, arriving at a 3 element list, and finally position 3.

>>> preDeletePositions [1,2,5]
[1,1,3]

>>> preDeletePositions [1,2,0]
[1,1,0]

data PreDeletePositions :: [Nat] -> Exp [Nat]

Convert a list of positions that reference deletions according to a final shape to 1 that references deletions relative to an initial shape.

To delete the positions [1,2,5] from a list, for example, you need to delete position 1, (arriving at a 4 element list), then position 1, arriving at a 3 element list, and finally position 3.

>>> :k! Eval (PreDeletePositions [1,2,5])
...
= [1, 1, 3]

>>> :k! Eval (PreDeletePositions [1,2,0])
...
= [1, 1, 0]

Instances

type Eval (PreDeletePositions xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (PreDeletePositions xs :: [Nat] -> Type)

preInsertPositions :: [Int] -> [Int]

Convert a list of position that reference insertions according to a final shape to 1 that references list insertions relative to an initial shape.

To insert into positions [1,2,0] from a list, starting from a 2 element list, for example, you need to insert at position 0, (arriving at a 3 element list), then position 1, arriving at a 4 element list, and finally position 0.

 preInsertPositions == reverse . preDeletePositions . reverse
>> preInsertPositions [1,2,5]

1,2,5

>>> preInsertPositions [1,2,0]
[0,1,0]

data PreInsertPositions :: [Nat] -> Exp [Nat]

Convert a list of position that reference insertions according to a final shape to 1 that references list insertions relative to an initial shape.

To insert into positions [1,2,0] from a list, starting from a 2 element list, for example, you need to insert at position 0, (arriving at a 3 element list), then position 1, arriving at a 4 element list, and finally position 0.

 preInsertPositions == reverse . preDeletePositions . reverse
>> :k! Eval (PreInsertPositions [1,2,5])

... = [1, 2, 5]

>>> :k! Eval (PreInsertPositions [1,2,0])
...
= [0, 1, 0]

Instances

type Eval (PreInsertPositions xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (PreInsertPositions xs :: [Nat] -> Type) = Eval ((Reverse :: [Nat] -> [Nat] -> Type) =<< (PreDeletePositions =<< Reverse xs))

setDims :: [Int] -> [Int] -> [Int] -> [Int]

Set dimensions of a shape.

>>> setDims [0,1] [1,5] [2,3,4]
[1,5,4]

>>> setDims [0] [3] []
[3]

data SetDims :: [Nat] -> [Nat] -> [Nat] -> Exp [Nat]

Set dimensions of a shape.

>>> :k! Eval (SetDims [0,1] [1,5] [2,3,4])
...
= [1, 5, 4]

>>> :k! Eval (SetDims '[0] '[3] '[])
...
= '[3]

Instances

type Eval (SetDims ds xs ns :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (SetDims ds xs ns :: [Nat] -> Type)

deleteDims :: [Int] -> [Int] -> [Int]

drop dimensions of a shape according to a list of positions (where position refers to the initial shape)

>>> deleteDims [1,0] [2, 3, 4]
[4]

data DeleteDims :: [Nat] -> [Nat] -> Exp [Nat]

drop dimensions of a shape according to a list of positions (where position refers to the initial shape)

>>> :k! Eval (DeleteDims [1,0] [2, 3, 4])
...
= '[4]

Instances

type Eval (DeleteDims xs ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DeleteDims xs ds :: [Nat] -> Type) = Eval ((Foldl' (Flip DeleteDim) ds :: [Nat] -> [Nat] -> Type) =<< PreDeletePositions xs)

dropDims :: [Int] -> [Int] -> [Int] -> [Int]

Drop a number of elements of a shape along the supplied dimensions.

>>> dropDims [0,2] [1,3] [2,3,4]
[1,3,1]

data DropDims :: [Nat] -> [Nat] -> [Nat] -> Exp [Nat]

Drop a number of elements of a shape along the supplied dimensions.

>>> :k! Eval (DropDims [0,2] [1,3] [2,3,4])
...
= [1, 3, 1]

Instances

type Eval (DropDims ds xs s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DropDims ds xs s :: [Nat] -> Type) = Eval (SetDims ds (Eval (ZipWith (-) (Eval (GetDims ds s)) xs)) s)

concatDims :: [Int] -> Int -> [Int] -> [Int]

Concatenate and replace dimensions, creating a new dimension at the supplied postion.

>>> concatDims [0,1] 1 [2,3,4]
[4,6]

data ConcatDims :: [Nat] -> Nat -> [Nat] -> Exp [Nat]

Drop a number of elements of a shape along the supplied dimensions.

>>> :k! Eval (ConcatDims [0,1] 1 [2,3,4])
...
= [4, 6]

Instances

type Eval (ConcatDims ds n s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (ConcatDims ds n s :: [Nat] -> Type) = Eval (InsertDim n (Eval (Size (Eval (GetDims ds s)))) (Eval (DeleteDims ds s)))

value-only operations

unconcatDimsIndex :: [Int] -> Int -> [Int] -> [Int] -> [Int]

Unconcatenate and reinsert dimensions for an index.

>>> unconcatDimsIndex [0,1] 1 [4,6] [2,3]
[0,3,2]

reverseIndex :: [Int] -> [Int] -> [Int] -> [Int]

reverse an index along specific dimensions.

>>> reverseIndex [0] [2,3,4] [0,1,2]
[1,1,2]

rotate :: Int -> [a] -> [a]

rotate a list

>>> rotate 1 [0..3]
[1,2,3,0]
>>> rotate (-1) [0..3]
[3,0,1,2]

rotateIndex :: Int -> Int -> [Int] -> [Int] -> [Int]

rotate an index along a specific dimension.

>>> rotateIndex 0 1 [2,3,4] [0,1,2]
[1,1,2]

rotatesIndex :: [Int] -> [Int] -> [Int] -> [Int] -> [Int]

rotate an index along specific dimensions.

>>> rotatesIndex [0] [1] [2,3,4] [0,1,2]
[1,1,2]

isDiag :: Eq a => [a] -> Bool

Test whether an index is a diagonal one.

>>> isDiag [2,2,2]
True
>>> isDiag [1,2]
False

windowed

expandWindows :: [Int] -> [Int] -> [Int]

Expanded shape of a windowed array

>>> expandWindows [2,2] [4,3,2]
[3,2,2,2,2]

data ExpandWindows :: [Nat] -> [Nat] -> Exp [Nat]

Expanded shape of a windowed array

>>> :k! Eval (ExpandWindows [2,2] [4,3,2])
...
= [3, 2, 2, 2, 2]

Instances

type Eval (ExpandWindows ws ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (ExpandWindows ws ds :: [Nat] -> Type) = Eval (Eval (ZipWith (-) (Eval (Map ((+) 1) ds)) ws) ++ Eval (ws ++ Eval (Drop (Eval (Rank ws)) ds)))

indexWindows :: Int -> [Int] -> [Int]

Index into windows of an expanded windowed array, given a rank of the windows.

>>> indexWindows 2 [0,1,2,1,1]
[2,2,1]

dimWindows :: [Int] -> [Int] -> [Int]

Dimensions of a windowed array.

>>> dimWindows [2,2] [2,3,4]
[0,1,2]

data DimWindows :: [Nat] -> [Nat] -> Exp [Nat]

Dimensions of a windowed array.

>>> :k! Eval (DimWindows [2,2] [4,3,2])
...
= [0, 1, 2]

Instances

type Eval (DimWindows ws s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DimWindows ws s :: [Nat] -> Type) = Eval (Eval (Range =<< Rank s) ++ Eval (EnumFromTo (Eval (2 * Eval (Rank s))) (Eval (Rank ws) - 1)))

Fcf re-exports

type family Eval (e :: Exp a) :: a

Expression evaluator.

Instances

type Eval (Size xs :: Nat -> Type)

Defined in Harpie.Shape

type Eval (Size xs :: Nat -> Type) = Eval (Foldr * 1 xs)

type Eval (Not 'False)

Defined in Fcf.Data.Bool

type Eval (Not 'False) = 'True

type Eval (Not 'True)

Defined in Fcf.Data.Bool

type Eval (Not 'True) = 'False

type Eval (Constraints (a ': as) :: Constraint -> Type)

Defined in Fcf.Utils

type Eval (Constraints (a ': as) :: Constraint -> Type) = (a, Eval (Constraints as))

type Eval (Constraints ('[] :: [Constraint]))

Defined in Fcf.Utils

type Eval (Constraints ('[] :: [Constraint])) = ()

type Eval (MEmpty_ :: a -> Type)

Defined in Fcf.Class.Monoid

type Eval (MEmpty_ :: a -> Type) = MEmpty :: a

type Eval (Sum ns :: Nat -> Type)

Defined in Fcf.Class.Foldable

type Eval (Sum ns :: Nat -> Type) = Eval (Foldr (+) 0 ns)

type Eval (Length ('[] :: [a]) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length ('[] :: [a]) :: Nat -> Type) = 0

type Eval (Length (a2 ': as) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)

type Eval (a * b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a * b :: Nat -> Type) = a * b

type Eval (a + b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a + b :: Nat -> Type) = a + b

type Eval (a - b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a - b :: Nat -> Type) = a - b

type Eval (a ^ b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a ^ b :: Nat -> Type) = a ^ b

type Eval (GetDim n xs :: Nat -> Type)

Defined in Harpie.Shape

type Eval (GetDim n xs :: Nat -> Type) = If (Eval (And '[Eval (TyEq n 0), Eval (TyEq xs ('[] :: [Nat]))])) 1 (Eval (FromMaybe (TypeError ((('Text "GetDim out of bounds or non-computable: " ':<>: 'ShowType n) ':<>: 'Text " ") ':<>: 'ShowType xs) :: Nat) (Eval (GetIndex n xs))))

type Eval (LastPos d s :: Nat -> Type)

Defined in Harpie.Shape

type Eval (LastPos d s :: Nat -> Type) = If ((0 == d) && (s == ('[] :: [Nat]))) 0 (Eval (GetDim d s) - 1)

type Eval (Rank xs :: Natural -> Type)

Defined in Harpie.Shape

type Eval (Rank xs :: Natural -> Type) = Eval (Length xs)

type Eval (And lst :: Bool -> Type)

Defined in Fcf.Class.Foldable

type Eval (And lst :: Bool -> Type) = Eval (Foldr (&&) 'True lst)

type Eval (Or lst :: Bool -> Type)

Defined in Fcf.Class.Foldable

type Eval (Or lst :: Bool -> Type) = Eval (Foldr (||) 'False lst)

type Eval ('False && b :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval ('False && b :: Bool -> Type) = 'False

type Eval ('True && b :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval ('True && b :: Bool -> Type) = b

type Eval (a && 'False :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (a && 'False :: Bool -> Type) = 'False

type Eval (a && 'True :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (a && 'True :: Bool -> Type) = a

type Eval ('False || b :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval ('False || b :: Bool -> Type) = b

type Eval ('True || b :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval ('True || b :: Bool -> Type) = 'True

type Eval (a || 'False :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (a || 'False :: Bool -> Type) = a

type Eval (a || 'True :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (a || 'True :: Bool -> Type) = 'True

type Eval (IsJust ('Just _a) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsJust ('Just _a) :: Bool -> Type) = 'True

type Eval (IsJust ('Nothing :: Maybe a) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsJust ('Nothing :: Maybe a) :: Bool -> Type) = 'False

type Eval (IsNothing ('Just _a) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsNothing ('Just _a) :: Bool -> Type) = 'False

type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsNothing ('Nothing :: Maybe a) :: Bool -> Type) = 'True

type Eval (Null ('[] :: [a]) :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Null ('[] :: [a]) :: Bool -> Type) = 'True

type Eval (Null (a2 ': as) :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Null (a2 ': as) :: Bool -> Type) = 'False

type Eval (a < b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a < b :: Bool -> Type) = Eval (Not =<< (a >= b))

type Eval (a <= b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a <= b :: Bool -> Type) = a <=? b

type Eval (a > b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a > b :: Bool -> Type) = Eval (Not =<< (a <= b))

type Eval (a >= b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a >= b :: Bool -> Type) = b <=? a

type Eval (IsDim d s :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsDim d s :: Bool -> Type) = Eval (IsFin d =<< Rank s) || ((0 == d) && (s == ('[] :: [Nat])))

type Eval (IsDims ds s :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsDims ds s :: Bool -> Type) = Eval ((And :: [Bool] -> Bool -> Type) =<< Map (Flip IsDim s) ds)

type Eval (IsFin x d :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsFin x d :: Bool -> Type) = x <? d

type Eval (IsFins xs ds :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsFins xs ds :: Bool -> Type) = Eval (And (Eval (ZipWith IsFin xs ds))) && Eval (LiftM2 (TyEq :: Natural -> Natural -> Bool -> Type) (Rank xs) (Rank ds))

type Eval (IsSubset xs ys :: Bool -> Type)

Defined in Harpie.Shape

type Eval (IsSubset xs ys :: Bool -> Type)

type Eval (ReorderOk ds xs :: Bool -> Type)

Defined in Harpie.Shape

type Eval (ReorderOk ds xs :: Bool -> Type) = Eval (TyEq (Eval (Rank ds)) (Eval (Rank xs))) && Eval ((And :: [Bool] -> Bool -> Type) =<< Map (Flip IsFin (Eval (Rank ds))) xs)

type Eval (Join e :: a -> Type)

Defined in Fcf.Combinators

type Eval (Join e :: a -> Type) = Eval (Eval e)

type Eval (Pure x :: a -> Type)

Defined in Fcf.Combinators

type Eval (Pure x :: a -> Type) = x

type Eval (Error msg :: a -> Type)

Defined in Fcf.Utils

type Eval (Error msg :: a -> Type) = TypeError ('Text msg) :: a

type Eval (TError msg :: a -> Type)

Defined in Fcf.Utils

type Eval (TError msg :: a -> Type) = TypeError msg :: a

type Eval (Minimum (x ': xs) :: a -> Type)

Defined in Harpie.Shape

type Eval (Minimum (x ': xs) :: a -> Type) = Eval (Foldr (Min :: a -> a -> a -> Type) x xs)

type Eval (Minimum ('[] :: [a]) :: a -> Type)

Defined in Harpie.Shape

type Eval (Minimum ('[] :: [a]) :: a -> Type) = TypeError ('Text "zero ranked") :: a

type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsLeft ('Left _a :: Either a b) :: Bool -> Type) = 'True

type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsLeft ('Right _a :: Either a b) :: Bool -> Type) = 'False

type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsRight ('Left _a :: Either a b) :: Bool -> Type) = 'False

type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsRight ('Right _a :: Either a b) :: Bool -> Type) = 'True

type Eval (Elem a2 as :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Elem a2 as :: Bool -> Type) = Eval ((IsJust :: Maybe Nat -> Bool -> Type) =<< FindIndex (TyEq a2 :: a1 -> Bool -> Type) as)

type Eval (IsInfixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsInfixOf xs ys :: Bool -> Type) = Eval ((Any (IsPrefixOf xs) :: [[a]] -> Bool -> Type) =<< Tails ys)

type Eval (IsPrefixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsPrefixOf xs ys :: Bool -> Type) = IsPrefixOf_ xs ys

type Eval (IsSuffixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsSuffixOf xs ys :: Bool -> Type) = Eval (IsPrefixOf ((Reverse :: [a] -> [a] -> Type) @@ xs) ((Reverse :: [a] -> [a] -> Type) @@ ys))

type Eval (ConcatenateOk i s0 s1 :: Bool -> Type)

Defined in Harpie.Shape

type Eval (ConcatenateOk i s0 s1 :: Bool -> Type) = Eval (IsDim i s0) && (Eval (IsDim i s1) && (Eval (LiftM2 (TyEq :: [Nat] -> [Nat] -> Bool -> Type) (DeleteDim i s0) (DeleteDim i s1)) && Eval (LiftM2 (TyEq :: Natural -> Natural -> Bool -> Type) ((Rank :: [Nat] -> Natural -> Type) =<< AsSingleton s0) ((Rank :: [Nat] -> Natural -> Type) =<< AsSingleton s1))))

type Eval (InsertOk d s si :: Bool -> Type)

Defined in Harpie.Shape

type Eval (InsertOk d s si :: Bool -> Type) = Eval (And '[Eval (IsDim d s), Eval (TyEq si (Eval (DeleteDim d s)))])

type Eval (Concat xs :: a -> Type)

Defined in Fcf.Class.Foldable

type Eval (Concat xs :: a -> Type) = Eval (FoldMap (Pure :: a -> a -> Type) xs)

type Eval (x .<> y :: a -> Type)

Defined in Fcf.Class.Monoid

type Eval (x .<> y :: a -> Type) = x <> y

type Eval (FromMaybe _a ('Just b) :: a -> Type)

Defined in Fcf.Data.Common

type Eval (FromMaybe _a ('Just b) :: a -> Type) = b

type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (FromMaybe a2 ('Nothing :: Maybe a1) :: a1 -> Type) = a2

type Eval (Fst '(a2, _b) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (Fst '(a2, _b) :: a1 -> Type) = a2

type Eval (Snd '(_a, b) :: a2 -> Type)

Defined in Fcf.Data.Common

type Eval (Snd '(_a, b) :: a2 -> Type) = b

type Eval (Max a b :: k -> Type)

Defined in Harpie.Shape

type Eval (Max a b :: k -> Type) = If (a >? b) a b

type Eval (Min a b :: k -> Type)

Defined in Harpie.Shape

type Eval (Min a b :: k -> Type) = If (a <? b) a b

type Eval (All p lst :: Bool -> Type)

Defined in Fcf.Class.Foldable

type Eval (All p lst :: Bool -> Type) = Eval (Foldr (Bicomap p (Pure :: Bool -> Bool -> Type) (&&)) 'True lst)

type Eval (Any p lst :: Bool -> Type)

Defined in Fcf.Class.Foldable

type Eval (Any p lst :: Bool -> Type) = Eval (Foldr (Bicomap p (Pure :: Bool -> Bool -> Type) (||)) 'False lst)

type Eval (TyEq a b :: Bool -> Type)

Defined in Fcf.Utils

type Eval (TyEq a b :: Bool -> Type) = TyEqImpl a b

type Eval (SliceOk d off l s :: Bool -> Type)

Defined in Harpie.Shape

type Eval (SliceOk d off l s :: Bool -> Type) = Eval (And '[Eval (IsFin off =<< GetDim d s), Eval ((<) l =<< GetDim d s), Eval ((off + l) < (Eval (GetDim d s) + 1)), Eval (IsDim d s)])

type Eval (SlicesOk ds offs ls s :: Bool -> Type)

Defined in Harpie.Shape

type Eval (SlicesOk ds offs ls s :: Bool -> Type)

type Eval (UnBool fal tru 'False :: a -> Type)

Defined in Fcf.Data.Bool

type Eval (UnBool fal tru 'False :: a -> Type) = Eval fal

type Eval (UnBool fal tru 'True :: a -> Type)

Defined in Fcf.Data.Bool

type Eval (UnBool fal tru 'True :: a -> Type) = Eval tru

type Eval (ConstFn a2 _b :: a1 -> Type)

Defined in Fcf.Combinators

type Eval (ConstFn a2 _b :: a1 -> Type) = a2

type Eval (f $ a3 :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (f $ a3 :: a2 -> Type) = Eval (f a3)

type Eval (f <$> e :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (f <$> e :: a2 -> Type) = f (Eval e)

type Eval (f <*> e :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)

type Eval (k =<< e :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (k =<< e :: a2 -> Type) = Eval (k (Eval e))

type Eval (e >>= k :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (e >>= k :: a2 -> Type) = Eval (k (Eval e))

type Eval (Pure1 f x :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (Pure1 f x :: a2 -> Type) = f x

type Eval (x & f :: a2 -> Type)

Defined in Fcf.Data.Function

type Eval (x & f :: a2 -> Type) = Eval (f x)

type Eval (Case ms a :: k -> Type)

Defined in Fcf.Utils

type Eval (Case ms a :: k -> Type) = Case_ ms a

type Eval (UnMaybe y f ('Just x) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (UnMaybe y f ('Just x) :: a1 -> Type) = Eval (f x)

type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (UnMaybe y f ('Nothing :: Maybe a2) :: a1 -> Type) = Eval y

type Eval (UnList y f xs :: a1 -> Type)

Defined in Fcf.Data.List

type Eval (UnList y f xs :: a1 -> Type) = Eval (Foldr f y xs)

type Eval (FoldMap f ('Left _a :: Either a3 a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('Left _a :: Either a3 a1) :: a2 -> Type) = MEmpty :: a2

type Eval (FoldMap f ('Right x :: Either a3 a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('Right x :: Either a3 a1) :: a2 -> Type) = Eval (f x)

type Eval (FoldMap f ('Just x) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('Just x) :: a2 -> Type) = Eval (f x)

type Eval (FoldMap f ('Nothing :: Maybe a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('Nothing :: Maybe a1) :: a2 -> Type) = MEmpty :: a2

type Eval (FoldMap f (x ': xs) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f (x ': xs) :: a2 -> Type) = Eval (f x) <> Eval (FoldMap f xs)

type Eval (FoldMap f ('[] :: [a1]) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('[] :: [a1]) :: a2 -> Type) = MEmpty :: a2

type Eval (Uncurry f '(x, y) :: a2 -> Type)

Defined in Fcf.Data.Common

type Eval (Uncurry f '(x, y) :: a2 -> Type) = Eval (f x y)

type Eval (Foldl' f y (x ': xs) :: a1 -> Type)

Defined in Harpie.Shape

type Eval (Foldl' f y (x ': xs) :: a1 -> Type) = Eval (Foldl' f (Eval (f y x)) xs)

type Eval (Foldl' f y ('[] :: [a2]) :: a1 -> Type)

Defined in Harpie.Shape

type Eval (Foldl' f y ('[] :: [a2]) :: a1 -> Type) = y

type Eval (Foldr f y ('Left _a :: Either a3 a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ('Left _a :: Either a3 a1) :: a2 -> Type) = y

type Eval (Foldr f y ('Right x :: Either a3 a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ('Right x :: Either a3 a1) :: a2 -> Type) = Eval (f x y)

type Eval (Foldr f y ('Just x) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ('Just x) :: a2 -> Type) = Eval (f x y)

type Eval (Foldr f y ('Nothing :: Maybe a1) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ('Nothing :: Maybe a1) :: a2 -> Type) = y

type Eval (Foldr f y (x ': xs) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y (x ': xs) :: a2 -> Type) = Eval (f x (Eval (Foldr f y xs)))

type Eval (Foldr f y ('[] :: [a1]) :: a2 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ('[] :: [a1]) :: a2 -> Type) = y

type Eval ((f <=< g) x :: a2 -> Type)

Defined in Fcf.Combinators

type Eval ((f <=< g) x :: a2 -> Type) = Eval (f (Eval (g x)))

type Eval (Flip f y x :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (Flip f y x :: a2 -> Type) = Eval (f x y)

type Eval (Pure2 f x y :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (Pure2 f x y :: a2 -> Type) = f x y

type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type)

Defined in Fcf.Data.Common

type Eval (UnEither f g ('Left x :: Either a1 b) :: a2 -> Type) = Eval (f x)

type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type)

Defined in Fcf.Data.Common

type Eval (UnEither f g ('Right y :: Either a1 b) :: a2 -> Type) = Eval (g y)

type Eval (LiftM2 f x y :: a3 -> Type)

Defined in Fcf.Combinators

type Eval (LiftM2 f x y :: a3 -> Type) = Eval (f (Eval x) (Eval y))

type Eval (On r f x y :: a2 -> Type)

Defined in Fcf.Data.Function

type Eval (On r f x y :: a2 -> Type) = Eval (r (Eval (f x)) (Eval (f y)))

type Eval (Pure3 f x y z :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (Pure3 f x y z :: a2 -> Type) = f x y z

type Eval (LiftM3 f x y z :: a4 -> Type)

Defined in Fcf.Combinators

type Eval (LiftM3 f x y z :: a4 -> Type) = Eval (f (Eval x) (Eval y) (Eval z))

type Eval (Bicomap f g r x y :: a4 -> Type)

Defined in Fcf.Data.Function

type Eval (Bicomap f g r x y :: a4 -> Type) = Eval (r (Eval (f x)) (Eval (g y)))

type Eval (AsScalar xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (AsScalar xs :: [Nat] -> Type) = If (xs == '[1]) ('[] :: [Nat]) xs

type Eval (AsSingleton xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (AsSingleton xs :: [Nat] -> Type) = If (xs == ('[] :: [Nat])) '[1] xs

type Eval (DimsOf xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DimsOf xs :: [Nat] -> Type) = Eval (Range =<< Rank xs)

type Eval (MinDim s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (MinDim s :: [Nat] -> Type) = If (s == ('[] :: [Nat])) ('[] :: [Nat]) '[Eval (Minimum s)]

type Eval (PreDeletePositions xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (PreDeletePositions xs :: [Nat] -> Type)

type Eval (PreInsertPositions xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (PreInsertPositions xs :: [Nat] -> Type) = Eval ((Reverse :: [Nat] -> [Nat] -> Type) =<< (PreDeletePositions =<< Reverse xs))

type Eval (Range x :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (Range x :: [Nat] -> Type) = If (x == 0) ('[] :: [Nat]) (Eval (EnumFromTo 0 (Eval (x - 1))))

type Eval (Init ('[] :: [a]) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Init ('[] :: [a]) :: Maybe [a] -> Type) = 'Nothing :: Maybe [a]

type Eval (Tail (_a ': as) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Tail (_a ': as) :: Maybe [a] -> Type) = 'Just as

type Eval (Tail ('[] :: [a]) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Tail ('[] :: [a]) :: Maybe [a] -> Type) = 'Nothing :: Maybe [a]

type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type) = Eval ((Map (Cons a2) :: Maybe [a1] -> Maybe [a1] -> Type) =<< Init (b ': as))

type Eval (Init '[a2] :: Maybe [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Init '[a2] :: Maybe [a1] -> Type) = 'Just ('[] :: [a1])

type Eval (Head ('[] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Head ('[] :: [a]) :: Maybe a -> Type) = 'Nothing :: Maybe a

type Eval (Last ('[] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Last ('[] :: [a]) :: Maybe a -> Type) = 'Nothing :: Maybe a

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) = 'Just a2

type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type) = Eval (Last (b ': as))

type Eval (Last '[a2] :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Last '[a2] :: Maybe a1 -> Type) = 'Just a2

type Eval (DecAt d ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DecAt d ds :: [Nat] -> Type) = Eval (ModifyDim d (Flip (-) 1) ds)

type Eval (DeleteDim i ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DeleteDim i ds :: [Nat] -> Type) = Eval (LiftM2 ((++) :: [Nat] -> [Nat] -> [Nat] -> Type) (Take i ds) (Drop (i + 1) ds))

type Eval (DeleteDims xs ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DeleteDims xs ds :: [Nat] -> Type) = Eval ((Foldl' (Flip DeleteDim) ds :: [Nat] -> [Nat] -> Type) =<< PreDeletePositions xs)

type Eval (DimWindows ws s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DimWindows ws s :: [Nat] -> Type) = Eval (Eval (Range =<< Rank s) ++ Eval (EnumFromTo (Eval (2 * Eval (Rank s))) (Eval (Rank ws) - 1)))

type Eval (EndDimsOf xs s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (EndDimsOf xs s :: [Nat] -> Type) = Eval (LiftM2 (Take :: Nat -> [Nat] -> [Nat] -> Type) (Rank xs) ((Reverse :: [Nat] -> [Nat] -> Type) =<< DimsOf s))

type Eval (EnumFromTo a b :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (EnumFromTo a b :: [Nat] -> Type)

type Eval (ExceptDims ds s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (ExceptDims ds s :: [Nat] -> Type) = Eval (DeleteDims ds =<< EnumFromTo 0 (Eval (Eval (Rank s) - 1)))

type Eval (ExpandWindows ws ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (ExpandWindows ws ds :: [Nat] -> Type) = Eval (Eval (ZipWith (-) (Eval (Map ((+) 1) ds)) ws) ++ Eval (ws ++ Eval (Drop (Eval (Rank ws)) ds)))

type Eval (GetDims xs ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (GetDims xs ds :: [Nat] -> Type) = Eval (Map (Flip GetDim ds) xs)

type Eval (GetLastPositions ds s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (GetLastPositions ds s :: [Nat] -> Type) = Eval (Map (Flip (-) 1) (Eval (GetDims ds s)))

type Eval (IncAt d ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (IncAt d ds :: [Nat] -> Type) = Eval (ModifyDim d ((+) 1) (Eval (AsSingleton ds)))

type Eval (Reorder ds xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (Reorder ds xs :: [Nat] -> Type) = If (Eval (ReorderOk ds xs)) (Eval (Map (Flip GetDim ds) xs)) (TypeError ('Text "Reorder dimension indices out of bounds") :: [Nat])

type Eval (Rerank r xs :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (Rerank r xs :: [Nat] -> Type) = If (Eval (r > Eval (Rank xs))) (Eval (Eval (Replicate (Eval (r - Eval (Rank xs))) 1) ++ xs)) (Eval ('[Eval (Size (Eval (Take (Eval (Eval (Eval (Rank xs) - r) + 1)) xs)))] ++ Eval (Drop (Eval (Eval (Eval (Rank xs) - r) + 1)) xs)))

type Eval (Tails ('[] :: [a]) :: [[a]] -> Type)

Defined in Fcf.Data.List

type Eval (Tails ('[] :: [a]) :: [[a]] -> Type) = '[] :: [[a]]

type Eval (Tails (a2 ': as) :: [[a1]] -> Type)

Defined in Fcf.Data.List

type Eval (Tails (a2 ': as) :: [[a1]] -> Type) = (a2 ': as) ': Eval (Tails as)

type Eval (Reverse l :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Reverse l :: [a] -> Type) = Eval (Rev l ('[] :: [a]))

type Eval (Squeeze xs :: [a] -> Type)

Defined in Harpie.Shape

type Eval (Squeeze xs :: [a] -> Type) = Eval (Filter (Not <=< (TyEq 1 :: a -> Bool -> Type)) xs)

type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type) = 'Nothing :: Maybe Nat

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) = Eval (If (Eval (p a2)) (Pure ('Just 0)) ((Map ((+) 1) :: Maybe Nat -> Maybe Nat -> Type) =<< FindIndex p as))

type Eval (NumIter a s :: Maybe (k, Nat) -> Type)

Defined in Fcf.Data.List

type Eval (NumIter a s :: Maybe (k, Nat) -> Type) = If (Eval (s > 0)) ('Just '(a, s - 1)) ('Nothing :: Maybe (k, Natural))

type Eval (Find _p ('[] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Find _p ('[] :: [a]) :: Maybe a -> Type) = 'Nothing :: Maybe a

type Eval (Find p (a2 ': as) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) = Eval (If (Eval (p a2)) (Pure ('Just a2)) (Find p as))

type Eval (GetIndex d xs :: Maybe k -> Type)

Defined in Harpie.Shape

type Eval (GetIndex d xs :: Maybe k -> Type)

type Eval (ConcatDims ds n s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (ConcatDims ds n s :: [Nat] -> Type) = Eval (InsertDim n (Eval (Size (Eval (GetDims ds s)))) (Eval (DeleteDims ds s)))

type Eval (Concatenate i s0 s1 :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (Concatenate i s0 s1 :: [Nat] -> Type) = If (Eval (ConcatenateOk i s0 s1)) (Eval (Eval (Take i s0) ++ ((Eval (GetDim i s0) + Eval (GetDim i s1)) ': Eval (Drop (i + 1) s0)))) (TypeError ('Text "Concatenate Mis-matched shapes.") :: [Nat])

type Eval (DropDim d t s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DropDim d t s :: [Nat] -> Type) = Eval (ModifyDim d (Max 0 <=< Flip (-) t) s)

type Eval (DropDims ds xs s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (DropDims ds xs s :: [Nat] -> Type) = Eval (SetDims ds (Eval (ZipWith (-) (Eval (GetDims ds s)) xs)) s)

type Eval (InsertDim d i ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (InsertDim d i ds :: [Nat] -> Type) = Eval (LiftM2 ((++) :: [Nat] -> [Nat] -> [Nat] -> Type) (Take d ds) (Cons i =<< Drop d ds))

type Eval (InsertDims ds xs s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (InsertDims ds xs s :: [Nat] -> Type)

type Eval (ModifyDim d f s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (ModifyDim d f s :: [Nat] -> Type) = Eval (LiftM2 ((++) :: [Nat] -> [Nat] -> [Nat] -> Type) (Take d s) (LiftM2 (Cons :: Nat -> [Nat] -> [Nat] -> Type) (f =<< GetDim d s) (Drop (d + 1) s)))

type Eval (SetDim d x ds :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (SetDim d x ds :: [Nat] -> Type) = Eval (ModifyDim d (ConstFn x :: Nat -> Nat -> Type) ds)

type Eval (SetDims ds xs ns :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (SetDims ds xs ns :: [Nat] -> Type)

type Eval (TakeDim d t s :: [Nat] -> Type)

Defined in Harpie.Shape

type Eval (TakeDim d t s :: [Nat] -> Type) = Eval (ModifyDim d (Min t) s)

type Eval (xs ++ ys :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (xs ++ ys :: [a] -> Type) = xs <> ys

type Eval (Drop n as :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Drop n as :: [a] -> Type) = Drop_ n as

type Eval (DropWhile p (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (DropWhile p (x ': xs) :: [a] -> Type) = Eval (If (Eval (p x)) (DropWhile p xs) (Pure (x ': xs)))

type Eval (DropWhile p ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (DropWhile p ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

type Eval (Filter _p ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Filter _p ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

type Eval (Intercalate xs xss :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intercalate xs xss :: [a] -> Type) = Eval ((Concat :: [[a]] -> [a] -> Type) =<< Intersperse xs xss)

type Eval (Intersperse _1 ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intersperse _1 ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

type Eval (Intersperse sep (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intersperse sep (x ': xs) :: [a] -> Type) = x ': Eval (PrependToAll sep xs)

type Eval (PrependToAll _1 ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (PrependToAll _1 ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

type Eval (PrependToAll sep (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (PrependToAll sep (x ': xs) :: [a] -> Type) = sep ': (x ': Eval (PrependToAll sep xs))

type Eval (Rev (x ': xs) ys :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Rev (x ': xs) ys :: [a] -> Type) = Eval (Rev xs (x ': ys))

type Eval (Rev ('[] :: [a]) ys :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Rev ('[] :: [a]) ys :: [a] -> Type) = ys

type Eval (Take n as :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Take n as :: [a] -> Type) = Take_ n as

type Eval (TakeWhile p (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (TakeWhile p (x ': xs) :: [a] -> Type) = Eval (If (Eval (p x)) ('(:) x <$> TakeWhile p xs) (Pure ('[] :: [a])))

type Eval (TakeWhile p ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (TakeWhile p ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

type Eval (Cons a2 as :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Cons a2 as :: [a1] -> Type) = a2 ': as

type Eval (Filter p (a2 ': as) :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Filter p (a2 ': as) :: [a1] -> Type) = Eval (If (Eval (p a2)) ('(:) a2 <$> Filter p as) (Filter p as))

type Eval (Replicate n a2 :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Replicate n a2 :: [a1] -> Type) = Eval (Unfoldr (NumIter a2) n)

type Eval (Snoc lst a :: [k] -> Type)

Defined in Fcf.Data.List

type Eval (Snoc lst a :: [k] -> Type) = Eval (lst ++ '[a])

type Eval (Lookup a as :: Maybe b -> Type)

Defined in Fcf.Data.List

type Eval (Lookup a as :: Maybe b -> Type) = Eval (Map (Snd :: (k, b) -> b -> Type) (Eval (Find ((TyEq a :: k -> Bool -> Type) <=< (Fst :: (k, b) -> k -> Type)) as)))

type Eval (Zip as bs :: [(a, b)] -> Type)

Defined in Fcf.Data.List

type Eval (Zip as bs :: [(a, b)] -> Type) = Eval (ZipWith (Pure2 ('(,) :: a -> b -> (a, b))) as bs)

type Eval (Unfoldr f c :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Unfoldr f c :: [a] -> Type) = Eval (UnfoldrCase f (f @@ c))

type Eval (UnfoldrCase _1 ('Nothing :: Maybe (a, b)) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (UnfoldrCase _1 ('Nothing :: Maybe (a, b)) :: [a] -> Type) = '[] :: [a]

type Eval (UnfoldrCase f ('Just ab) :: [a2] -> Type)

Defined in Fcf.Data.List

type Eval (UnfoldrCase f ('Just ab) :: [a2] -> Type) = Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab)))

type Eval (SetIndex n a' as :: [k] -> Type)

Defined in Fcf.Data.List

type Eval (SetIndex n a' as :: [k] -> Type) = SetIndexImpl n a' as

type Eval (Map f ('Just a3) :: Maybe a2 -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f ('Just a3) :: Maybe a2 -> Type) = 'Just (Eval (f a3))

type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f ('Nothing :: Maybe a) :: Maybe b -> Type) = 'Nothing :: Maybe b

type Eval (ConcatMap f xs :: [b] -> Type)

Defined in Fcf.Class.Foldable

type Eval (ConcatMap f xs :: [b] -> Type) = Eval (FoldMap f xs)

type Eval (Map f ('[] :: [a]) :: [b] -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f ('[] :: [a]) :: [b] -> Type) = '[] :: [b]

type Eval (Map f (a2 ': as) :: [b] -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f (a2 ': as) :: [b] -> Type) = Eval (f a2) ': Eval (Map f as)

type Eval (ZipWith _f ('[] :: [a]) _bs :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith _f ('[] :: [a]) _bs :: [c] -> Type) = '[] :: [c]

type Eval (ZipWith _f _as ('[] :: [b]) :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith _f _as ('[] :: [b]) :: [c] -> Type) = '[] :: [c]

type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) = Eval (f a2 b2) ': Eval (ZipWith f as bs)

type Eval (Break p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Break p lst :: ([a], [a]) -> Type) = Eval (Span (Not <=< p) lst)

type Eval (Partition p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Partition p lst :: ([a], [a]) -> Type) = Eval (Foldr (PartHelp p) '('[] :: [a], '[] :: [a]) lst)

type Eval (Span p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Span p lst :: ([a], [a]) -> Type) = '(Eval (TakeWhile p lst), Eval (DropWhile p lst))

type Eval (Unzip as :: ([a], [b]) -> Type)

Defined in Fcf.Data.List

type Eval (Unzip as :: ([a], [b]) -> Type) = Eval (Foldr (Cons2 :: (a, b) -> ([a], [b]) -> ([a], [b]) -> Type) '('[] :: [a], '[] :: [b]) (Eval as))

type Eval (PartHelp p a2 '(xs, ys) :: ([a1], [a1]) -> Type)

Defined in Fcf.Data.List

type Eval (PartHelp p a2 '(xs, ys) :: ([a1], [a1]) -> Type) = If (Eval (p a2)) '(a2 ': xs, ys) '(xs, a2 ': ys)

type Eval (Cons2 '(a3, b) '(as, bs) :: ([a1], [a2]) -> Type)

Defined in Fcf.Data.List

type Eval (Cons2 '(a3, b) '(as, bs) :: ([a1], [a2]) -> Type) = '(a3 ': as, b ': bs)

type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f ('Left x :: Either a2 a1) :: Either a2 b -> Type) = 'Left x :: Either a2 b

type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f ('Right a3 :: Either a2 a1) :: Either a2 b -> Type) = 'Right (Eval (f a3)) :: Either a2 b

type Eval (Map f '(x, a2) :: (k2, k1) -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f '(x, a2) :: (k2, k1) -> Type) = '(x, Eval (f a2))

type Eval ((f *** f') '(b2, b'2) :: (k1, k2) -> Type)

Defined in Fcf.Data.Common

type Eval ((f *** f') '(b2, b'2) :: (k1, k2) -> Type) = '(Eval (f b2), Eval (f' b'2))

type Eval (Second g x :: f a' b' -> Type)

Defined in Fcf.Class.Bifunctor

type Eval (Second g x :: f a' b' -> Type) = Eval (Bimap (Pure :: a' -> a' -> Type) g x)

type Eval (First f2 x :: f1 a' b' -> Type)

Defined in Fcf.Class.Bifunctor

type Eval (First f2 x :: f1 a' b' -> Type) = Eval (Bimap f2 (Pure :: b' -> b' -> Type) x)

type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type)

Defined in Fcf.Class.Bifunctor

type Eval (Bimap f g ('Right y :: Either a b1) :: Either a' b2 -> Type) = 'Right (Eval (g y)) :: Either a' b2

type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type)

Defined in Fcf.Class.Bifunctor

type Eval (Bimap f g ('Left x :: Either a1 b) :: Either a2 b' -> Type) = 'Left (Eval (f x)) :: Either a2 b'

type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type)

Defined in Fcf.Class.Bifunctor

type Eval (Bimap f g '(x, y) :: (k1, k2) -> Type) = '(Eval (f x), Eval (g y))

type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f '(x, y, a2) :: (k2, k3, k1) -> Type) = '(x, y, Eval (f a2))

type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f '(x, y, z, a2) :: (k2, k3, k4, k1) -> Type) = '(x, y, z, Eval (f a2))

type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type)

Defined in Fcf.Class.Functor

type Eval (Map f '(x, y, z, w, a2) :: (k2, k3, k4, k5, k1) -> Type) = '(x, y, z, w, Eval (f a2))

data ((b :: [a]) ++ (c :: [a])) (d :: [a])

List catenation.

Example

>>> data Example where Ex :: a -> Example  -- Hide the type of examples to avoid brittleness in different GHC versions
>>> :kind! Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural])
Ex (Eval ([1, 2] ++ [3, 4]) :: [Natural]) :: Example
= Ex [1, 2, 3, 4]

Instances

type Eval (xs ++ ys :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (xs ++ ys :: [a] -> Type) = xs <> ys