hasktorch-0.2.0.0: Functional differentiable programming in Haskell
Safe HaskellSafe-Inferred
LanguageHaskell2010

Torch.Typed.Auxiliary

Synopsis

Documentation

natValI :: forall n. KnownNat n => Int Source #

natValInt16 :: forall n. KnownNat n => Int16 Source #

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

Equations

Fst '(x, _) = x 

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

Equations

Snd '(_, x) = x 

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

Equations

Fst3 '(x, _, _) = x 

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

Equations

Snd3 '(_, x, _) = x 

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

Equations

Trd3 '(_, _, x) = x 

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

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 Source #

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

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 ... Source #

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 ... Source #

Equations

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

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

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 ... Source #

Equations

MaybePrepend Nothing t = t 
MaybePrepend (Just h) t = h ': t 

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

Equations

LastDim (_ ': '[]) = 0 
LastDim (_ ': t) = 1 + LastDim t 

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

Equations

Product '[] = 1 
Product (x ': xs) = x * Product xs 

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

Equations

BackwardsImpl last n = last - n 

type Backwards l n = BackwardsImpl (LastDim l) n Source #

type IsSuffixOf xs ys = CheckIsSuffixOf xs ys (IsSuffixOfImpl xs ys (DropLengthMaybe xs ys)) Source #

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 ... Source #

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 ... Source #

Equations

IsSuffixOfImpl xs ys ('Just delta) = xs == DropLength delta ys 
IsSuffixOfImpl _ _ 'Nothing = 'False 

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

Equations

DropLengthMaybe '[] ys = 'Just ys 
DropLengthMaybe _ '[] = 'Nothing 
DropLengthMaybe (_ ': xs) (_ ': ys) = DropLengthMaybe xs ys 

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

Equations

DropLength '[] ys = ys 
DropLength _ '[] = '[] 
DropLength (_ ': xs) (_ ': ys) = DropLength xs ys 

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

Equations

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

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

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 ... Source #

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 ... Source #

Equations

CheckInsert _ _ _ (Just xs) = xs 
CheckInsert n x l Nothing = DimOutOfBound l n 

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

Equations

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

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

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 ... Source #

Equations

CheckRemove l n Nothing = DimOutOfBound l n 
CheckRemove _ _ (Just result) = result 

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

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

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 ... Source #

Equations

CheckIndex l n Nothing = DimOutOfBound l n 
CheckIndex _ _ (Just result) = result 

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

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

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)) Source #

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

Equations

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

type Reverse l = ReverseImpl l '[] Source #

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

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 ... Source #

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 ... Source #

Equations

If 'True t e = t 
If 'False t e = e 

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

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 ... Source #

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)) Source #

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

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 ... Source #

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') Source #

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

Equations

DTypeIsFloatingPoint _ 'Half = () 
DTypeIsFloatingPoint _ 'Float = () 
DTypeIsFloatingPoint _ 'Double = () 
DTypeIsFloatingPoint '(deviceType, _) dtype = UnsupportedDTypeForDevice deviceType dtype 

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

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 ... Source #

Equations

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

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

Equations

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

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

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 ... Source #

Equations

StandardFloatingPointDTypeValidation '('CPU, 0) dtype = (DTypeIsFloatingPoint '('CPU, 0) dtype, DTypeIsNotHalf '('CPU, 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 ... Source #

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 Source #

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

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