0

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

有人可以启发我吗？我是否在尝试一些不可能的事情，我只是弄错了语法吗？

4

1 回答 1

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 堆栈溢出不是很活跃。

于 2021-05-13T16:16:13.117 回答