3.2 KiB
Welcome to Idris2!
Idris is a programming language designed to encourage Type-Driven Development.
Getting started
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.
Libraries shipped with the compiler
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.
Prelude
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
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.
Contrib
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
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.
Papers
papers is not installed by default.
It contains complex examples that are lifted from academic papers using dependent typeds
and demonstrates advanced language features.