如何使用带有参数化元组的接口？答案

【问题标题】：How to use interfaces with parameterized tuple?如何使用带有参数化元组的接口？
【发布时间】：2022-08-20 09:27:46
【问题描述】：

我有 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)，但看起来这是不可能的。 Here 是关于它的链接问题。

将Coords 定义为Vect 的Fins 可能会容易得多。
@michaelmesser，我不认为这是可能的，因为每个维度都有不同的大小，所以每个坐标组件都有不同的类型。例如(Fin 2, Fin 3)。
然后使用All 而不是Vect

标签： idris idris2

【解决方案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

您也可以尝试使用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

【讨论】：