Module dyn_tensor 

Dynamic tensor types for gradual shape adoption.

This module provides types for working with tensors whose shapes are not known at compile time, enabling gradual adoption of shape-indexed types.

Overview

Shape-indexed tensors (Tensor '[m, n] Float) provide compile-time dimension checking, but sometimes shapes are only known at runtime. DynTensor bridges this gap by providing an existentially-quantified wrapper.

Usage Pattern

-- Convert static to dynamic (always succeeds)
toDynamic :: Tensor shape a -> DynTensor a

-- Convert dynamic to static (may fail at runtime)
fromDynamic :: KnownShape shape => DynTensor a -> Maybe (Tensor shape a)

-- Example:
processData :: DynTensor Float -> IO ()
processData dyn = case fromDynamic @'[1024, 768] dyn of
    Just tensor -> optimizedPath tensor  -- statically known shape
    Nothing     -> fallbackPath dyn      -- dynamic shape handling

Type Signatures

DynTensor :: * -> *

toDynamic :: forall shape a. Tensor shape a -> DynTensor a

fromDynamic :: forall shape a. KnownShape shape
            => DynTensor a -> Maybe (Tensor shape a)

withDynShape :: DynTensor a -> (forall shape. Tensor shape a -> r) -> r

dynShape :: DynTensor a -> [Int]

Functions

dyn_rank_type

Creates the type for dynRank.

dyn_shape_type

Creates the type for dynShape.

dyn_tensor_elem_type

Extracts the element type from a DynTensor a type.

dyn_tensor_of

Creates a DynTensor a type.

dyn_tensor_tycon

Creates the DynTensor type constructor.

from_dynamic_type

Creates the type for fromDynamic.

is_dyn_tensor

Checks if a type is a DynTensor type.

shape_witness_of

Creates a ShapeWitness shape type.

shape_witness_tycon

Creates the ShapeWitness type constructor.

static_shape_witness

Creates a static shape witness type from concrete dimensions.

to_dynamic_type

Creates the type for toDynamic.

with_dyn_shape_type

Creates the type for withDynShape.