Idris2:有没有在接口实现中使用隐含的方法

Question

我使用Idris2通过Idris跟踪TDD。我在第6章中使用模式处理DataStore。首先，对于一些上下文：

infixr 5 .+.

data Schema = SString
            | SInt
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

在某些情况下，我们希望格式化SchemaType schema类型的值以显示给用户。在这本书中，这个问题通过一个display函数得到了解决，如下所示：

display : SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = (x .+. y)} (iteml, itemr) = display iteml ++ ", " ++ display itemr

我想知道是否可以使用Show接口，这样我就可以直接调用show item了。

我尝试了以下几种方法：

Show (SchemaType schema) where
  show {schema = SString} item = show item  
  show {schema = SInt} item = show item
  show {schema = (x .+. y)} (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")" 

但它告诉我模式将被擦除，因此不能使用。

我试图让idris在运行时保留它，但我只是猜测语法并得到错误，我真的不知道如何解释。

尝试1：

{schema:_} -> Show (SchemaType schema) where
  show {schema = SString} item = show item  
  show {schema = SInt} item = show item 
  show {schema = (x .+. y)} (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

抛出：

Error: While processing left hand side of show. Can't match on ?postpone [no locals in scope] (Non linear pattern variable).

/home/stefan/dev/tdd-idris/SchemaDataStore.idr:27:33--27:34
 23 |
 24 | {schema:_} -> Show (SchemaType schema) where
 25 |   show {schema = SString} item = show item
 26 |   show {schema = SInt} item = show item
 27 |   show {schema = (x .+. y)} (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
                                      ^

尝试2：

Show ({schema:_} -> SchemaType schema) where
  show {schema = SString} item = show item  
  show {schema = SInt} item = show item 
  show {schema = (x .+. y)} (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

抛出：

Error: While processing left hand side of show. schema is not a valid argument in show ?item.

/home/stefan/dev/tdd-idris/SchemaDataStore.idr:25:3--25:31
 24 | Show ({schema:_} -> SchemaType schema) where
 25 |   show {schema = SString} item = show item
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

尝试3

Show (SchemaType schema) where
  show item =
    case (schema, item) of
       (SString,  str)            => show str
       (SInt,     int)            => show int
       ((x .+. y), (left, right)) => "(" ++ show x ++ ", " ++ show y ++ ")"

抛出：

Error: While processing right hand side of show. Sorry, I can't find any elaboration which works. If Builtin.Pair: schema is not accessible in this context.

/home/stefan/dev/tdd-idris/SchemaDataStore.idr:26:11--26:17
 24 | Show (SchemaType schema) where
 25 |   show item =
 26 |     case (schema, item) of
                ^^^^^^

有没有人能开导一下我？我是不是在尝试一些不可能的事情，我是不是把语法搞错了？

Answer 1

schema不是show的参数。我想这就是你想要的：

{schema : _} -> Show (SchemaType schema) where
  show item =
    case (schema, item) of
       (SString,  str)            => show str
       (SInt,     int)            => show int
       ((x .+. y), (left, right)) => "(" ++ show x ++ ", " ++ show y ++ ")"

然而，这会产生另一个错误，因为类型类实际上只适用于data，而您正在将其与函数一起使用。也许不一致上的某个人(在标签描述中)知道如何让它工作。Idris堆栈溢出不是很活跃。

Answer 2

这个怎么样。

infixr 5 .+.

data Schema = SString
            | SInt
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)


namespace AdHoc
  public export
  show : {scm : _} -> SchemaType scm -> String
  show {scm = SString } str = show str
  show {scm = SInt    } num = show num
  show {scm = (a .+. b)} (x, y) = "(" ++ AdHoc.show x ++ ", " ++ AdHoc.show y ++ ")"

main : IO ()
main = putStrLn $ show {scm = (SString .+. SInt)} ("adhoc", 0)