Torch.Typed.Auxiliary

Documentation

natValI :: forall (n :: Nat). KnownNat n => Int

natValInt16 :: forall (n :: Nat). KnownNat n => Int16

type family Fst (t :: (a, b)) :: a where ...

Equations

Fst ('(x, _1) :: (a, b)) = x

type family Snd (t :: (a, b)) :: b where ...

Equations

Snd ('(_1, x) :: (a, b)) = x

type family Fst3 (t :: (a, b, c)) :: a where ...

Equations

Fst3 ('(x, _1, _2) :: (a, b, c)) = x

type family Snd3 (t :: (a, b, c)) :: b where ...

Equations

Snd3 ('(_1, x, _2) :: (a, b, c)) = x

type family Trd3 (t :: (a, b, c)) :: c where ...

Equations

Trd3 ('(_1, _2, x) :: (a, b, c)) = x

type family DimOutOfBoundCheckImpl (shape :: [a]) (dim :: Nat) (xs :: [a]) (n :: Nat) where ...

Equations

DimOutOfBoundCheckImpl (shape :: [a]) dim ('[] :: [a]) _1 = DimOutOfBound shape dim :: Constraint

DimOutOfBoundCheckImpl (_1 :: [a]) _2 (_3 :: [a]) 0 = ()

DimOutOfBoundCheckImpl (shape :: [a]) dim (_1 ': xs :: [a]) n = DimOutOfBoundCheckImpl shape dim xs (n - 1)

type DimOutOfBoundCheck (shape :: [a]) (dim :: Nat) = DimOutOfBoundCheckImpl shape dim shape dim

type family DimOutOfBound (shape :: [a]) (dim :: Nat) :: k where ...

Equations

DimOutOfBound (shape :: [k1]) dim = TypeError (((('Text "Out of bound dimension: " ':<>: 'ShowType dim) ':<>: 'Text " (the tensor is only ") ':<>: 'ShowType (ListLength shape)) ':<>: 'Text "D)") :: k2

type family IndexOutOfBound (shape :: [a]) (dim :: Nat) (idx :: Nat) :: k where ...

Equations

IndexOutOfBound (shape :: [a]) dim idx = TypeError (((((('Text "Out of bound index " ':<>: 'ShowType idx) ':<>: 'Text " for dimension ") ':<>: 'ShowType dim) ':<>: 'Text " (the tensor shape is ") ':<>: 'ShowType shape) ':<>: 'Text ")") :: k

type family AppendToMaybe (h :: a) (mt :: Maybe [a]) :: Maybe [a] where ...

Equations

AppendToMaybe (h :: a) ('Nothing :: Maybe [a]) = 'Nothing :: Maybe [a]

AppendToMaybe (h :: a) ('Just t :: Maybe [a]) = 'Just (h ': t)

type family AppendToMaybe' (h :: Maybe a) (mt :: Maybe [a]) :: Maybe [a] where ...

Equations

AppendToMaybe' ('Nothing :: Maybe a) (_1 :: Maybe [a]) = 'Nothing :: Maybe [a]

AppendToMaybe' (_1 :: Maybe a) ('Nothing :: Maybe [a]) = 'Nothing :: Maybe [a]

AppendToMaybe' ('Just h :: Maybe a) ('Just t :: Maybe [a]) = 'Just (h ': t)

type family MaybePrepend (mh :: Maybe a) (t :: [a]) :: [a] where ...

Equations

MaybePrepend ('Nothing :: Maybe a) (t :: [a]) = t

MaybePrepend ('Just h :: Maybe a) (t :: [a]) = h ': t

type family LastDim (l :: [a]) :: Nat where ...

Equations

LastDim ('[_1] :: [a]) = 0

LastDim (_1 ': t :: [a]) = 1 + LastDim t

type family Product (xs :: [Nat]) :: Nat where ...

Equations

Product ('[] :: [Nat]) = 1

Product (x ': xs) = x * Product xs

type family BackwardsImpl (last :: Nat) (n :: Nat) :: Nat where ...

Equations

BackwardsImpl last n = last - n

type Backwards (l :: [a]) (n :: Nat) = BackwardsImpl (LastDim l) n

type IsSuffixOf (xs :: [b]) (ys :: [b]) = CheckIsSuffixOf xs ys (IsSuffixOfImpl xs ys (DropLengthMaybe xs ys))

Evaluate a type-level constraint for whether or not the former shape is a suffix of the latter shape

>>> :kind! IsSuffixOf '[1] '[1]
IsSuffixOf '[1] '[1] :: Constraint
= () :: Constraint
>>> :kind! IsSuffixOf '[1] '[2, 1]
IsSuffixOf '[1] '[2, 1] :: Constraint
= () :: Constraint
>>> :kind! IsSuffixOf '[2] '[2, 1]
IsSuffixOf '[2] '[2, 1] :: Constraint
= (TypeError ...)
>>> :kind! IsSuffixOf '[1, 1] '[2, 1]
IsSuffixOf '[1, 1] '[2, 1] :: Constraint
= (TypeError ...)
>>> :kind! IsSuffixOf '[2, 1] '[2, 1]
IsSuffixOf '[2, 1] '[2, 1] :: Constraint
= () :: Constraint

type family CheckIsSuffixOf (xs :: [a]) (ys :: [a]) (result :: Bool) where ...

Equations

CheckIsSuffixOf (_1 :: [a]) (_2 :: [a]) 'True = ()

CheckIsSuffixOf (xs :: [a]) (ys :: [a]) 'False = TypeError (('ShowType xs ':<>: 'Text " is not a suffix of ") ':<>: 'ShowType ys) :: Constraint

type family IsSuffixOfImpl (xs :: [a]) (ys :: [a]) (mDelta :: Maybe [b]) :: Bool where ...

Equations

IsSuffixOfImpl (xs :: [b]) (ys :: [b]) ('Just delta :: Maybe [a]) = xs == DropLength delta ys

IsSuffixOfImpl (_1 :: [a]) (_2 :: [a]) ('Nothing :: Maybe [b]) = 'False

type family DropLengthMaybe (xs :: [a]) (ys :: [b]) :: Maybe [b] where ...

Equations

DropLengthMaybe ('[] :: [a]) (ys :: [b]) = 'Just ys

DropLengthMaybe (_1 :: [a]) ('[] :: [b]) = 'Nothing :: Maybe [b]

DropLengthMaybe (_1 ': xs :: [a]) (_2 ': ys :: [b]) = DropLengthMaybe xs ys

type family DropLength (xs :: [a]) (ys :: [b]) :: [b] where ...

Equations

DropLength ('[] :: [a]) (ys :: [b]) = ys

DropLength (_1 :: [a]) ('[] :: [b]) = '[] :: [b]

DropLength (_1 ': xs :: [a]) (_2 ': ys :: [b]) = DropLength xs ys

type family Init (xs :: [a]) :: [a] where ...

Equations

Init ('[] :: [a]) = TypeError ('Text "Init of empty list.") :: [a]

Init ('[x] :: [a]) = '[] :: [a]

Init (x ': xs :: [a]) = x ': Init xs

type family Last (xs :: [a]) :: a where ...

Equations

Last ('[] :: [a]) = TypeError ('Text "Last of empty list.") :: a

Last ('[x] :: [a]) = x

Last (x ': xs :: [a]) = Last xs

type family InsertImpl (n :: Nat) (x :: a) (l :: [a]) :: Maybe [a] where ...

Equations

InsertImpl 0 (x :: a) (l :: [a]) = 'Just (x ': l)

InsertImpl n (x :: a) ('[] :: [a]) = 'Nothing :: Maybe [a]

InsertImpl n (x :: a) (h ': t :: [a]) = AppendToMaybe h (InsertImpl (n - 1) x t)

type family CheckInsert (n :: Nat) (x :: a) (l :: [a]) (result :: Maybe [a]) :: [a] where ...

Equations

CheckInsert _1 (_2 :: a) (_3 :: [a]) ('Just xs :: Maybe [a]) = xs

CheckInsert n (x :: a) (l :: [a]) ('Nothing :: Maybe [a]) = DimOutOfBound l n :: [a]

type family Insert (n :: Nat) (x :: a) (l :: [a]) :: [a] where ...

Equations

Insert n (x :: a) (l :: [a]) = CheckInsert n x l (InsertImpl n x l)

type family RemoveImpl (l :: [a]) (n :: Nat) :: Maybe [a] where ...

Equations

RemoveImpl (h ': t :: [a]) 0 = 'Just t

RemoveImpl (h ': t :: [a]) n = AppendToMaybe h (RemoveImpl t (n - 1))

RemoveImpl (_1 :: [a]) _2 = 'Nothing :: Maybe [a]

type family CheckRemove (l :: [a]) (n :: Nat) (result :: Maybe [a]) :: [a] where ...

Equations

CheckRemove (l :: [a]) n ('Nothing :: Maybe [a]) = DimOutOfBound l n :: [a]

CheckRemove (_1 :: [a]) _2 ('Just result :: Maybe [a]) = result

type Remove (l :: [a]) (n :: Nat) = CheckRemove l n (RemoveImpl l n)

type family IndexImpl (l :: [a]) (n :: Nat) :: Maybe a where ...

Equations

IndexImpl (h ': t :: [a]) 0 = 'Just h

IndexImpl (h ': t :: [a]) n = IndexImpl t (n - 1)

IndexImpl (_1 :: [a]) _2 = 'Nothing :: Maybe a

type family CheckIndex (l :: [a]) (n :: Nat) (result :: Maybe a) :: a where ...

Equations

CheckIndex (l :: [a]) n ('Nothing :: Maybe a) = DimOutOfBound l n :: a

CheckIndex (_1 :: [a]) _2 ('Just result :: Maybe a) = result

type Index (l :: [k]) (n :: Nat) = CheckIndex l n (IndexImpl l n)

type family InRangeCheck (shape :: [Nat]) (dim :: Nat) (idx :: Nat) (ok :: Ordering) where ...

Equations

InRangeCheck _1 _2 _3 'LT = ()

InRangeCheck shape dim idx _1 = IndexOutOfBound shape dim idx :: Constraint

type InRange (shape :: [Nat]) (dim :: Nat) (idx :: Nat) = InRangeCheck shape dim idx (CmpNat idx (Index shape dim))

type family ReverseImpl (l :: [a]) (acc :: [a]) :: [a] where ...

Equations

ReverseImpl ('[] :: [a]) (acc :: [a]) = acc

ReverseImpl (h ': t :: [a]) (acc :: [a]) = ReverseImpl t (h ': acc)

type Reverse (l :: [a]) = ReverseImpl l ('[] :: [a])

type family ExtractDim (dim :: Nat) (shape :: [Nat]) :: Maybe Nat where ...

Equations

ExtractDim 0 (h ': _1) = 'Just h

ExtractDim dim (_1 ': t) = ExtractDim (dim - 1) t

ExtractDim _1 _2 = 'Nothing :: Maybe Nat

type family ReplaceDim (dim :: Nat) (shape :: [Nat]) (n :: Nat) :: Maybe [Nat] where ...

Equations

ReplaceDim 0 (_1 ': t) n = 'Just (n ': t)

ReplaceDim dim (h ': t) n = AppendToMaybe h (ReplaceDim (dim - 1) t n)

ReplaceDim _1 _2 _3 = 'Nothing :: Maybe [Nat]

type family If (c :: Bool) (t :: k) (e :: k) :: k where ...

Equations

If 'True (t :: k) (e :: k) = t

If 'False (t :: k) (e :: k) = e

type family AllDimsPositive (shape :: [Nat]) where ...

Equations

AllDimsPositive ('[] :: [Nat]) = ()

AllDimsPositive (x ': xs) = If (1 <=? x) (AllDimsPositive xs) (TypeError (('Text "Expected positive dimension but got " ':<>: 'ShowType x) ':<>: 'Text "!") :: Constraint)

type family IsAtLeast (n :: Nat) (m :: Nat) (cmp :: Ordering) where ...

Equations

IsAtLeast n m 'LT = TypeError (((('Text "Expected a dimension of size at least " ':<>: 'ShowType n) ':<>: 'Text " but got ") ':<>: 'ShowType m) ':<>: 'Text "!") :: Constraint

IsAtLeast _1 _2 _3 = ()

type (>=) (n :: Nat) (m :: Nat) = (IsAtLeast n m (CmpNat n m), KnownNat (n - m))

type family CmpDType (dtype :: DType) (dtype' :: DType) :: Ordering where ...

Equations

CmpDType dtype dtype = 'EQ

CmpDType 'Bool 'UInt8 = 'LT

CmpDType 'Bool 'Int8 = 'LT

CmpDType 'Bool 'Int16 = 'LT

CmpDType 'Bool 'Int32 = 'LT

CmpDType 'Bool 'Int64 = 'LT

CmpDType 'Bool 'Half = 'LT

CmpDType 'Bool 'Float = 'LT

CmpDType 'Bool 'Double = 'LT

CmpDType 'UInt8 'Int8 = 'LT

CmpDType 'UInt8 'Int16 = 'LT

CmpDType 'UInt8 'Int32 = 'LT

CmpDType 'UInt8 'Int64 = 'LT

CmpDType 'UInt8 'Half = 'LT

CmpDType 'UInt8 'Float = 'LT

CmpDType 'UInt8 'Double = 'LT

CmpDType 'Int8 'Int16 = 'LT

CmpDType 'Int8 'Int32 = 'LT

CmpDType 'Int8 'Int64 = 'LT

CmpDType 'Int8 'Half = 'LT

CmpDType 'Int8 'Float = 'LT

CmpDType 'Int8 'Double = 'LT

CmpDType 'Int16 'Int32 = 'LT

CmpDType 'Int16 'Int64 = 'LT

CmpDType 'Int16 'Half = 'LT

CmpDType 'Int16 'Float = 'LT

CmpDType 'Int16 'Double = 'LT

CmpDType 'Int32 'Int64 = 'LT

CmpDType 'Int32 'Half = 'LT

CmpDType 'Int32 'Float = 'LT

CmpDType 'Int32 'Double = 'LT

CmpDType 'Int64 'Half = 'LT

CmpDType 'Int64 'Float = 'LT

CmpDType 'Int64 'Double = 'LT

CmpDType 'Half 'Float = 'LT

CmpDType 'Half 'Double = 'LT

CmpDType 'Float 'Double = 'LT

CmpDType _1 _2 = 'GT

type family DTypePromotionImpl (dtype :: DType) (dtype' :: DType) (ord :: Ordering) :: DType where ...

Equations

DTypePromotionImpl 'UInt8 'Int8 _1 = 'Int16

DTypePromotionImpl 'Int8 'UInt8 _1 = 'Int16

DTypePromotionImpl dtype _1 'EQ = dtype

DTypePromotionImpl _1 dtype 'LT = dtype

DTypePromotionImpl dtype _1 'GT = dtype

type DTypePromotion (dtype :: DType) (dtype' :: DType) = DTypePromotionImpl dtype dtype' (CmpDType dtype dtype')

type family DTypeIsFloatingPoint (device :: (DeviceType, Nat)) (dtype :: DType) where ...

Equations

DTypeIsFloatingPoint _1 'Half = ()

DTypeIsFloatingPoint _1 'Float = ()

DTypeIsFloatingPoint _1 'Double = ()

DTypeIsFloatingPoint '(deviceType, _1) dtype = UnsupportedDTypeForDevice deviceType dtype

type family DTypeIsIntegral (device :: (DeviceType, Nat)) (dtype :: DType) where ...

Equations

DTypeIsIntegral _1 'Bool = ()

DTypeIsIntegral _1 'UInt8 = ()

DTypeIsIntegral _1 'Int8 = ()

DTypeIsIntegral _1 'Int16 = ()

DTypeIsIntegral _1 'Int32 = ()

DTypeIsIntegral _1 'Int64 = ()

DTypeIsIntegral '(deviceType, _1) dtype = UnsupportedDTypeForDevice deviceType dtype

type family DTypeIsNotHalf (device :: (DeviceType, Nat)) (dtype :: DType) where ...

Equations

DTypeIsNotHalf '(deviceType, _1) 'Half = UnsupportedDTypeForDevice deviceType 'Half

DTypeIsNotHalf _1 _2 = ()

type family DTypeIsNotBool (device :: (DeviceType, Nat)) (dtype :: DType) where ...

Equations

DTypeIsNotBool '(deviceType, _1) 'Bool = UnsupportedDTypeForDevice deviceType 'Bool

DTypeIsNotBool _1 _2 = ()

type family UnsupportedDTypeForDevice (deviceType :: DeviceType) (dtype :: DType) where ...

Equations

UnsupportedDTypeForDevice deviceType dtype = TypeError (((('Text "This operation does not support " ':<>: 'ShowType dtype) ':<>: 'Text " tensors on devices of type ") ':<>: 'ShowType deviceType) ':<>: 'Text ".") :: Constraint

type family StandardFloatingPointDTypeValidation (device :: (DeviceType, Nat)) (dtype :: DType) where ...

Equations

StandardFloatingPointDTypeValidation '('CPU, 0) dtype = (DTypeIsFloatingPoint '('CPU, 0) dtype, DTypeIsNotHalf '('CPU, 0) dtype)

StandardFloatingPointDTypeValidation '('MPS, 0) dtype = (DTypeIsFloatingPoint '('MPS, 0) dtype, DTypeIsNotHalf '('MPS, 0) dtype)

StandardFloatingPointDTypeValidation '('CUDA, deviceIndex) dtype = DTypeIsFloatingPoint '('CUDA, deviceIndex) dtype

StandardFloatingPointDTypeValidation '(deviceType, _1) dtype = UnsupportedDTypeForDevice deviceType dtype

type family StandardDTypeValidation (device :: (DeviceType, Nat)) (dtype :: DType) where ...

Equations

StandardDTypeValidation '('CPU, 0) dtype = (DTypeIsNotBool '('CPU, 0) dtype, DTypeIsNotHalf '('CPU, 0) dtype)

StandardDTypeValidation '('CUDA, deviceIndex) dtype = DTypeIsNotBool '('CUDA, deviceIndex) dtype

StandardDTypeValidation '(deviceType, _1) dtype = UnsupportedDTypeForDevice deviceType dtype

unsafeConstraint :: (c => a) -> a

withNat :: Int -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r

forEachNat :: forall (n :: Nat) a. KnownNat n => (forall (i :: Nat). KnownNat i => Proxy i -> a) -> [a]