Как создать пустой список в Idris REPL?

Question

Я хочу создать myEmptyList и myNonemptyList в REPL.Однако Idris сообщил об ошибке несоответствия типов для myEmptyList.Почему?

     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     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]

Answer 1

Несоответствие объясняется тем, что :let myEmptyList : List Integer = [] не определяет myEmptyList, он только объявляет свой тип как List Integer = [], тип равенства, который неправильно набран, потому что [] и List Integer имеют разные типы.

Вы можете определить myEmptyList следующим образом: :let myEmptyList : List Integer; myEmptyList = [] или, альтернативно, :let myEmptyList = the (List Integer) [].