Отличаются ли списки символов от строк в Idris?

Question

В Haskell следующее выдает «hello»: putStrLn (['h', 'e', 'l', 'l', 'o']), однако это приводит к ошибке компиляции в Idris:

48 | main = do
   |        ~~ ...
When checking right hand side of main with expected type
        IO ()

When checking an application of function Prelude.Interactive.putStrLn:
        Can't disambiguate since no name has a suitable type:
                Prelude.List.::, Prelude.Stream.::

Я подозреваю, что это потому, что String встроен в Idris, а не в Haskell. Тем не менее, может ли класс типов использоваться в Idris для обработки List Char как экземпляра String (были String классом типа)?

Answer 1

Правильно, строки не совпадают со списком символов в Idris.Но есть функции, которые позволяют вам превращать список символов в строку и наоборот.

unpack превращает строку в список символов

pack функция превращает складываемые символы в строку

Таким образом, для печати списка символов вам просто необходимо:

putStrLn $ pack ['h', 'e', 'l', 'l', 'o']