Prove arbitrarily-nested Vect alias is showable

1
votes

I've been trying to figure out how to implement Show for my Tensor type for ages. Tensor is a thin wrapper round either a single value, or arbitrarily-nested Vects of values

import Data.Vect

Shape : Nat -> Type
Shape rank = Vect rank Nat

array_type: (shape: Shape rank) -> (dtype: Type) -> Type
array_type [] dtype = dtype
array_type (d :: ds) dtype = Vect d (array_type ds dtype)

data Tensor : (shape: Shape rank) -> (dtype: Type) -> Type where
  MkTensor : array_type shape dtype -> Tensor shape dtype

Show dtype => Show (Tensor shape dtype) where
  show (MkTensor x) = show x

I get

When checking right hand side of Prelude.Show.Main.Tensor shape dtype implementation of Prelude.Show.Show, method show with expected type
        String

Can't find implementation for Show (array_type shape dtype)

which is understandable given array_type's not trivial. I believe that it should be showable, as I can show highly-nested Vects in the REPL as long their elements are Show. I guess Idris just doesn't know it's an arbitrarily nested Vect.

If I pull in some implicit parameters and case split on rank/shape, I get somewhere

Show dtype => Show (Tensor {rank} shape dtype) where
  show {rank = Z} {shape = []} (MkTensor x) = show x  -- works
  show {rank = (S Z)} {shape = (d :: [])} (MkTensor x) = show x  -- works
  show {rank = (S k)} {shape = (d :: ds)} (MkTensor x) = show x  -- doesn't work

and I can indefinitely expand this to higher and higher rank explicitly, where the RHS is always just show x, but I can't figure out how to get this to type check for all ranks. I'd guess some recursive thing is required.

EDIT to be clear, I want to know how to do this by using Idris' implementation of Show for Vects. I want to avoid having to construct an implementation manually myself.

2
type-inferenceidrisdependent-type

2 Answers

2
votes

If you want to go via the Show (Vect n a) implementations, you can do that as well, by defining a Show implementation that requires that there is a Show for the vector:

import Data.Vect
import Data.List

Shape : Nat -> Type
Shape rank = Vect rank Nat

array_type: (shape: Shape rank) -> (dtype: Type) -> Type
array_type [] dtype = dtype
array_type (d :: ds) dtype = Vect d (array_type ds dtype)

data Tensor : (shape: Shape rank) -> (dtype: Type) -> Type where
  MkTensor : array_type shape dtype -> Tensor shape dtype

Show (array_type shape dtype) => Show (Tensor {rank} shape dtype) where
  show (MkTensor x) = show x

For all choices of shape, the Show (array_type shape dtype) constraint will reduce to Show dtype, so e.g. this works:

myTensor : Tensor [1, 2, 3] Int
myTensor = MkTensor [[[1, 2, 3], [4, 5, 6]]]

*ShowVect> show myTensor 
"[[[1, 2, 3], [4, 5, 6]]]" : String
1
votes

You were on the right track: you can do it by writing a recursive function over the nested vectors, and then lifting it to your Tensor type in the Show implementation:

showV : Show dtype => array_type shape dtype -> String
showV {rank = 0} {shape = []} x = show x
showV {rank = (S k)} {shape = d :: ds} xs = combine $ map showV xs
  where
    combine : Vect n String -> String
    combine ss = "[" ++ concat (intersperse ", " . toList $ ss) ++ "]"

Show dtype => Show (Tensor {rank} shape dtype) where
  show (MkTensor x) = showV x

Example:

λΠ> show $ the (Tensor [1, 2, 3] Int) $ MkTensor [[[1, 2, 3], [4, 5, 6]]]
"[[[1, 2, 3], [4, 5, 6]]]"