Copyright	(c) Grant Weyburne 2022
License	BSD-3
Safe Haskell	None
Language	Haskell2010

Cybus.NatHelper

Contents

peano
arithmetic
matrix dimension synonyms
matrix helpers
list and nonempty conversions

Description

Synopsis

type family NatToPeanoT n where ...
type family PeanoToNatT n where ...
data Peano
- = Z
- | S !Peano
type DiffT i j n = (j + 1) - i
type DiffTC i j n = (i <=! j, j <=! n)
type family FacT x where ...
type (<=!) i n = (FailUnless (i <=? n) (((('Text "i>n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n), PosC i)
type (<!) i n = (FailUnless ((i + 1) <=? n) (((('Text "i>=n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n), KnownNat i)
type LTEQT msg i n = (FailUnless (i <=? n) ((((('Text "i>n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n) :<>: msg), PosC i)
type D1 a = '[a]
type D2 a b = '[a, b]
type D3 a b c = '[a, b, c]
type D4 a b c d = '[a, b, c, d]
type D5 a b c d e = '[a, b, c, d, e]
type D6 a b c d e f = '[a, b, c, d, e, f]
type D7 a b c d e f g = '[a, b, c, d, e, f, g]
type D8 a b c d e f g h = '[a, b, c, d, e, f, g, h]
type D9 a b c d e f g h i = '[a, b, c, d, e, f, g, h, i]
type D10 a b c d e f g h i j = '[a, b, c, d, e, f, g, h, i, j]
type family ProductT ns where ...
type NN n = NN' '[] n
type family NN' ns n where ...
type family ReverseT ns where ...
type family ListTupleT n a = result | result -> n a where ...
class ValidateNestedListC x y where
- validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
class ValidateNestedNonEmptyC x y where
- validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos)
validateNestedList :: forall x. ValidateNestedListC x (ValidateNestedListT x) => x -> Either String (NonEmpty Pos)
validateNestedNonEmpty :: forall x. ValidateNestedNonEmptyC x (ValidateNestedNonEmptyT x) => x -> Either String (NonEmpty Pos)
type family ValidateNestedListT x where ...
type family ValidateNestedNonEmptyT x where ...
nestedNonEmptyToList :: forall ns a. NestedListC ns => NonEmptyNST ns a -> Either String (ListNST ns a)
nestedListToNonEmpty :: forall ns a. NestedListC ns => ListNST ns a -> Either String (NonEmptyNST ns a)
class NestedListC ns where
- nestedListToNonEmptyC :: proxy a -> ListNST ns a -> Either String (NonEmptyNST ns a)
- nestedNonEmptyToListC :: proxy a -> NonEmptyNST ns a -> Either String (ListNST ns a)
- flattenNestedListC :: proxy a -> ListNST ns a -> Either String [a]
type family NonEmptyNST ns a where ...
type family ListNST ns a where ...

peano

type family NatToPeanoT n where ... Source #

convert Nat to Peano

Equations

NatToPeanoT 0 = 'Z
NatToPeanoT n = 'S (NatToPeanoT (n - 1))

type family PeanoToNatT n where ... Source #

convert Peano to Nat

Equations

PeanoToNatT 'Z = 0
PeanoToNatT ('S n) = 1 + PeanoToNatT n

data Peano Source #

peano numbers for converting between Nat and peano

Constructors

Z
S !Peano

Instances

Instances details

Eq Peano Source #
Instance details Defined in Cybus.NatHelper Methods (==) :: Peano -> Peano -> Bool # (/=) :: Peano -> Peano -> Bool #
Ord Peano Source #
Instance details Defined in Cybus.NatHelper Methods compare :: Peano -> Peano -> Ordering # (<) :: Peano -> Peano -> Bool # (<=) :: Peano -> Peano -> Bool # (>) :: Peano -> Peano -> Bool # (>=) :: Peano -> Peano -> Bool # max :: Peano -> Peano -> Peano # min :: Peano -> Peano -> Peano #
Show Peano Source #
Instance details Defined in Cybus.NatHelper Methods showsPrec :: Int -> Peano -> ShowS # show :: Peano -> String # showList :: [Peano] -> ShowS #

arithmetic

type DiffT i j n = (j + 1) - i Source #

find the number of N between "i" and "j" while ensuring i<=j and j<=n

type DiffTC i j n = (i <=! j, j <=! n) Source #

constraint for DiffC with better error messages

type family FacT x where ... Source #

get the factorial of a Nat

Equations

FacT 0 = 1
FacT 1 = 1
FacT n = n * FacT (n - 1)

type (<=!) i n = (FailUnless (i <=? n) (((('Text "i>n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n), PosC i) Source #

constraint for ensuring that "i" <= "n"

type (<!) i n = (FailUnless ((i + 1) <=? n) (((('Text "i>=n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n), KnownNat i) Source #

constraint for ensuring that "i" <= "n"

type LTEQT msg i n = (FailUnless (i <=? n) ((((('Text "i>n" :<>: 'Text ": i=") :<>: 'ShowType i) :<>: 'Text " n=") :<>: 'ShowType n) :<>: msg), PosC i) Source #

constraint for ensuring that "i" <= "n" with a custom error message

matrix dimension synonyms

type D1 a = '[a] Source #

matrix dimension of degree 1

type D2 a b = '[a, b] Source #

matrix dimension of degree 2

type D3 a b c = '[a, b, c] Source #

matrix dimension of degree 3

type D4 a b c d = '[a, b, c, d] Source #

matrix dimension of degree 4

type D5 a b c d e = '[a, b, c, d, e] Source #

matrix dimension of degree 5

type D6 a b c d e f = '[a, b, c, d, e, f] Source #

matrix dimension of degree 6

type D7 a b c d e f g = '[a, b, c, d, e, f, g] Source #

matrix dimension of degree 7

type D8 a b c d e f g h = '[a, b, c, d, e, f, g, h] Source #

matrix dimension of degree 8

type D9 a b c d e f g h i = '[a, b, c, d, e, f, g, h, i] Source #

matrix dimension of degree 9

type D10 a b c d e f g h i j = '[a, b, c, d, e, f, g, h, i, j] Source #

matrix dimension of degree 10

matrix helpers

type family ProductT ns where ... Source #

product of a type level list as a Nat

Equations

ProductT '[] = TypeError ('Text "ProductT: empty indices")
ProductT '[n] = n
ProductT (n ': (n1 ': ns)) = n * ProductT (n1 ': ns)

type NN n = NN' '[] n Source #

generates a list of indices using each digit of the given Nat

type family NN' ns n where ... Source #

generates a list of indices using the individual digits of the given Nat

Equations

NN' ns 0 = ns
NN' ns n = NN' (Mod n 10 ': ns) (Div n 10)

type family ReverseT ns where ... Source #

reverse a type level list

Equations

ReverseT (n ': ns) = ReverseT' (n ': ns) '[]

type family ListTupleT n a = result | result -> n a where ... Source #

translates a type of size "n" to a tuple of size "n"

Equations

ListTupleT 1 a = One a
ListTupleT 2 a = (a, a)
ListTupleT 3 a = (a, a, a)
ListTupleT 4 a = (a, a, a, a)
ListTupleT 5 a = (a, a, a, a, a)
ListTupleT 6 a = (a, a, a, a, a, a)
ListTupleT 7 a = (a, a, a, a, a, a, a)
ListTupleT 8 a = (a, a, a, a, a, a, a, a)
ListTupleT 9 a = (a, a, a, a, a, a, a, a, a)
ListTupleT 10 a = (a, a, a, a, a, a, a, a, a, a)
ListTupleT 11 a = (a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 12 a = (a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 13 a = (a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 14 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 15 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 16 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 17 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 18 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 19 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)
ListTupleT 20 a = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a)

list and nonempty conversions

class ValidateNestedListC x y where Source #

extracts the dimensions of a nested list: doesnt allow empty dimensions

Methods

validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos) Source #

Instances

Instances details

(TypeError ('Text "ValidateNestedListC: not defined at 0") :: Constraint) => ValidateNestedListC x 'Z Source #
Instance details Defined in Cybus.NatHelper Methods validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos) Source #
ValidateNestedListC x ('S 'Z) Source #
Instance details Defined in Cybus.NatHelper Methods validateNestedListC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos) Source #
ValidateNestedListC x ('S n) => ValidateNestedListC [x] ('S ('S n)) Source #
Instance details Defined in Cybus.NatHelper Methods validateNestedListC :: [Pos] -> [x] -> [[x]] -> Either String (NonEmpty Pos) Source #

class ValidateNestedNonEmptyC x y where Source #

extracts the dimensions of a nested nonempty list: doesnt allow empty dimensions

Methods

validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos) Source #

Instances

Instances details

(TypeError ('Text "ValidateNestedNonEmptyC: not defined at 'Z") :: Constraint) => ValidateNestedNonEmptyC x 'Z Source #
Instance details Defined in Cybus.NatHelper Methods validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos) Source #
ValidateNestedNonEmptyC x ('S 'Z) Source #
Instance details Defined in Cybus.NatHelper Methods validateNestedNonEmptyC :: [Pos] -> x -> [x] -> Either String (NonEmpty Pos) Source #
ValidateNestedNonEmptyC x ('S zs) => ValidateNestedNonEmptyC (NonEmpty x) ('S ('S zs)) Source #
Instance details Defined in Cybus.NatHelper Methods validateNestedNonEmptyC :: [Pos] -> NonEmpty x -> [NonEmpty x] -> Either String (NonEmpty Pos) Source #

validateNestedList :: forall x. ValidateNestedListC x (ValidateNestedListT x) => x -> Either String (NonEmpty Pos) Source #

validate that the nested list is consistent in size along all dimensions

validateNestedNonEmpty :: forall x. ValidateNestedNonEmptyC x (ValidateNestedNonEmptyT x) => x -> Either String (NonEmpty Pos) Source #

validate that the nested nonempty list is consistent in size along all dimensions

type family ValidateNestedListT x where ... Source #

extracts the dimensions of a nested list

Equations

ValidateNestedListT [x] = 'S (ValidateNestedListT x)
ValidateNestedListT _ = 'S 'Z

type family ValidateNestedNonEmptyT x where ... Source #

extracts the dimensions of a nested nonempty list

Equations

ValidateNestedNonEmptyT (NonEmpty x) = 'S (ValidateNestedNonEmptyT x)
ValidateNestedNonEmptyT _ = 'S 'Z

nestedNonEmptyToList :: forall ns a. NestedListC ns => NonEmptyNST ns a -> Either String (ListNST ns a) Source #

convert a nested nonempty list into a nested list

nestedListToNonEmpty :: forall ns a. NestedListC ns => ListNST ns a -> Either String (NonEmptyNST ns a) Source #

convert a nested list into a nested nonempty list

class NestedListC ns where Source #

methods for working with nested lists

Methods

nestedListToNonEmptyC :: proxy a -> ListNST ns a -> Either String (NonEmptyNST ns a) Source #

convert a nested list to a nested nonempty list

nestedNonEmptyToListC :: proxy a -> NonEmptyNST ns a -> Either String (ListNST ns a) Source #

convert a nested nonempty list to a nested list

flattenNestedListC :: proxy a -> ListNST ns a -> Either String [a] Source #

Instances

Instances details

(TypeError ('Text "NestedListC '[]: empty indices") :: Constraint) => NestedListC ('[] :: [Nat]) Source #
Instance details Defined in Cybus.NatHelper Methods nestedListToNonEmptyC :: proxy a -> ListNST '[] a -> Either String (NonEmptyNST '[] a) Source # nestedNonEmptyToListC :: proxy a -> NonEmptyNST '[] a -> Either String (ListNST '[] a) Source # flattenNestedListC :: proxy a -> ListNST '[] a -> Either String [a] Source #
(PosC n, NestedListC (n1 ': ns)) => NestedListC (n ': (n1 ': ns)) Source #
Instance details Defined in Cybus.NatHelper Methods nestedListToNonEmptyC :: proxy a -> ListNST (n ': (n1 ': ns)) a -> Either String (NonEmptyNST (n ': (n1 ': ns)) a) Source # nestedNonEmptyToListC :: proxy a -> NonEmptyNST (n ': (n1 ': ns)) a -> Either String (ListNST (n ': (n1 ': ns)) a) Source # flattenNestedListC :: proxy a -> ListNST (n ': (n1 ': ns)) a -> Either String [a] Source #
PosC n => NestedListC '[n] Source #
Instance details Defined in Cybus.NatHelper Methods nestedListToNonEmptyC :: proxy a -> ListNST '[n] a -> Either String (NonEmptyNST '[n] a) Source # nestedNonEmptyToListC :: proxy a -> NonEmptyNST '[n] a -> Either String (ListNST '[n] a) Source # flattenNestedListC :: proxy a -> ListNST '[n] a -> Either String [a] Source #

type family NonEmptyNST ns a where ... Source #

convert a matrix index into nested lists

Equations

NonEmptyNST '[] _ = TypeError ('Text "NonEmptyNST: empty indices")
NonEmptyNST '[_] a = NonEmpty a
NonEmptyNST (_ ': (n1 ': ns)) a = NonEmpty (NonEmptyNST (n1 ': ns) a)

type family ListNST ns a where ... Source #

convert a matrix index into nested lists

Equations

ListNST '[] _ = TypeError ('Text "ListNST: empty indices")
ListNST '[_] a = [a]
ListNST (_ ': (n1 ': ns)) a = [ListNST (n1 ': ns) a]