时间戳

首页 > 解决方案 > 证明任意嵌套的 Vect 别名是可显示的

type-inference - 证明任意嵌套的 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能够，因为我可以在 REPL 中show高度嵌套Vects，只要它们的元素是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 的Showfor Vects 实现来做到这一点。我想避免自己手动构建实现。

标签： type-inferenceidrisdependent-type

解决方案

如果你想通过Show (Vect n a)实现，你也可以这样做，通过定义一个Show需要有一个Showfor 向量的实现：

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, 2, 3], [4, 5, 6]]]

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

推荐阅读