代码之家 › 专栏 › 技术社区 › Yang Bo

如何在Idris REPL中创建空列表?

dependent-type idris typechecking read-eval-print-loop list

2

Yang Bo · 技术社区 · 7 年前

myEmptyList 和 myNonemptyList 我的空列表

     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.0
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Idris> :let myEmptyList : List Integer = []
(input):1:33: When checking type of myEmptyList:
When checking argument y to type constructor =:
        Type mismatch between
                List elem (Type of [])
        and
                Type (Expected type)
(input):1:18:No type declaration for myEmptyList
Idris> :let myNonemptyList : List Integer = [42]

1 回复 | 直到 7 年前

1

4

András Kovács 7 年前

不匹配是因为 :let myEmptyList : List Integer = [] myEmptyList ,它仅将其类型声明为 List Integer = [] ,是一个相等类型,由于 [] List Integer 有不同的类型。

你可以定义具体如下: :let myEmptyList : List Integer; myEmptyList = [] ,或者 :let myEmptyList = the (List Integer) [] .