如何使用参数化元组的接口

Question

我有一个Coord函数，它将n维大小转换为以给定大小为界的坐标类型：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 s:

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
^^^^^^

早些时候，我尝试实现Show (Coord s)，但看起来这是不可能的。这是关于它的相关问题。

Answer 1

您可以制作自己的类似列表的数据类型：

data Coords : List Nat -> Type where
Nil : Coords []
(::) : Fin x -> Coords xs -> Coords (x :: xs)
toList : Coords xs -> List Nat
toList [] = []
toList (x::xs) = finToNat x :: toList xs
example : Coords [2, 3]
example = [1, 2]
Show (Coords xs) where
show cs = show $ toList cs

您也可以尝试使用Data.Vect.Quantifiers.All或Data.List.Quantifiers.All:

import Data.Vect
import Data.Vect.Quantifiers
example : All Fin [1, 2, 3]
example = [0, 1, 2]
-- not sure why this is isn't included with Idris
export
All (Show . p) xs => Show (All p xs) where
show pxs = "[" ++ show' "" pxs ++ "]"
where
show' : String -> All (Show . p) xs' => All p xs' -> String
show' acc @{[]} [] = acc
show' acc @{[_]} [px] = acc ++ show px
show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
string : String
string = show example