TensorSafe.Shape

This module declares all Shape related functions and data structures, as well as all singleton -- instances for the Shape data type. This module was highly influenciated by Grenade, a Haskell -- library for deep learning with dependent types. See: https://github.com/HuwCampbell/grenade

Documentation

data Shape

The current shapes we accept. at the moment this is just one, two, and three dimensional Vectors/Matricies.

These are only used with DataKinds, as Kind Shape, with Types 'D1, 'D2, 'D3.

Constructors

D1 Nat

One dimensional vector

D2 Nat Nat

Two dimensional matrix. Row, Column.

D3 Nat Nat Nat

Three dimensional matrix. Row, Column, Channels.

Instances

KnownNat a => SingI (D1 a :: Shape)

Defined in TensorSafe.Shape

Methods

sing :: Sing (D1 a)

(KnownNat a, KnownNat b) => SingI (D2 a b :: Shape)

Defined in TensorSafe.Shape

Methods

sing :: Sing (D2 a b)

(KnownNat a, KnownNat b, KnownNat c) => SingI (D3 a b c :: Shape)

Defined in TensorSafe.Shape

Methods

sing :: Sing (D3 a b c)

SingI i => ValidNetwork ([] :: [Type]) (i ': ([] :: [Shape]))

Defined in TensorSafe.Network

Methods

mkINetwork :: INetwork [] (i ': [])

(Show x, Show (INetwork xs rs)) => Show (INetwork (x ': xs) (i ': rs))

Defined in TensorSafe.Network

Methods

showsPrec :: Int -> INetwork (x ': xs) (i ': rs) -> ShowS

show :: INetwork (x ': xs) (i ': rs) -> String

showList :: [INetwork (x ': xs) (i ': rs)] -> ShowS

Show (INetwork ([] :: [Type]) (i ': ([] :: [Shape])))

Defined in TensorSafe.Network

Methods

showsPrec :: Int -> INetwork [] (i ': []) -> ShowS

show :: INetwork [] (i ': []) -> String

showList :: [INetwork [] (i ': [])] -> ShowS

(SingI i, SingI o, Layer x, ValidNetwork xs (o ': rs), Out x i ~ o) => ValidNetwork (x ': xs) (i ': (o ': rs))

Defined in TensorSafe.Network

Methods

mkINetwork :: INetwork (x ': xs) (i ': (o ': rs))

data Sing (n :: Shape)

Defined in TensorSafe.Shape

data Sing (n :: Shape) where

• D1Sing :: forall (n :: Shape) (a :: Nat). KnownNat a => Sing a -> Sing (D1 a)
• D2Sing :: forall (n :: Shape) (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Sing a -> Sing b -> Sing (D2 a b)
• D3Sing :: forall (n :: Shape) (a :: Nat) (b :: Nat) (c :: Nat). (KnownNat a, KnownNat b, KnownNat c) => Sing a -> Sing b -> Sing c -> Sing (D3 a b c)

data S (n :: Shape) where

Concrete data structures for a Shape.

All shapes are held in contiguous memory. 3D is held in a matrix (usually row oriented) which has height depth * rows.

Constructors

S1D :: KnownNat len => R len -> S (D1 len)

S2D :: (KnownNat rows, KnownNat columns) => L rows columns -> S (D2 rows columns)

S3D :: (KnownNat rows, KnownNat columns, KnownNat depth, KnownNat (rows * depth)) => L (rows * depth) columns -> S (D3 rows columns depth)

Instances

Show (S n)

Defined in TensorSafe.Shape

Methods

showsPrec :: Int -> S n -> ShowS

show :: S n -> String

showList :: [S n] -> ShowS

type family ShapeEquals (sIn :: Shape) (sOut :: Shape) :: Bool where ...

Compares two Shapes at kinds level and returns a Bool kind

Equations

ShapeEquals s s = True

ShapeEquals _ _ = False

type family ShapeEquals' (sIn :: Shape) (sOut :: Shape) :: Bool where ...

Same as ShapeEquals, which compares two Shapes at kinds level, but raises a TypeError exception if the Shapes are not the equal.

Equations

ShapeEquals' s s = True

ShapeEquals' s1 s2 = TypeError (((Text "Couldn't match the Shape " :<>: ShowType s1) :<>: Text " with the Shape ") :<>: ShowType s2)