| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
HordeAd.Core.TensorKind
Description
Two kinds of singletons for tensor kindss and constraints and lemmas associated with the singletons.
Synopsis
- data SingletonTK (y :: TK) where
- STKScalar :: forall r. GoodScalar r => SingletonTK ('TKScalar r)
- STKR :: forall (n :: Nat) (x :: TK). SNat n -> SingletonTK x -> SingletonTK ('TKR2 n x)
- STKS :: forall (sh :: [Nat]) (x :: TK). ShS sh -> SingletonTK x -> SingletonTK ('TKS2 sh x)
- STKX :: forall (sh :: [Maybe Nat]) (x :: TK). StaticShX sh -> SingletonTK x -> SingletonTK ('TKX2 sh x)
- STKProduct :: forall (y1 :: TK) (z :: TK). SingletonTK y1 -> SingletonTK z -> SingletonTK ('TKProduct y1 z)
- class KnownSTK (y :: TK) where
- knownSTK :: SingletonTK y
- data TKConversion (a :: TK) (b :: TK) where
- ConvId :: forall (a :: TK). TKConversion a a
- ConvCmp :: forall (b1 :: TK) (b :: TK) (a :: TK). TKConversion b1 b -> TKConversion a b1 -> TKConversion a b
- ConvRX :: forall (n :: Nat) (a1 :: TK). TKConversion ('TKR2 n a1) ('TKX2 (Replicate n ('Nothing :: Maybe Nat)) a1)
- ConvSX :: forall (sh :: [Nat]) (a1 :: TK). TKConversion ('TKS2 sh a1) ('TKX2 (MapJust sh) a1)
- ConvXR :: forall (a1 :: TK) (sh :: [Maybe Nat]). SingletonTK a1 -> TKConversion ('TKX2 sh a1) ('TKR2 (Rank sh) a1)
- ConvXS :: forall (sh :: [Nat]) (a1 :: TK). TKConversion ('TKX2 (MapJust sh) a1) ('TKS2 sh a1)
- ConvXS' :: forall (sh :: [Maybe Nat]) (sh' :: [Nat]) (a1 :: TK). Rank sh ~ Rank sh' => FullShapeTK ('TKS2 sh' a1) -> TKConversion ('TKX2 sh a1) ('TKS2 sh' a1)
- ConvXX' :: forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]) (a1 :: TK). Rank sh ~ Rank sh' => FullShapeTK ('TKX2 sh' a1) -> TKConversion ('TKX2 sh a1) ('TKX2 sh' a1)
- ConvRR :: forall (a1 :: TK) (b1 :: TK) (n :: Nat). TKConversion a1 b1 -> TKConversion ('TKR2 n a1) ('TKR2 n b1)
- ConvSS :: forall (a1 :: TK) (b1 :: TK) (sh :: [Nat]). TKConversion a1 b1 -> TKConversion ('TKS2 sh a1) ('TKS2 sh b1)
- ConvXX :: forall (a1 :: TK) (b1 :: TK) (sh :: [Maybe Nat]). TKConversion a1 b1 -> TKConversion ('TKX2 sh a1) ('TKX2 sh b1)
- ConvT2 :: forall (a1 :: TK) (a' :: TK) (b1 :: TK) (b' :: TK). TKConversion a1 a' -> TKConversion b1 b' -> TKConversion ('TKProduct a1 b1) ('TKProduct a' b')
- Conv0X :: forall (a :: TK). SingletonTK a -> TKConversion a ('TKX2 ('[] :: [Maybe Nat]) a)
- ConvX0 :: forall (b :: TK). TKConversion ('TKX2 ('[] :: [Maybe Nat]) b) b
- ConvNest :: forall (sh :: [Maybe Nat]) (a1 :: TK) (sh' :: [Maybe Nat]). SingletonTK ('TKX2 sh a1) -> TKConversion ('TKX2 (sh ++ sh') a1) ('TKX2 sh ('TKX2 sh' a1))
- ConvUnnest :: forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]) (a1 :: TK). TKConversion ('TKX2 sh ('TKX2 sh' a1)) ('TKX2 (sh ++ sh') a1)
- ConvZip :: forall (a1 :: TK) (b1 :: TK) (sh :: [Maybe Nat]). SingletonTK a1 -> SingletonTK b1 -> TKConversion ('TKProduct ('TKX2 sh a1) ('TKX2 sh b1)) ('TKX2 sh ('TKProduct a1 b1))
- ConvUnzip :: forall (a1 :: TK) (b1 :: TK) (sh :: [Maybe Nat]). SingletonTK a1 -> SingletonTK b1 -> TKConversion ('TKX2 sh ('TKProduct a1 b1)) ('TKProduct ('TKX2 sh a1) ('TKX2 sh b1))
- convertSTK :: forall (a :: TK) (b :: TK). TKConversion a b -> SingletonTK a -> SingletonTK b
- convertFTK :: forall (a :: TK) (b :: TK). TKConversion a b -> FullShapeTK a -> FullShapeTK b
- buildTKConversion :: forall (k :: Nat) (a :: TK) (b :: TK). SNat k -> FullShapeTK a -> TKConversion a b -> TKConversion (BuildTensorKind k a) (BuildTensorKind k b)
- withKnownSTK :: forall (y :: TK) r. SingletonTK y -> (KnownSTK y => r) -> r
- lemKnownSTK :: forall (y :: TK). SingletonTK y -> Dict KnownSTK y
- sameKnownSTK :: forall (y1 :: TK) (y2 :: TK). (KnownSTK y1, KnownSTK y2) => Maybe (y1 :~: y2)
- sameSTK :: forall (y1 :: TK) (y2 :: TK). SingletonTK y1 -> SingletonTK y2 -> Maybe (y1 :~: y2)
- stkUnit :: SingletonTK TKUnit
- buildSTK :: forall (k :: Nat) (y :: TK). SNat k -> SingletonTK y -> SingletonTK (BuildTensorKind k y)
- razeSTK :: forall (z :: TK). SingletonTK z -> SingletonTK (RazeTensorKind z)
- adSTK :: forall (y :: TK). SingletonTK y -> SingletonTK (ADTensorKind y)
- lemKnownSTKOfBuild :: forall (k :: Nat) (y :: TK). SNat k -> SingletonTK y -> Dict KnownSTK (BuildTensorKind k y)
- lemKnownSTKOfAD :: forall (y :: TK). SingletonTK y -> Dict KnownSTK (ADTensorKind y)
- lemBuildOfAD :: forall (k :: Nat) (y :: TK). SNat k -> SingletonTK y -> BuildTensorKind k (ADTensorKind y) :~: ADTensorKind (BuildTensorKind k y)
- lengthSTK :: forall (x :: TK). SingletonTK x -> Int
- widthSTK :: forall (y :: TK). SingletonTK y -> Int
- data FullShapeTK (y :: TK) where
- FTKScalar :: forall r. GoodScalar r => FullShapeTK ('TKScalar r)
- FTKR :: forall (n :: Nat) (x :: TK). IShR n -> FullShapeTK x -> FullShapeTK ('TKR2 n x)
- FTKS :: forall (sh :: [Nat]) (x :: TK). ShS sh -> FullShapeTK x -> FullShapeTK ('TKS2 sh x)
- FTKX :: forall (sh :: [Maybe Nat]) (x :: TK). IShX sh -> FullShapeTK x -> FullShapeTK ('TKX2 sh x)
- FTKProduct :: forall (y1 :: TK) (z :: TK). FullShapeTK y1 -> FullShapeTK z -> FullShapeTK ('TKProduct y1 z)
- matchingFTK :: forall (y1 :: TK) (y2 :: TK). FullShapeTK y1 -> FullShapeTK y2 -> Maybe (y1 :~: y2)
- ftkToSTK :: forall (y :: TK). FullShapeTK y -> SingletonTK y
- ftkUnit :: FullShapeTK TKUnit
- buildFTK :: forall (k :: Nat) (y :: TK). SNat k -> FullShapeTK y -> FullShapeTK (BuildTensorKind k y)
- razeFTK :: forall (y :: TK) (k :: Nat). SNat k -> SingletonTK y -> FullShapeTK (BuildTensorKind k y) -> FullShapeTK y
- adFTK :: forall (y :: TK). FullShapeTK y -> FullShapeTK (ADTensorKind y)
- differentiableFTK :: forall (y :: TK). FullShapeTK y -> Bool
- newtype DummyDualTarget (y :: TK) = DummyDualTarget (FullShapeTK y)
Tensor kind singletons
data SingletonTK (y :: TK) where Source #
Tensor kind singleton type.
Constructors
| STKScalar :: forall r. GoodScalar r => SingletonTK ('TKScalar r) | |
| STKR :: forall (n :: Nat) (x :: TK). SNat n -> SingletonTK x -> SingletonTK ('TKR2 n x) | |
| STKS :: forall (sh :: [Nat]) (x :: TK). ShS sh -> SingletonTK x -> SingletonTK ('TKS2 sh x) | |
| STKX :: forall (sh :: [Maybe Nat]) (x :: TK). StaticShX sh -> SingletonTK x -> SingletonTK ('TKX2 sh x) | |
| STKProduct :: forall (y1 :: TK) (z :: TK). SingletonTK y1 -> SingletonTK z -> SingletonTK ('TKProduct y1 z) |
Instances
| Show (SingletonTK y) Source # | |
Defined in HordeAd.Core.TensorKind Methods showsPrec :: Int -> SingletonTK y -> ShowS # show :: SingletonTK y -> String # showList :: [SingletonTK y] -> ShowS # | |
class KnownSTK (y :: TK) where Source #
The constraints corresponding to SingletonTK.
Methods
knownSTK :: SingletonTK y Source #
Instances
| GoodScalar r => KnownSTK ('TKScalar r) Source # | |
Defined in HordeAd.Core.TensorKind Methods knownSTK :: SingletonTK ('TKScalar r) Source # | |
| (KnownSTK y, KnownSTK z) => KnownSTK ('TKProduct y z) Source # | |
Defined in HordeAd.Core.TensorKind Methods knownSTK :: SingletonTK ('TKProduct y z) Source # | |
| (KnownSTK x, KnownNat n) => KnownSTK ('TKR2 n x) Source # | |
Defined in HordeAd.Core.TensorKind Methods knownSTK :: SingletonTK ('TKR2 n x) Source # | |
| (KnownSTK x, KnownShS sh) => KnownSTK ('TKS2 sh x) Source # | |
Defined in HordeAd.Core.TensorKind Methods knownSTK :: SingletonTK ('TKS2 sh x) Source # | |
| (KnownSTK x, KnownShX sh) => KnownSTK ('TKX2 sh x) Source # | |
Defined in HordeAd.Core.TensorKind Methods knownSTK :: SingletonTK ('TKX2 sh x) Source # | |
data TKConversion (a :: TK) (b :: TK) where Source #
This is copied, with modifications, from ox-arrays.
This is a recipe for converting arrays, not always followed, and a proof a conversion is possible, with some proof obligations delayed to runtime (in ConvXS' and ConvXX', where not only the ranks of the shapes need to agree, but also the dimensions of the input array and of the output shape, which is not all captured in the type). As in ox-arrays, conversions only change the meta-data, not the underlying vector representation of the array.
Constructors
| ConvId :: forall (a :: TK). TKConversion a a | |
| ConvCmp :: forall (b1 :: TK) (b :: TK) (a :: TK). TKConversion b1 b -> TKConversion a b1 -> TKConversion a b | |
| ConvRX :: forall (n :: Nat) (a1 :: TK). TKConversion ('TKR2 n a1) ('TKX2 (Replicate n ('Nothing :: Maybe Nat)) a1) | |
| ConvSX :: forall (sh :: [Nat]) (a1 :: TK). TKConversion ('TKS2 sh a1) ('TKX2 (MapJust sh) a1) | |
| ConvXR :: forall (a1 :: TK) (sh :: [Maybe Nat]). SingletonTK a1 -> TKConversion ('TKX2 sh a1) ('TKR2 (Rank sh) a1) | |
| ConvXS :: forall (sh :: [Nat]) (a1 :: TK). TKConversion ('TKX2 (MapJust sh) a1) ('TKS2 sh a1) | |
| ConvXS' :: forall (sh :: [Maybe Nat]) (sh' :: [Nat]) (a1 :: TK). Rank sh ~ Rank sh' => FullShapeTK ('TKS2 sh' a1) -> TKConversion ('TKX2 sh a1) ('TKS2 sh' a1) | |
| ConvXX' :: forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]) (a1 :: TK). Rank sh ~ Rank sh' => FullShapeTK ('TKX2 sh' a1) -> TKConversion ('TKX2 sh a1) ('TKX2 sh' a1) | |
| ConvRR :: forall (a1 :: TK) (b1 :: TK) (n :: Nat). TKConversion a1 b1 -> TKConversion ('TKR2 n a1) ('TKR2 n b1) | |
| ConvSS :: forall (a1 :: TK) (b1 :: TK) (sh :: [Nat]). TKConversion a1 b1 -> TKConversion ('TKS2 sh a1) ('TKS2 sh b1) | |
| ConvXX :: forall (a1 :: TK) (b1 :: TK) (sh :: [Maybe Nat]). TKConversion a1 b1 -> TKConversion ('TKX2 sh a1) ('TKX2 sh b1) | |
| ConvT2 :: forall (a1 :: TK) (a' :: TK) (b1 :: TK) (b' :: TK). TKConversion a1 a' -> TKConversion b1 b' -> TKConversion ('TKProduct a1 b1) ('TKProduct a' b') | |
| Conv0X :: forall (a :: TK). SingletonTK a -> TKConversion a ('TKX2 ('[] :: [Maybe Nat]) a) | |
| ConvX0 :: forall (b :: TK). TKConversion ('TKX2 ('[] :: [Maybe Nat]) b) b | |
| ConvNest :: forall (sh :: [Maybe Nat]) (a1 :: TK) (sh' :: [Maybe Nat]). SingletonTK ('TKX2 sh a1) -> TKConversion ('TKX2 (sh ++ sh') a1) ('TKX2 sh ('TKX2 sh' a1)) | |
| ConvUnnest :: forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]) (a1 :: TK). TKConversion ('TKX2 sh ('TKX2 sh' a1)) ('TKX2 (sh ++ sh') a1) | |
| ConvZip :: forall (a1 :: TK) (b1 :: TK) (sh :: [Maybe Nat]). SingletonTK a1 -> SingletonTK b1 -> TKConversion ('TKProduct ('TKX2 sh a1) ('TKX2 sh b1)) ('TKX2 sh ('TKProduct a1 b1)) | |
| ConvUnzip :: forall (a1 :: TK) (b1 :: TK) (sh :: [Maybe Nat]). SingletonTK a1 -> SingletonTK b1 -> TKConversion ('TKX2 sh ('TKProduct a1 b1)) ('TKProduct ('TKX2 sh a1) ('TKX2 sh b1)) |
Instances
| Category TKConversion Source # | |
Defined in HordeAd.Core.TensorKind Methods id :: forall (a :: TK). TKConversion a a # (.) :: forall (b :: TK) (c :: TK) (a :: TK). TKConversion b c -> TKConversion a b -> TKConversion a c # | |
| Show (TKConversion a b) Source # | |
Defined in HordeAd.Core.TensorKind Methods showsPrec :: Int -> TKConversion a b -> ShowS # show :: TKConversion a b -> String # showList :: [TKConversion a b] -> ShowS # | |
convertSTK :: forall (a :: TK) (b :: TK). TKConversion a b -> SingletonTK a -> SingletonTK b Source #
convertFTK :: forall (a :: TK) (b :: TK). TKConversion a b -> FullShapeTK a -> FullShapeTK b Source #
buildTKConversion :: forall (k :: Nat) (a :: TK) (b :: TK). SNat k -> FullShapeTK a -> TKConversion a b -> TKConversion (BuildTensorKind k a) (BuildTensorKind k b) Source #
withKnownSTK :: forall (y :: TK) r. SingletonTK y -> (KnownSTK y => r) -> r Source #
Turning a singleton into a constraint via a continuation.
lemKnownSTK :: forall (y :: TK). SingletonTK y -> Dict KnownSTK y Source #
Turning a singleton into a dictionary containing constraint.
sameKnownSTK :: forall (y1 :: TK) (y2 :: TK). (KnownSTK y1, KnownSTK y2) => Maybe (y1 :~: y2) Source #
sameSTK :: forall (y1 :: TK) (y2 :: TK). SingletonTK y1 -> SingletonTK y2 -> Maybe (y1 :~: y2) Source #
A plausible implementation of testEquality on SingletonTK.
buildSTK :: forall (k :: Nat) (y :: TK). SNat k -> SingletonTK y -> SingletonTK (BuildTensorKind k y) Source #
razeSTK :: forall (z :: TK). SingletonTK z -> SingletonTK (RazeTensorKind z) Source #
adSTK :: forall (y :: TK). SingletonTK y -> SingletonTK (ADTensorKind y) Source #
lemKnownSTKOfBuild :: forall (k :: Nat) (y :: TK). SNat k -> SingletonTK y -> Dict KnownSTK (BuildTensorKind k y) Source #
lemKnownSTKOfAD :: forall (y :: TK). SingletonTK y -> Dict KnownSTK (ADTensorKind y) Source #
lemBuildOfAD :: forall (k :: Nat) (y :: TK). SNat k -> SingletonTK y -> BuildTensorKind k (ADTensorKind y) :~: ADTensorKind (BuildTensorKind k y) Source #
Full shape tensor kind quasi-singletons
data FullShapeTK (y :: TK) where Source #
Full shape tensor kind singleton type.
Constructors
| FTKScalar :: forall r. GoodScalar r => FullShapeTK ('TKScalar r) | |
| FTKR :: forall (n :: Nat) (x :: TK). IShR n -> FullShapeTK x -> FullShapeTK ('TKR2 n x) | |
| FTKS :: forall (sh :: [Nat]) (x :: TK). ShS sh -> FullShapeTK x -> FullShapeTK ('TKS2 sh x) | |
| FTKX :: forall (sh :: [Maybe Nat]) (x :: TK). IShX sh -> FullShapeTK x -> FullShapeTK ('TKX2 sh x) | |
| FTKProduct :: forall (y1 :: TK) (z :: TK). FullShapeTK y1 -> FullShapeTK z -> FullShapeTK ('TKProduct y1 z) |
Instances
| Show (FullShapeTK y) Source # | |
Defined in HordeAd.Core.TensorKind Methods showsPrec :: Int -> FullShapeTK y -> ShowS # show :: FullShapeTK y -> String # showList :: [FullShapeTK y] -> ShowS # | |
| Eq (FullShapeTK y) Source # | |
Defined in HordeAd.Core.TensorKind Methods (==) :: FullShapeTK y -> FullShapeTK y -> Bool # (/=) :: FullShapeTK y -> FullShapeTK y -> Bool # | |
matchingFTK :: forall (y1 :: TK) (y2 :: TK). FullShapeTK y1 -> FullShapeTK y2 -> Maybe (y1 :~: y2) Source #
A plausible implementation of testEquality on FullShapeTK. It does not
take into account shape difference in ranked and mixed tensors
that FullShapeTK, but not SingletonTK, captures.
ftkToSTK :: forall (y :: TK). FullShapeTK y -> SingletonTK y Source #
A conversion that is fully determined by the property that it
commutes with the testEquality implementations.
buildFTK :: forall (k :: Nat) (y :: TK). SNat k -> FullShapeTK y -> FullShapeTK (BuildTensorKind k y) Source #
razeFTK :: forall (y :: TK) (k :: Nat). SNat k -> SingletonTK y -> FullShapeTK (BuildTensorKind k y) -> FullShapeTK y Source #
adFTK :: forall (y :: TK). FullShapeTK y -> FullShapeTK (ADTensorKind y) Source #
differentiableFTK :: forall (y :: TK). FullShapeTK y -> Bool Source #
newtype DummyDualTarget (y :: TK) Source #
Constructors
| DummyDualTarget (FullShapeTK y) |