为归纳定义的类型寻找实现(显示) [英] Finding an implementation (of show) for an inductively defined type

问题描述

以下代码段来自 (https://stackoverflow.com/a/37461290/2129302):>

The following snippet was from (https://stackoverflow.com/a/37461290/2129302):

tensor : Vect n Nat -> Type -> Type
tensor []        a = a
tensor (m :: ms) a = Vect m (tensor ms a)

我想定义以下内容:

mkStr : (Show a) => tensor shape a -> String
mkStr x = show x

但是这会产生以下错误:

But instead this gives the following error:

Can't find implementation for Show (tensor shape a)

但是，在 REPL 上，我可以运行show [some tensor value...]".为什么会这样，我可以做些什么来解决它?

However, on the REPL I can run "show [some tensor value...]". Why is this and what can I do to fix it?

推荐答案

您不是在显示 a，而是在显示 张量形状 a.因此，以下应该有效，您需要以下一种方式编写类型:

You're not showing a, you're showing tensor shape a. Thus, the following should work and you need to write type in the next way:

mkStr : (Show (tensor shape a)) => tensor shape a -> String
mkStr x = show x

这篇关于为归纳定义的类型寻找实现(显示)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！