Idris2：有没有办法在接口实现中使用隐式答案

【问题标题】：Idris2: Is there a way use implicits in interface implementationsIdris2：有没有办法在接口实现中使用隐式
【发布时间】：2021-05-13 16:02:37
【问题描述】：

我正在使用 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
                ^^^^^^

有人可以请教我吗？我是否尝试了一些不可能的事情，我只是语法错误吗？

【问题讨论】：

标签： interface idris implicit-parameters

【解决方案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，并且您正在将它与函数一起使用。也许 Discord 上的某个人（在标签描述中）知道如何让它工作。 Idris 堆栈溢出不是很活跃。

【讨论】：