Idris 0.10 Released

A new version of Idris, 0.10, has been released. You can find this on hackage, or from the download page. Documentation is available from There’s only a small number of changes from version 0.9.20, which are detailed below.

Thanks as always to everyone who has contributed, either with code, documentation or by testing and reporting issues. You can find the names of all contributors in the CONTRIBUTORS file in the source repository.

Language Updates

  • The class and instance keywords have been deprecated. The class keyword has been replaced by interface. Instances are now called implementations and are introduced by giving the interface name and parameters. For example:
    interface Eq a where
        (==) : a -> a -> Bool
        (/=) : a -> a -> Bool
        (==) x y = not (/=) x y
        (/=) x y = not (==) x y
    Eq Bool where
        True  == True  = True
        True  == False = False
        False == True  = False
        False == False = True
    Eq a => Eq (Maybe a) where
        Nothing  == Nothing  = True
        Nothing  == (Just _) = False
        (Just _) == Nothing  = False
        (Just a) == (Just b) = a == b

    This is as before, but without the instance keyword.

    The rationale for this change is that interfaces as implemented in Idris have several differences from Haskell type classes, even though they have a lot in common. They can be parameterised by things which are not types (including values and interfaces themselves). They are primarily for overloading interfaces, rather than classifying types, and hence there can be multiple implementations.

  • New Fractional interface, with functions (/) and recip.

REPL Updates

  • New command :watch which watches the currently loaded file, and reloads it if it has been changed.

Miscellaneous Updates

  • Idris’ logging infrastructure has been categorised. Command line and repl are available. For command line the option --logging-categories CATS is used to pass in the categories. Here CATS is a colon separated quoted string containing the categories to log. The REPL command is logcats CATS, where CATS is a whitespace separated list of categories. Default is for all categories to be logged.
  • New flag --listlogcats to list logging categories.

Future Release Plans

Version 1.0 of the Idris language is intended to coincide with the completion of the book
Type Driven Development with Idris. The version of Idris on Hackage will be kept up to date with the latest draft of the book.

Idris is still research software, so we expect there to be bugs. Please don’t keep them to yourself! If you find any problem, please report it on the github issue tracker. It is very helpful if you can also provide a small test case which reproduces your problem.

Also, do let us know how you get on in general either via the mailing list or the #idris channel on