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
docs.idris-lang.org. 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.
instancekeywords have been deprecated. The
classkeyword 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
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.
Fractionalinterface, with functions
- New command
:watchwhich watches the currently loaded file, and reloads it if it has been changed.
- Idris’ logging infrastructure has been categorised. Command line and repl are available. For command line the option
--logging-categories CATSis used to pass in the categories. Here
CATSis a colon separated quoted string containing the categories to log. The REPL command is
logcats CATS, where
CATSis a whitespace separated list of categories. Default is for all categories to be logged.
- New flag
--listlogcatsto 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 irc.freenode.net.