A purely functional programming language with first class types
Go to file
Vit Brunner b1040a26b3 Appease the linter
Hey I haven't even touched those things!
2022-03-14 18:13:57 +01:00
.github [ ci ] install mingw64 gcc for windows (#2338) 2022-03-03 22:29:25 +00:00
benchmark [ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
bootstrap Detect ARM Macs as a Darwin OS 2021-11-03 08:43:32 +00:00
docs Fix links to GitHub wiki 2022-03-11 20:31:43 +01:00
icons Add icons 2020-05-20 18:48:55 +01:00
libs [ refactor ] Factor out a type for primitive types out of Constant 2022-03-10 23:07:20 +00:00
lint Lint utility 2021-01-16 10:00:03 +00:00
nix [ nix ] fix bitrot 2021-12-31 09:16:35 -08:00
Release Experimental Scheme based evaluator (#1956) 2021-09-24 20:38:55 +01:00
samples [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
src [ refactor ] Factor out a type for primitive types out of Constant 2022-03-10 23:07:20 +00:00
support [ fix ] euclidian mod and div for scheme backends 2022-03-08 17:40:29 +00:00
tests [ refactor ] Factor out a type for primitive types out of Constant 2022-03-10 23:07:20 +00:00
.editorconfig [ install ] Check if 'realpath' exists for Chez and Racket backends (#1210) 2021-04-06 15:42:04 +01:00
.gitattributes Mark bootstrap code as generated 2021-06-30 22:11:54 +01:00
.gitignore Add %deprecate pragma (#2086) 2021-11-17 10:41:03 +00:00
bootstrap-stage1-chez.sh Write files into bootstrap-build directory during bootstrap 2021-07-04 03:17:13 +01:00
bootstrap-stage1-racket.sh Write files into bootstrap-build directory during bootstrap 2021-07-04 03:17:13 +01:00
bootstrap-stage2.sh [fix] Loading libidris2_support.dll with Racket (#1583) 2021-07-21 14:35:21 +01:00
CHANGELOG.md [ refactor ] Factor out a type for primitive types out of Constant 2022-03-10 23:07:20 +00:00
config.mk [fix] Loading libidris2_support.dll with Racket (#1583) 2021-07-21 14:35:21 +01:00
CONTRIBUTING.md Appease the linter 2022-03-14 18:13:57 +01:00
CONTRIBUTORS make writeBufferData return the number of bytes that have been written (#2276) 2022-01-25 13:25:06 +00:00
default.nix Nix fixes (#1623) 2021-06-28 11:47:47 +01:00
flake.lock Use chez-racket from mainline Nixpkgs 2021-12-29 18:33:05 -08:00
flake.nix Use chez-racket from mainline Nixpkgs 2021-12-29 18:33:05 -08:00
idris2.ipkg Support for incremental compilation with Chez 2021-06-27 15:40:23 +01:00
idris2api.ipkg [ doc ] :printdef for interface implementations (#2340) 2022-03-07 11:47:20 +00:00
idris2protocols.ipkg.hide [ refactor ] More IDE protocol (#2238) 2022-01-06 10:09:29 +00:00
INSTALL.md [ typo ] In INSTALL.md 2021-10-23 15:16:23 +01:00
LICENSE Add licence and changelog and update REAMDE 2020-05-20 11:31:48 +01:00
Makefile [ libs ] move propaganda out of contrib (#2213) 2022-01-25 12:25:55 +00:00
README.md Appease the linter 2022-03-14 18:13:57 +01:00

Idris 2

Documentation Status Build Status

Idris 2 is a purely functional programming language with first class types.

For full installation instructions, see INSTALL.md. Briefly, if you have Chez Scheme installed, with the executable name chez, type:

  • make bootstrap SCHEME=chez
  • make install

You may need to change chez to be the local name of your Chez Scheme. This is often one of scheme, chezscheme or chezscheme9.5 (depending on the version). On a modern desktop machine, this process (including tests) should take less than 5 minutes.

Idris 2 is mostly backward compatible with Idris 1, with some minor exceptions. The most notable user visible differences, which might cause Idris 1 programs to fail to type check, are:

  • Unbound implicit arguments are always erased, so it is a type error to attempt to pattern match on one.

  • Simplified resolution of ambiguous names, which might mean you need to explicitly disambiguate more often. As a general rule, Idris 2 will be able to disambiguate between names which have different concrete return types (such as data constructors), or which have different concrete argument types (such as record projections). It may struggle to resolve ambiguities if one name requires an interface to be resolved.

  • The cong function now takes its congruence explicitly as its first argument.

  • Minor differences in the meaning of export modifiers private, export, and public export, which now refer to visibility of names from other namespaces rather than visibility from other files.

  • Module names must match the filename in which they are defined (unless the module's name is "Main").

  • Anything which uses a %language pragma in Idris 1 is likely to be different. Notably, elaborator reflection will exist, but most likely in a slightly different form because the internal details of the elaborator are different.

  • The Prelude is much smaller (and easier to replace with an alternative). Command-line option --no-prelude can be used to not implicitly import Prelude.

  • let x = val in e no longer computes with x in e, instead being essentially equivalent to (\x => e) val. This is to make the behaviour of let consistent in the presence of case and with (where it is hard to push the computation inside the case/with efficiently). Instead, you can define functions locally with let, which do have computational force, as follows:

    let x : ?
        x = val in
        e
    

Watch this space for more details and the rationale for the changes, as I get around to writing it...

Summary of new features:

  • A core language based on "Quantitative Type Theory" which allows explicit annotation of erased types, and linear types.
  • let bindings are now more expressive, and can be used to define pattern matching functions locally.
  • Names which are in scope in a type are also always in scope in the body of the corresponding definition.
  • Better inference. Holes are global to a source file, rather than local to a definition, meaning that some holes can be left in function types to be inferred by the type checker. This also gives better inference for the types of case expressions, and means fewer annotations are needed in interface declarations.
  • Better type checker implementation which minimises the need for compile time evaluation.
  • New Chez Scheme based backend which both compiles and runs faster than the default Idris 1 backend. (Also, optionally, Racket and Gambit can be used as targets).
  • Everything works faster :).

A significant change in the implementation is that there is an intermediate language TTImp, which is essentially a desugared Idris, and is cleanly separated from the high level language which means it is potentially usable as a core language for other high level syntaxes.

JavaScript

The JavaScript codegen uses the new BigInt, hence Node.js 10.4 or higher is required.

Editor Plugins

The wiki lists the current plugins available for common text editors and their features.

Things still missing

  • Cumulativity (so we currently have Type : Type! Bear that in mind when you think you've proved something :))
  • 'rewrite' doesn't yet work on dependent types

Contributions wanted

If you want to learn about Idris more, contributing to the compiler could be one way to do so. Just select one good first issue and ask about it on the Discord channel.

Talks

Edwin Brady Tells Us What's New in Idris 2 (Berlin Functional Programming Group)

Scheme Workshop Keynote (ACM SIGPLAN)

Idris 2 - Type-driven Development of Idris (Curry On - London 2019)

Idris 2: Type-driven Development of Idris (Code Mesh LDN 18)