Idris for Haskellers

Things to look out for when expecting Idris to be Haskell:

• Top level functions must have type annotations.
• Functions and data types must be defined in the source file before it can be used. Mutually dependent functions can be linked using a mutual block.
• The type given to lists is not indicated using a special syntax i.e. [Int]. Rather the List type is used. For example, [Int] in Haskell is equivalent to List Int. Brackets are used as syntactic sugar for representing a list of values.
• Functions are overloaded, for example, (++) can mean Prelude.List.(++) : List a -> List a -> List a or Prelude.Strings.(++) : String -> String -> String. So Haskell's foldl (++) [] ["1","2"], for example, needs to be written as foldl Strings.(++) "" ["1","2"] if it is not possible to disambiguate between the possible meanings of (++) based on the argument and return types given to (++)
• In Idris String is not represented as a synonym for a list of characters. For example, Haskell's foldl (++) [] ["1","2"] needs to be written as foldl Strings.(++) "" ["1","2"] in Idris but surprisingly concat $ replicate 5 "bla" works just like in Haskell , because String is Monoid and List is Foldable.
• deriving does not work yet.
• Operators for cons and type annotations are swapped. Type annotations are denoted in Idris by : rather than ::. Thus Idris's cons operator is ::.
• In Idris there is no undefined, holes (such as ?hole) can be used instead of undefined. Also, believe_me from the built-in-s can be used to define undefined.
• Haskell's error is in Debug.Error.error (Debug.Error.error is not really like Haskell's error though because it won't get caught like it can in Haskell.)
• Idris' Template-Haskell is "reflected elaboration"
• fmap is map in Idris.
• Record syntax has a slightly different syntax in Idris, notably, records have only one constructor in Idris, unlike in Haskell, where records can have multi constructors. Why this limitation ? Multi constructor records have non-total accessor functions.
• There is no Read typeclass in Idris.
• :let in the REPL should be used instead of just let.
• Unlike GHCI, the Idris REPL is not inside of an implicit IO monad. Use :x in the REPL for executing IO actions.
• 2 :: Int should be written as the Int 2 in Idris.
• Error messages not always tell you yet as clearly as in Haskell what is wrong if your code does not compile. Error messages are helpful for locating roughly where the error is in the source code, but not always yet as to what the error is.
• head does NOT work on arbitrary lists in Idris, only on lists that are non-empty: Prelude.List.head : (l : List a) -> {auto ok : NonEmpty l} -> a
• The arrow in a lambda expression or a case expression in Idris is denoted by => instead of -> (Haskell).
• There should be commas between multiple parameters in lambda expression in Idris like \s, n => s + n instead of \s n -> s + n in Haskell.
• There is no !! infix operator to get an element from a list by its index, use index function instead.
• There is no syntax for type alias in Idris, just use standard functions to define aliases, for example , myNewtype:Type and then myNewtype=(Int, String).
• In Idris type-classes are called interfaces. In Idris it is possible to get hold of the vtable (type class records), pass it around and feed it to functions explicitly (in contrast to Haskell where this can only happen implicitly).