Torch.Typed.Auxiliary

Documentation

natValI :: forall n. KnownNat n => Int

natValInt16 :: forall n. KnownNat n => Int16

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

Equations

Fst '(x, _) = x

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

Equations

Snd '(_, x) = x

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

Equations

Fst3 '(x, _, _) = x

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

Equations

Snd3 '(_, x, _) = x

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

Equations

Trd3 '(_, _, x) = x

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

Equations

DimOutOfBoundCheckImpl shape dim '[] _ = DimOutOfBound shape dim

DimOutOfBoundCheckImpl _ _ _ 0 = ()

DimOutOfBoundCheckImpl shape dim (_ ': xs) n = DimOutOfBoundCheckImpl shape dim xs (n - 1)

type DimOutOfBoundCheck shape dim = DimOutOfBoundCheckImpl shape dim shape dim

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

Equations

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

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

Equations

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

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

Equations

AppendToMaybe h Nothing = Nothing

AppendToMaybe h (Just t) = Just (h : t)

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

Equations

AppendToMaybe' Nothing _ = Nothing

AppendToMaybe' _ Nothing = Nothing

AppendToMaybe' (Just h) (Just t) = Just (h : t)

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

Equations

MaybePrepend Nothing t = t

MaybePrepend (Just h) t = h : t

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

Equations

LastDim (_ ': '[]) = 0

LastDim (_ ': t) = 1 + LastDim t

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

Equations

Product '[] = 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 n = BackwardsImpl (LastDim l) n

type IsSuffixOf xs ys = 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) :: Constraint where ...

Equations

CheckIsSuffixOf _ _ 'True = ()

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

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

Equations

IsSuffixOfImpl xs ys ('Just delta) = xs == DropLength delta ys

IsSuffixOfImpl _ _ 'Nothing = 'False

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

Equations

DropLengthMaybe '[] ys = 'Just ys

DropLengthMaybe _ '[] = 'Nothing

DropLengthMaybe (_ : xs) (_ : ys) = DropLengthMaybe xs ys

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

Equations

DropLength '[] ys = ys

DropLength _ '[] = '[]

DropLength (_ : xs) (_ : ys) = DropLength xs ys

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

Equations

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

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

Init (x ': xs) = x ': Init xs

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

Equations

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

Last (x ': '[]) = x

Last (x ': xs) = Last xs

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

Equations

InsertImpl 0 x l = Just (x ': l)

InsertImpl n x '[] = Nothing

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

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

Equations

CheckInsert _ _ _ (Just xs) = xs

CheckInsert n x l Nothing = DimOutOfBound l n

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

Equations

Insert n x l = CheckInsert n x l (InsertImpl n x l)

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

Equations

RemoveImpl (h ': t) 0 = Just t

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

RemoveImpl _ _ = Nothing

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

Equations

CheckRemove l n Nothing = DimOutOfBound l n

CheckRemove _ _ (Just result) = result

type Remove l n = CheckRemove l n (RemoveImpl l n)

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

Equations

IndexImpl (h ': t) 0 = Just h

IndexImpl (h ': t) n = IndexImpl t (n - 1)

IndexImpl _ _ = Nothing

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

Equations

CheckIndex l n Nothing = DimOutOfBound l n

CheckIndex _ _ (Just result) = result

type Index l n = CheckIndex l n (IndexImpl l n)

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

Equations

InRangeCheck _ _ _ 'LT = ()

InRangeCheck shape dim idx _ = IndexOutOfBound shape dim idx

type InRange shape dim idx = InRangeCheck shape dim idx (CmpNat idx (Index shape dim))

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

Equations

ReverseImpl '[] acc = acc

ReverseImpl (h ': t) acc = ReverseImpl t (h ': acc)

type Reverse l = ReverseImpl l '[]

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

Equations

ExtractDim 0 (h ': _) = Just h

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

ExtractDim _ _ = Nothing

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

Equations

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

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

ReplaceDim _ _ _ = Nothing

type family If c t e where ...

Equations

If 'True t e = t

If 'False t e = e

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

Equations

AllDimsPositive '[] = ()

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

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

Equations

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

IsAtLeast _ _ _ = ()

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 _ _ = 'GT

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

Equations

DTypePromotionImpl UInt8 Int8 _ = Int16

DTypePromotionImpl Int8 UInt8 _ = Int16

DTypePromotionImpl dtype _ EQ = dtype

DTypePromotionImpl _ dtype LT = dtype

DTypePromotionImpl dtype _ GT = dtype

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

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

Equations

DTypeIsFloatingPoint _ 'Half = ()

DTypeIsFloatingPoint _ 'Float = ()

DTypeIsFloatingPoint _ 'Double = ()

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

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

Equations

DTypeIsIntegral _ 'Bool = ()

DTypeIsIntegral _ 'UInt8 = ()

DTypeIsIntegral _ 'Int8 = ()

DTypeIsIntegral _ 'Int16 = ()

DTypeIsIntegral _ 'Int32 = ()

DTypeIsIntegral _ 'Int64 = ()

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

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

Equations

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

DTypeIsNotHalf _ _ = ()

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

Equations

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

DTypeIsNotBool _ _ = ()

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

Equations

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

type family StandardFloatingPointDTypeValidation (device :: (DeviceType, Nat)) (dtype :: DType) :: Constraint 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, _) dtype = UnsupportedDTypeForDevice deviceType dtype

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

Equations

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

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

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

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

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

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