Search code examples
idris

Are character lists different than Strings in Idris?


In Haskell, the following will print "hello": putStrLn (['h', 'e', 'l', 'l', 'o']), however, this results in the compile error in 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.::

My suspicion is that this is because String is a builtin in Idris, but not in Haskell. Still, could a a typeclass be used in Idris to treat List Char as an instance of String (were String a type class)?


Solution

  • That's right, strings are not the same as list of characters in Idris. But there are functions that allow you to turn list of characters into a string and vice versa.

    unpack turns a string into a list of characters

    pack function turns a Foldable of characters into a string

    Thus, in order to print list of characters, you just need:

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