CODEWITHSUNDEEP
idrisdependent-type
joel
joel

Reputation: 7867

Constrain collection of dependent types to match between args and return

I want to write a function that takes in a collection (I'm not too fussed what kind) of dependent types, and returns another collection of the same types but perhaps with different values. The elements are of the form

data Tensor : (Vect r Nat) -> Type where

For example, a function that accepts a (Tensor [2, 3, 4], Tensor [2], Tensor []) or (Tensor [3],) and returns values of the same type.

What I've tried

Upvotes: 1

Views: 53

Answers (1)

Cactus
Cactus

Reputation: 27626

You can write a function that is indexed by the complete shape of all the Tensors, not just any one of them. The shape of each Tensor is a List Nat, so the shape of a list of them is a List (List Nat):

import Data.Vect 

data Tensor : (Vect r Nat) -> Type where

data Tensors : List (List Nat) -> Type where
  Nil : Tensors []
  Cons : Tensor (fromList ns) -> Tensors nss ->  Tensors (ns :: nss)

Here's an example of a shape-preserving map function:

mapTensors 
  : ({0 r : Nat} -> {0 ns : Vect r Nat} -> Tensor ns -> Tensor ns) -> 
  Tensors nss -> Tensors nss
mapTensors f Nil = Nil
mapTensors f (Cons t ts) = Cons (f t) (mapTensors f ts)

Upvotes: 1

Related Questions