证明任意嵌套的Vect别名是可显示的

如何解决证明任意嵌套的Vect别名是可显示的

我一直试图找出如何为我的Show类型实现Tensor的年龄。 Tensor是单个值或任意嵌套的Vect个值的精简包装器

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

我明白了

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)

鉴于array_type的重要性，这是可以理解的。我相信它应该show是可行的，因为我可以show在REPL中高度嵌套的Vect，只要它们的元素是Show。我想Idris只是不知道它是任意嵌套的Vect。

如果我引入一些隐式参数并按大小/形状区分大小写，我会到达某个地方

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

，我可以将其无限期地扩展到越来越高的级别， ，其中RHS始终只是show x，但我不知道如何获取它进行类型检查所有级别。我猜想需要一些递归的东西。

编辑，我想知道如何通过使用Idris对Show的{​​{1}}的实现来做到这一点。我希望避免自己亲自构造实现。

解决方法

如果您想通过Show (Vect n a)实现，也可以通过定义Show实现来实现，该实现要求向量必须有Show：>

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

对于shape的所有选择，Show (array_type shape dtype)约束将减少为Show dtype，例如可行：

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

*ShowVect> show myTensor 
"[[[1,6]]]" : String

,

您的方向正确：您可以通过在嵌套向量上编写递归函数，然后在Tensor实现中将其提升为Show类型来实现：

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

示例：

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