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

问题描述

我正在使用 Idris2 跟踪 Idris 的 TDD。我在第 6 章中使用模式处理 DataStore。首先是一些上下文：

--we're going to use a temp table; make sure it doesn't already exist
if (object_id('tempdb..#tmpTbl') is not null)
    drop table #tmpTbl

--initial query to retrieve all the columns
select *
into #tmpTbl
from TblWithManycolumns

--update column(s) from another table or query
update #tmpTbl
set ColToBeReplaced = trv.ColWithReplacementValue
from #tmpTbl t
join TableWithReplacementValue trv
    on trv.KeyCol = t.KeyCol
--where trv.FilterCol = @FilterVal -- if needed

--this select contains the final output data
select * from #tmpTbl
drop table #tmpTbl

有时我们希望格式化 TblWithManyColumns 类型的值以显示给用户。在这本书中，这个问题用一个 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

但它告诉我模式将被删除，因此无法使用。

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

尝试 1：

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 ++ ")" 

尝试 2：

{schema:_} -> Show (SchemaType schema) where
  show {schema = SString} item = show item  
  show {schema = SInt} item = show item 
  show {schema = (x .+. y)} (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," ++ show y ++ ")"
                                      ^

尝试 3

Show ({schema:_} -> SchemaType schema) where
  show {schema = SString} item = show item  
  show {schema = SInt} item = show item 
  show {schema = (x .+. y)} (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
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

有人能指教我吗？我是不是在尝试一些不可能的事情，我是不是语法错误？

解决方法

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

,

这个怎么样。

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)