如何为参数化元组类型Coord实现Show等接口？

类型定义与问题重现 #

我们定义了Coord类型，将n维尺寸描述（Size类型为List Nat）转换为带约束的坐标类型，例如Coord [2,3]等价于(Fin 2, Fin 3)：

import Data.Fin
import Data.List

Size : Type
Size = List Nat

Coord : Size -> Type
Coord [] = ()
Coord s@(_ :: _) = foldr1 (,) $ map Fin s

尝试调用show函数转换Coord实例时触发错误：

foo : Coord s -> String
foo x = show x

错误信息：

Error: While processing right hand side of foo. Can't find an implementation for Show (Coord s).

 22 | foo : Coord s -> String
 23 | foo x = show x
              ^^^^^^

解决方法 #

Coord是依赖于Size结构的递归类型，需通过递归方式实现Show接口，利用Fin自带的Show实例，结合元组的结构推导：

实现Show接口

-- 空尺寸对应的Coord类型为()，直接实现Show
implementation Show (Coord []) where
  show () = "()"

-- 非空尺寸：Coord (n::ns) 是(Fin n, Coord ns)，只要Coord ns有Show实例即可递归实现
implementation {n : Nat} {ns : Size} -> [Show (Coord ns)] => Show (Coord (n :: ns)) where
  show (finVal, coordRest) = "(" ++ show finVal ++ ", " ++ show coordRest ++ ")"

同理实现Eq接口（支持(==)）

如果需要使用相等判断，用同样的递归逻辑实现Eq：

implementation Eq (Coord []) where
  () == () = True

implementation {n : Nat} {ns : Size} -> [Eq (Coord ns), Eq (Fin n)] => Eq (Coord (n :: ns)) where
  (f1, c1) == (f2, c2) = f1 == f2 && c1 == c2

完成上述实现后，foo函数即可正常编译运行，Idris会根据Size的具体结构自动推导对应的接口实例。

内容的提问来源于stack exchange，提问作者magras