|
1 | 1 | Idris 2 |
2 | 2 | ======= |
3 | 3 |
|
4 | | -[](https://idris2.readthedocs.io/en/latest/?badge=latest) |
5 | | -[](https://github.com/idris-lang/Idris2/actions/workflows/ci-idris2.yml) |
6 | | - |
7 | 4 | [Idris 2](https://idris-lang.org/) is a purely functional programming language |
8 | | -with first class types. |
9 | | - |
10 | | -For full installation instructions, see [INSTALL.md](INSTALL.md). Briefly, if |
11 | | -you have Chez Scheme installed, with the executable name `chez`, type: |
12 | | - |
13 | | -* `make bootstrap SCHEME=chez` |
14 | | -* `make install` |
15 | | - |
16 | | -You may need to change `chez` to be the local name of your Chez Scheme. This |
17 | | -is often one of `scheme`, `chezscheme` or `chezscheme9.5` (depending on the |
18 | | -version). On a modern desktop machine, this process (including tests) |
19 | | -should take less than 5 minutes. |
20 | | - |
21 | | -Idris 2 is mostly backwards compatible with Idris 1, with some minor |
22 | | -exceptions. The most notable user visible differences, which might cause Idris |
23 | | -1 programs to fail to type check, are: |
24 | | - |
25 | | -+ Unbound implicit arguments are always erased, so it is a type error to |
26 | | - attempt to pattern match on one. |
27 | | -+ Simplified resolution of ambiguous names, which might mean you need to |
28 | | - explicitly disambiguate more often. As a general rule, Idris 2 will be able |
29 | | - to disambiguate between names which have different concrete return types |
30 | | - (such as data constructors), or which have different concrete argument |
31 | | - types (such as record projections). It may struggle to resolve ambiguities |
32 | | - if one name requires an interface to be resolved. |
33 | | -+ The `cong` function now takes its congruence explicitly as its first argument. |
34 | | -+ Minor differences in the meaning of export modifiers `private`, `export`, |
35 | | - and `public export`, which now refer to visibility of names from other |
36 | | - *namespaces* rather than visibility from other *files*. |
37 | | -+ Module names must match the filename in which they are defined (unless |
38 | | - the module's name is "Main"). |
39 | | -+ Anything which uses a `%language` pragma in Idris 1 is likely to be different. |
40 | | - Notably, elaborator reflection will exist, but most likely in a slightly |
41 | | - different form because the internal details of the elaborator are different. |
42 | | -+ The `Prelude` is much smaller (and easier to replace with an alternative). |
43 | | - Command-line option `--no-prelude` can be used to not implicitly import `Prelude`. |
44 | | -+ `let x = val in e` no longer computes with `x` in `e`, instead being |
45 | | - essentially equivalent to `(\x => e) val`. This is to make the |
46 | | - behaviour of `let` consistent in the presence of `case` and `with` (where |
47 | | - it is hard to push the computation inside the `case`/`with` efficiently). |
48 | | - Instead, you can define functions locally with `let`, which do have |
49 | | - computational force, as follows: |
50 | | - |
51 | | - let x : ? |
52 | | - x = val in |
53 | | - e |
54 | | - |
55 | | -Watch this space for more details and the rationale for the changes, as I |
56 | | -get around to writing it... |
57 | | - |
58 | | -Summary of new features: |
59 | | - |
60 | | -+ A core language based on "Quantitative Type Theory" which allows explicit |
61 | | - annotation of erased types, and linear types. |
62 | | -+ `let` bindings are now more expressive, and can be used to define pattern |
63 | | - matching functions locally. |
64 | | -+ Names which are in scope in a type are also always in scope in the body of |
65 | | - the corresponding definition. |
66 | | -+ Better inference. Holes are global to a source file, rather than local to |
67 | | - a definition, meaning that some holes can be left in function types to be |
68 | | - inferred by the type checker. This also gives better inference for the types |
69 | | - of `case` expressions, and means fewer annotations are needed in interface |
70 | | - declarations. |
71 | | -+ Better type checker implementation which minimises the need for compile |
72 | | - time evaluation. |
73 | | -+ New Chez Scheme based back end which both compiles and runs faster than the |
74 | | - default Idris 1 back end. (Also, optionally, Racket and Gambit can be used |
75 | | - as targets). |
76 | | -+ Everything works faster :). |
77 | | - |
78 | | -A significant change in the implementation is that there is an intermediate |
79 | | -language `TTImp`, which is essentially a desugared Idris, and is cleanly |
80 | | -separated from the high level language which means it is potentially usable |
81 | | -as a core language for other high level syntaxes. |
82 | | - |
83 | | -Javascript |
84 | | ----------- |
85 | | -The javascript codegen uses the new BigInt, hence nodejs 10.4 or higher is required. |
86 | | - |
87 | | -Editor Plugins |
88 | | --------------- |
89 | | -The [wiki](https://github.com/idris-lang/Idris2/wiki/The-Idris-editor-experience) |
90 | | -lists the current plugins available for common text editors and their features. |
91 | | - |
92 | | -JVM |
93 | | -=== |
94 | | -### Build with Maven |
95 | | -+ To install with tests: `mvn install` |
96 | | -+ To install without tests `mvn install -DskipTests` |
97 | | -+ To recompile libraries without building compiler `mvn install -DskipIdrisCompile` |
98 | | -+ To recompile without building libraries `mvn install -DskipIdrisInstallLibrary` |
99 | | -+ To run all JVM tests `mvn -f tests/pom.xml integration-test` |
100 | | -+ To run a single test `mvn -f tests/pom.xml integration-test -Didris.tests="only=idris2/basic001"` |
101 | | - |
102 | | -Things still missing |
103 | | --------------------- |
104 | | - |
105 | | -+ Cumulativity (so we currently have Type : Type! Bear that in mind when you |
106 | | - think you've proved something :)) |
107 | | -+ 'rewrite' doesn't yet work on dependent types |
108 | | - |
109 | | -Contributions wanted |
110 | | -------------------- |
111 | | - |
112 | | -+ [Contribution guidelines](CONTRIBUTING.md) |
113 | | -+ [Good first issues](https://github.com/idris-lang/Idris2/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22) |
114 | | -+ [Contributors wanted](https://github.com/idris-lang/Idris2/wiki/Contributions-wanted) |
115 | | - |
116 | | -If you want to learn about Idris more, contributing to the compiler could be one |
117 | | -way to do so. Just select one good first issue and ask about it on the [Discord](https://discord.gg/UX68fDs2jc) channel. |
118 | | - |
119 | | -Talks |
120 | | ------ |
121 | | - |
122 | | -[](https://www.youtube.com/watch?v=nbClauMCeds "Edwin Brady Tells Us What's New in Idris 2 (Berlin Functional Programming Group)") |
123 | | - |
124 | | -[](https://www.youtube.com/watch?v=h9YAOaBWuIk "Scheme Workshop Keynote (ACM SIGPLAN)") |
125 | | - |
126 | | -[](https://www.youtube.com/watch?v=DRq2NgeFcO0 "Idris 2 - Type-driven Development of Idris (Curry On - London 2019)") |
127 | | - |
128 | | -[](https://www.youtube.com/watch?v=mOtKD7ml0NU "Idris 2: Type-driven Development of Idris (Code Mesh LDN 18)") |
| 5 | +with first class types. This repository provides Idris 2 compiler targeting JVM bytecode so that Idris 2 compiler and Idris 2 programs can run on the JVM. |
| 6 | + |
| 7 | +## Status: Work in progress - currently building Idris 2 0.3.0 for JVM |
| 8 | + |
| 9 | +## Install |
| 10 | + |
| 11 | +* Download the latest Idris 2 JVM release from here https://github.com/mmhelloworld/idris-jvm/releases/tag/v0.3.0-SNAPSHOT-20210831. |
| 12 | +* Extract the archive and add `idris2` launcher script directory `<EXTRACTED_DIRECTORY_ROOT>/bin` to PATH. |
| 13 | +* Create an environment variable `IDRIS_JVM_HOME` pointing to the extracted directory. |
| 14 | + |
| 15 | +## Example |
| 16 | + |
| 17 | +#### helloworld.idr |
| 18 | + |
| 19 | + ```idris |
| 20 | + module Main |
| 21 | + |
| 22 | + data Tree a = Leaf |
| 23 | + | Node (Tree a) a (Tree a) |
| 24 | + |
| 25 | + inorder : Tree a -> List a |
| 26 | + inorder Leaf = [] |
| 27 | + inorder (Node left a right) = inorder left ++ [a] ++ inorder right |
| 28 | + |
| 29 | + tree : Tree String |
| 30 | + tree = Node |
| 31 | + (Node |
| 32 | + (Node Leaf "3" Leaf) |
| 33 | + "+" |
| 34 | + (Node Leaf "7" Leaf)) |
| 35 | + "/" |
| 36 | + (Node Leaf "2" Leaf) |
| 37 | + |
| 38 | + main : IO () |
| 39 | + main = printLn $ inorder tree |
| 40 | + ``` |
| 41 | + |
| 42 | +#### Compile |
| 43 | + |
| 44 | +`idris helloworld.idr -o main` |
| 45 | + |
| 46 | +#### Run |
| 47 | + |
| 48 | +* On Linux/Mac OS: `java -cp "build/exec/main_app/main.jar:$IDRIS_JVM_HOME/lib/*" main.Main` |
| 49 | +* On Windows: `java -cp "build\exec\main_app\main.jar;%IDRIS_JVM_HOME%\lib\*" main.Main` |
| 50 | + |
| 51 | +## License |
| 52 | +This repository extends [idris-lang/Idris2](https://github.com/idris-lang/Idris2) repository with JVM backend. Files from [idris-lang/Idris2](https://github.com/idris-lang/Idris2) are covered by that repository's [license](https://github.com/idris-lang/Idris2/blob/main/LICENSE). |
| 53 | + |
| 54 | +All other files from this repository are covered by BSD-3-Clause License. See [LICENSE](IDRIS2-LICENSE). |
0 commit comments