Idris is a programming language designed to encourage Type-Driven Development.
Once you have installed Idris2
you can write a simple hello-world by opening a Main.idr file and writing:
module Main
||| My first Idris2 function
main : IO ()
main = putStrLn "Hello, and welcome to Idris2!"
You can run this example by using the --exec ENTRYPOINT option.
The command idris2 --exec main Main.idr will compile the module and immediately run main.
The line starting with a triple pipe (|||) attaches documentation to the identifier. You
can consult it by loading the file in the REPL (idris2 Main.idr) and querying the compiler
using the :doc command: :doc main will return:
Main.main : IO ()
My first Idris2 function
Visibility: private
You should be able to use :doc on identifiers (e.g. main, IO, (), putStrLn, etc.) and
keywords (module, :, =, private, etc.) and hopefully get helpful information.
Here are links to the automatically generated documentation for the libraries shipped with the bleeding edge version of the compiler. The documentation for the latest released version is available on the idris-lang.org site.
The prelude is always implicitly loaded unless you use the --no-prelude command-line option.
This is where the built-in types are bound, where the core data types (List, Nat, Equal, etc.)
and interfaces (Eq, Show, Functor, etc.) are defined.
base contains all the basics needed to write small programs. Its modules can be used by adding
an import statement to the top of your file.
In Data.List for instance you
will find functions to take or drop values from a list, or partition it using a given predicate.
You can explore the content of a namespace like Data.List by using :browse Data.List in the REPL.
For more information about specific entries, you can then use :doc.
The contrib library contains a bit of everything. It will eventually be disbanded in favour of
third-party packages once we have a convenient package manager. To use modules defined in it, you
can pass the -p contrib option to idris2.
linear is the add-on to base you'll need for programs using linearity. Similarly to contrib,
you will need to pass -p linear to idris2 to use modules defined in it.
network is the add-on to base you'll need for programs using sockets.
Similarly to contrib and linear, you will need to pass -p network
to idris2 to use modules defined in it.
test is the add-on to base you'll need to write test suites.
Similarly to other add-ons, you will need to pass -p test to
idris2 to use modules defined in it.
papers is not installed by default.
It contains complex examples that are lifted from academic papers using dependent typeds
and demonstrates advanced language features.