edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-27 14:52:10 +03:00
Code Issues Projects Releases Wiki Activity

More documentation refreshing

Browse Source 
That's most of it now - just missing a section on multiplicities, and a
section on the differences from Idris 1.

Ideally, there should also be a much more gentle introduction (basically
doing the same as the first 3 chapters of TypeDD in Idris). But that's
for some other time...
This commit is contained in:
Edwin Brady 2020-02-25 22:33:01 +00:00
parent 16ae7994e7
commit 2ca5509eb6
5 changed files with 34 additions and 674 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
docs/tutorial/conclusions.rst
View File

@ -7,6 +7,9 @@ Further Reading
Further information about Idris programming, and programming with
dependent types in general, can be obtained from various sources:
- `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
by Edwin Brady, available from `Manning <https://www.manning.com>`_.
- The Idris web site (http://www.idris-lang.org/) and by asking
questions on the mailing list.
@ -21,8 +24,8 @@ dependent types in general, can be obtained from various sources:
- https://github.com/idris-lang/Idris-dev/wiki/Language-Features
- Examining the prelude and exploring the ``samples`` in the
distribution. The Idris source can be found online at:
https://github.com/idris-lang/Idris-dev.
distribution. The Idris 2 source can be found online at:
https://github.com/edwinb/Idris2.
- Existing projects on the ``Idris Hackers`` web space:
http://idris-hackers.github.io.

1
docs/tutorial/index.rst
View File

@ -36,6 +36,5 @@ changes since Idris 1, see :ref:`updates-index`.
views
theorems
interactive
syntax
miscellany
conclusions

41
docs/tutorial/interactive.rst
View File

@ -4,16 +4,14 @@
Interactive Editing
*******************
[NOT UPDATED FOR IDRIS 2 YET]
By now, we have seen several examples of how Idris’ dependent type
system can give extra confidence in a function’s correctness by giving
a more precise description of its intended behaviour in its *type*. We
have also seen an example of how the type system can help with EDSL
have also seen an example of how the type system can help with embedded DSL
development by allowing a programmer to describe the type system of an
object language. However, precise types give us more than verification
of programs — we can also exploit types to help write programs which
are *correct by construction*.
of programs — we can also use the type system to help write programs which
are *correct by construction*, interactively.
The Idris REPL provides several commands for inspecting and
modifying parts of programs, based on their types, such as case
@ -21,9 +19,9 @@ splitting on a pattern variable, inspecting the type of a
hole, and even a basic proof search mechanism. In this
section, we explain how these features can be exploited by a text
editor, and specifically how to do so in `Vim
<https://github.com/idris-hackers/idris-vim>`_. An interactive mode
<https://github.com/edwinb/idris2-vim>`_. An interactive mode
for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also
available.
available (though not yet updated for Idris 2).
Editing at the REPL
===================
@ -44,17 +42,15 @@ alternative form, which *updates* the source file in-place:
:command! [line number] [name]
When the REPL is loaded, it also starts a background process which
accepts and responds to REPL commands, using ``idris --client``. For
example, if we have a REPL running elsewhere, we can execute commands
such as:
It is also possible to invoke Idris in a mode which runs a REPL command,
displays the result, then exits, using ``idris2 --client``. For example:
::
$ idris --client ':t plus'
Prelude.Nat.plus : Nat -> Nat -> Nat
$ idris --client '2+2'
4 : Integer
$ idris2 --client ':t plus'
Prelude.plus : Nat -> Nat -> Nat
$ idris2 --client '2+2'
4
A text editor can take advantage of this, along with the editing
commands, in order to provide interactive editing support.
@ -178,7 +174,7 @@ surprisingly, there is only one possibility if we try to solve ``:ps
.. code-block:: idris
f x y :: (vzipWith f xs ys)
f x y :: vzipWith f xs ys
This works because ``vzipWith`` has a precise enough type: The
resulting vector has to be non-empty (a ``::``); the first element
@ -227,7 +223,7 @@ interactive editing support using the commands described above.
Interactive editing is achieved using the following editor commands,
each of which update the buffer directly:
- ``\d`` adds a template definition for the name declared on the
- ``\a`` adds a template definition for the name declared on the
current line (using ``:addclause``).
- ``\c`` case splits the variable at the cursor (using
@ -238,12 +234,9 @@ each of which update the buffer directly:
- ``\w`` adds a ``with`` clause (using ``:makewith``).
- ``\o`` invokes a proof search to solve the hole under the
- ``\s`` invokes a proof search to solve the hole under the
cursor (using ``:proofsearch``).
- ``\p`` invokes a proof search with additional hints to solve the
hole under the cursor (using ``:proofsearch``).
There are also commands to invoke the type checker and evaluator:
- ``\t`` displays the type of the (globally visible) name under the
@ -256,4 +249,8 @@ There are also commands to invoke the type checker and evaluator:
Corresponding commands are also available in the Emacs mode. Support
for other editors can be added in a relatively straightforward manner
by using ``idris –client``.
by using ``idris2 -–client``.
More sophisticated support can be added by using the IDE protocol (yet to
be documented for Idris 2, but which mostly extends to protocol documented for
`Idris 1 <http://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.

446
docs/tutorial/miscellany.rst
View File

@ -4,30 +4,24 @@
Miscellany
**********
[NOT UPDATED FOR IDRIS 2 YET, SOME NOT YET IMPLEMENTED]
In this section we discuss a variety of additional features:
+ auto, implicit, and default arguments;
+ literate programming;
+ interfacing with external libraries through the foreign function;
+ interface;
+ type providers;
+ code generation; and
+ literate programming; and
+ the universe hierarchy.
Implicit arguments
=======================
==================
We have already seen implicit arguments, which allows arguments to be
omitted when they can be inferred by the type checker, e.g.
.. code-block:: idris
index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a
index : forall a, n . Fin n -> Vect n a -> a
Auto implicit arguments
------------------------
-----------------------
In other situations, it may be possible to infer arguments not by type
checking but by searching the context for an appropriate value, or
@ -55,7 +49,8 @@ this to happen silently. We define ``head`` as follows:
The ``auto`` annotation on the implicit argument means that Idris
will attempt to fill in the implicit argument by searching for a value
of the appropriate type. It will try the following, in order:
of the appropriate type. In fact, internally, this is exactly how interface
resolution works. It will try the following, in order:
- Local variables, i.e. names bound in pattern matches or ``let`` bindings,
with exactly the right type.
@ -95,39 +90,11 @@ and will return the 5th fibonacci number. Note that while this works, this is no
intended use of the ``default`` annotation. It is included here for illustrative purposes
only. Usually, ``default`` is used to provide things like a custom proof search script.
Implicit conversions
====================
Idris supports the creation of *implicit conversions*, which allow
automatic conversion of values from one type to another when required to
make a term type correct. This is intended to increase convenience and
reduce verbosity. A contrived but simple example is the following:
.. code-block:: idris
implicit intString : Int -> String
intString = show
test : Int -> String
test x = "Number " ++ x
In general, we cannot append an ``Int`` to a ``String``, but the
implicit conversion function ``intString`` can convert ``x`` to a
``String``, so the definition of ``test`` is type correct. An implicit
conversion is implemented just like any other function, but given the
``implicit`` modifier, and restricted to one explicit argument.
Only one implicit conversion will be applied at a time. That is,
implicit conversions cannot be chained. Implicit conversions of simple
types, as above, are however discouraged! More commonly, an implicit
conversion would be used to reduce verbosity in an embedded domain
specific language, or to hide details of a proof. Such examples are
beyond the scope of this tutorial.
Literate programming
====================
[NOT YET IN IDRIS 2]
Like Haskell, Idris supports *literate* programming. If a file has
an extension of ``.lidr`` then it is assumed to be a literate file. In
literate programs, everything is assumed to be a comment unless the line
@ -146,404 +113,11 @@ An additional restriction is that there must be a blank line between a
program line (beginning with ``>``) and a comment line (beginning with
any other character).
Foreign function calls
======================
For practical programming, it is often necessary to be able to use
external libraries, particularly for interfacing with the operating
system, file system, networking, *et cetera*. Idris provides a
lightweight foreign function interface for achieving this, as part of
the prelude. For this, we assume a certain amount of knowledge of C and
the ``gcc`` compiler. First, we define a datatype which describes the
external types we can handle:
.. code-block:: idris
data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit
Each of these corresponds directly to a C type. Respectively: ``int``,
``double``, ``char``, ``char*``, ``void*`` and ``void``. There is also a
translation to a concrete Idris type, described by the following
function:
.. code-block:: idris
interpFTy : FTy -> Type
interpFTy FInt = Int
interpFTy FFloat = Double
interpFTy FChar = Char
interpFTy FString = String
interpFTy FPtr = Ptr
interpFTy FUnit = ()
A foreign function is described by a list of input types and a return
type, which can then be converted to an Idris type:
.. code-block:: idris
ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
A foreign function is assumed to be impure, so ``ForeignTy`` builds an
``IO`` type, for example:
.. code-block:: idris
Idris> ForeignTy [FInt, FString] FString
Int -> String -> IO String : Type
Idris> ForeignTy [FInt, FString] FUnit
Int -> String -> IO () : Type
We build a call to a foreign function by giving the name of the
function, a list of argument types and the return type. The built in
construct ``mkForeign`` converts this description to a function callable
by Idris:
.. code-block:: idris
data Foreign : Type -> Type where
FFun : String -> (xs:List FTy) -> (t:FTy) ->
Foreign (ForeignTy xs t)
mkForeign : Foreign x -> x
Note that the compiler expects ``mkForeign`` to be fully applied to
build a complete foreign function call. For example, the ``putStr``
function is implemented as follows, as a call to an external function
``putStr`` defined in the run-time system:
.. code-block:: idris
putStr : String -> IO ()
putStr x = mkForeign (FFun "putStr" [FString] FUnit) x
Include and linker directives
-----------------------------
Foreign function calls are translated directly to calls to C functions,
with appropriate conversion between the Idris representation of a
value and the C representation. Often this will require extra libraries
to be linked in, or extra header and object files. This is made possible
through the following directives:
- ``%lib target x`` — include the ``libx`` library. If the target is
``C`` this is equivalent to passing the ``-lx`` option to ``gcc``. If
the target is Java the library will be interpreted as a
``groupId:artifactId:packaging:version`` dependency coordinate for
maven.
- ``%include target x`` — use the header file or import ``x`` for the
given back end target.
- ``%link target x.o`` — link with the object file ``x.o`` when using
the given back end target.
- ``%dynamic x.so`` — dynamically link the interpreter with the shared
object ``x.so``.
Testing foreign function calls
------------------------------
Normally, the Idris interpreter (used for typechecking and at the REPL)
will not perform IO actions. Additionally, as it neither generates C
code nor compiles to machine code, the ``%lib``, ``%include`` and
``%link`` directives have no effect. IO actions and FFI calls can be
tested using the special REPL command ``:x EXPR``, and C libraries can
be dynamically loaded in the interpreter by using the ``:dynamic``
command or the ``%dynamic`` directive. For example:
.. code-block:: idris
Idris> :dynamic libm.so
Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
0.9995736030415051 : Double
Type Providers
==============
Idris type providers, inspired by F#’s type providers, are a means of
making our types be “about” something in the world outside of Idris. For
example, given a type that represents a database schema and a query that
is checked against it, a type provider could read the schema of a real
database during type checking.
Idris type providers use the ordinary execution semantics of Idris to
run an IO action and extract the result. This result is then saved as a
constant in the compiled code. It can be a type, in which case it is
used like any other type, or it can be a value, in which case it can be
used as any other value, including as an index in types.
Type providers are still an experimental extension. To enable the
extension, use the ``%language`` directive:
.. code-block:: idris
%language TypeProviders
A provider ``p`` for some type ``t`` is simply an expression of type
``IO (Provider t)``. The ``%provide`` directive causes the type checker
to execute the action and bind the result to a name. This is perhaps
best illustrated with a simple example. The type provider ``fromFile``
reads a text file. If the file consists of the string ``Int``, then the
type ``Int`` will be provided. Otherwise, it will provide the type
``Nat``.
.. code-block:: idris
strToType : String -> Type
strToType "Int" = Int
strToType _ = Nat
fromFile : String -> IO (Provider Type)
fromFile fname = do Right str <- readFile fname
| Left err => pure (Provide Void)
pure (Provide (strToType (trim str)))
We then use the ``%provide`` directive:
.. code-block:: idris
%provide (T1 : Type) with fromFile "theType"
foo : T1
foo = 2
If the file named ``theType`` consists of the word ``Int``, then ``foo``
will be an ``Int``. Otherwise, it will be a ``Nat``. When Idris
encounters the directive, it first checks that the provider expression
``fromFile theType`` has type ``IO (Provider Type)``. Next, it executes
the provider. If the result is ``Provide t``, then ``T1`` is defined as
``t``. Otherwise, the result is an error.
Our datatype ``Provider t`` has the following definition:
.. code-block:: idris
data Provider a = Error String
| Provide a
We have already seen the ``Provide`` constructor. The ``Error``
constructor allows type providers to return useful error messages. The
example in this section was purposefully simple. More complex type
provider implementations, including a statically-checked SQLite binding,
are available in an external collection [1]_.
C Target
========
The default target of Idris is C. Compiling via:
::
$ idris hello.idr -o hello
is equivalent to:
::
$ idris --codegen C hello.idr -o hello
When the command above is used, a temporary C source is generated, which
is then compiled into an executable named ``hello``.
In order to view the generated C code, compile via:
::
$ idris hello.idr -S -o hello.c
To turn optimisations on, use the ``%flag C`` pragma within the code, as
is shown below:
.. code-block:: idris
module Main
%flag C "-O3"
factorial : Int -> Int
factorial 0 = 1
factorial n = n * (factorial (n-1))
main : IO ()
main = do
putStrLn $ show $ factorial 3
To compile the generated C with debugging information e.g. to use
``gdb`` to debug segmentation faults in Idris programs, use the
``%flag C`` pragma to include debugging symbols, as is shown below:
.. code-block:: idris
%flag C "-g"
JavaScript Target
=================
Idris is capable of producing *JavaScript* code that can be run in a
browser as well as in the *NodeJS* environment or alike. One can use the
FFI to communicate with the *JavaScript* ecosystem.
Code Generation
---------------
Code generation is split into two separate targets. To generate code
that is tailored for running in the browser issue the following command:
::
$ idris --codegen javascript hello.idr -o hello.js
The resulting file can be embedded into your HTML just like any other
*JavaScript* code.
Generating code for *NodeJS* is slightly different. Idris outputs a
*JavaScript* file that can be directly executed via ``node``.
::
$ idris --codegen node hello.idr -o hello
$ ./hello
Hello world
Take into consideration that the *JavaScript* code generator is using
``console.log`` to write text to ``stdout``, this means that it will
automatically add a newline to the end of each string. This behaviour
does not show up in the *NodeJS* code generator.
Using the FFI
-------------
To write a useful application we need to communicate with the outside
world. Maybe we want to manipulate the DOM or send an Ajax request. For
this task we can use the FFI. Since most *JavaScript* APIs demand
callbacks we need to extend the FFI so we can pass functions as
arguments.
The *JavaScript* FFI works a little bit differently than the regular
FFI. It uses positional arguments to directly insert our arguments into
a piece of *JavaScript* code.
One could use the primitive addition of *JavaScript* like so:
.. code-block:: idris
module Main
primPlus : Int -> Int -> IO Int
primPlus a b = mkForeign (FFun "%0 + %1" [FInt, FInt] FInt) a b
main : IO ()
main = do
a <- primPlus 1 1
b <- primPlus 1 2
print (a, b)
Notice that the ``%n`` notation qualifies the position of the ``n``-th
argument given to our foreign function starting from 0. When you need a
percent sign rather than a position simply use ``%%`` instead.
Passing functions to a foreign function is very similar. Let’s assume
that we want to call the following function from the *JavaScript* world:
.. code-block:: idris
function twice(f, x) {
return f(f(x));
}
We obviously need to pass a function ``f`` here (we can infer it from
the way we use ``f`` in ``twice``, it would be more obvious if
*JavaScript* had types).
The *JavaScript* FFI is able to understand functions as arguments when
you give it something of type ``FFunction``. The following example code
calls ``twice`` in *JavaScript* and returns the result to our Idris
program:
.. code-block:: idris
module Main
twice : (Int -> Int) -> Int -> IO Int
twice f x = mkForeign (
FFun "twice(%0,%1)" [FFunction FInt FInt, FInt] FInt
) f x
main : IO ()
main = do
a <- twice (+1) 1
print a
The program outputs ``3``, just like we expected.
Including external *JavaScript* files
-------------------------------------
Whenever one is working with *JavaScript* one might want to include
external libraries or just some functions that she or he wants to call
via FFI which are stored in external files. The *JavaScript* and
*NodeJS* code generators understand the ``%include`` directive. Keep in
mind that *JavaScript* and *NodeJS* are handled as different code
generators, therefore you will have to state which one you want to
target. This means that you can include different files for *JavaScript*
and *NodeJS* in the same Idris source file.
So whenever you want to add an external *JavaScript* file you can do
this like so:
For *NodeJS*:
.. code-block:: idris
%include Node "path/to/external.js"
And for use in the browser:
.. code-block:: idris
%include JavaScript "path/to/external.js"
The given files will be added to the top of the generated code.
For library packages you can also use the ipkg objs option to include the
js file in the installation, and use:
.. code-block:: idris
%include Node "package/external.js"
The *JavaScript* and *NodeJS* backends of Idris will also lookup for the file
on that location.
Including *NodeJS* modules
--------------------------
The *NodeJS* code generator can also include modules with the ``%lib``
directive.
.. code-block:: idris
%lib Node "fs"
This directive compiles into the following *JavaScript*
.. code-block:: javascript
var fs = require("fs");
Shrinking down generated *JavaScript*
-------------------------------------
Idris can produce very big chunks of *JavaScript* code. However, the
generated code can be minified using the ``closure-compiler`` from
Google. Any other minifier is also suitable but ``closure-compiler``
offers advanced compilation that does some aggressive inlining and code
elimination. Idris can take full advantage of this compilation mode
and it’s highly recommended to use it when shipping a *JavaScript*
application written in Idris.
Cumulativity
============
[NOT YET IN IDRIS 2]
Since values can appear in types and *vice versa*, it is natural that
types themselves have types. For example:

213
docs/tutorial/syntax.rst
View File

@ -1,213 +0,0 @@
.. _sect-syntax:
*****************
Syntax Extensions
*****************
[NOT UPDATED FOR IDRIS 2 YET, AND POSSIBLY TO BE DELETED]
Idris supports the implementation of *Embedded Domain Specific
Languages* (EDSLs) in several ways [1]_. One way, as we have already
seen, is through extending ``do`` notation. Another important way is
to allow extension of the core syntax. In this section we describe two
ways of extending the syntax: ``syntax`` rules and ``dsl`` notation.
``syntax`` rules
================
We have seen ``if...then...else`` expressions, but these are not built
in. Instead, we can define a function in the prelude as follows (we
have already seen this function in Section :ref:`sect-lazy`):
.. code-block:: idris
ifThenElse : (x:Bool) -> Lazy a -> Lazy a -> a;
ifThenElse True t e = t;
ifThenElse False t e = e;
and then extend the core syntax with a ``syntax`` declaration:
.. code-block:: idris
syntax if [test] then [t] else [e] = ifThenElse test t e;
The left hand side of a ``syntax`` declaration describes the syntax
rule, and the right hand side describes its expansion. The syntax rule
itself consists of:
- **Keywords** — here, ``if``, ``then`` and ``else``, which must be
valid identifiers.
- **Non-terminals** — included in square brackets, ``[test]``, ``[t]``
and ``[e]`` here, which stand for arbitrary expressions. To avoid
parsing ambiguities, these expressions cannot use syntax extensions
at the top level (though they can be used in parentheses).
- **Names** — included in braces, which stand for names which may be
bound on the right hand side.
- **Symbols** — included in quotations marks, e.g. ``":="``. This can
also be used to include reserved words in syntax rules, such as
``"let"`` or ``"in"``.
The limitations on the form of a syntax rule are that it must include
at least one symbol or keyword, and there must be no repeated
variables standing for non-terminals. Any expression can be used, but
if there are two non-terminals in a row in a rule, only simple
expressions may be used (that is, variables, constants, or bracketed
expressions). Rules can use previously defined rules, but may not be
recursive. The following syntax extensions would therefore be valid:
.. code-block:: idris
syntax [var] ":=" [val] = Assign var val;
syntax [test] "?" [t] ":" [e] = if test then t else e;
syntax select [x] from [t] "where" [w] = SelectWhere x t w;
syntax select [x] from [t] = Select x t;
Syntax macros can be further restricted to apply only in patterns (i.e.
only on the left hand side of a pattern match clause) or only in terms
(i.e. everywhere but the left hand side of a pattern match clause) by
being marked as ``pattern`` or ``term`` syntax rules. For example, we
might define an interval as follows, with a static check that the lower
bound is below the upper bound using ``so``:
.. code-block:: idris
data Interval : Type where
MkInterval : (lower : Double) -> (upper : Double) ->
So (lower < upper) -> Interval
We can define a syntax which, in patterns, always matches ``Oh`` for
the proof argument, and in terms requires a proof term to be provided:
.. code-block:: idris
pattern syntax "[" [x] "..." [y] "]" = MkInterval x y Oh
term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
In terms, the syntax ``[x...y]`` will generate a proof obligation
``bounds_lemma`` (possibly renamed).
Finally, syntax rules may be used to introduce alternative binding
forms. For example, a ``for`` loop binds a variable on each iteration:
.. code-block:: idris
syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
main : IO ()
main = do for x in [1..10]:
putStrLn ("Number " ++ show x)
putStrLn "Done!"
Note that we have used the ``{x}`` form to state that ``x`` represents
a bound variable, substituted on the right hand side. We have also put
``in`` in quotation marks since it is already a reserved word.
``dsl`` notation
================
The well-typed interpreter in Section :ref:`sect-interp` is a simple
example of a common programming pattern with dependent types. Namely:
describe an *object language* and its type system with dependent types
to guarantee that only well-typed programs can be represented, then
program using that representation. Using this approach we can, for
example, write programs for serialising binary data [2]_ or running
concurrent processes safely [3]_.
Unfortunately, the form of object language programs makes it rather
hard to program this way in practice. Recall the factorial program in
``Expr`` for example:
.. code-block:: idris
fact : Expr G (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var Stop) (Val 0))
(Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
(Var Stop)))
Since this is a particularly useful pattern, Idris provides syntax
overloading [1]_ to make it easier to program in such object
languages:
.. code-block:: idris
mkLam : TTName -> Expr (t::g) t' -> Expr g (TyFun t t')
mkLam _ body = Lam body
dsl expr
variable = Var
index_first = Stop
index_next = Pop
lambda = mkLam
A ``dsl`` block describes how each syntactic construct is represented
in an object language. Here, in the ``expr`` language, any variable is
translated to the ``Var`` constructor, using ``Pop`` and ``Stop`` to
construct the de Bruijn index (i.e., to count how many bindings since
the variable itself was bound); and any lambda is translated to a
``Lam`` constructor. The ``mkLam`` function simply ignores its first
argument, which is the name that the user chose for the variable. It
is also possible to overload ``let`` and dependent function syntax
(``pi``) in this way. We can now write ``fact`` as follows:
.. code-block:: idris
fact : Expr G (TyFun TyInt TyInt)
fact = expr (\x => If (Op (==) x (Val 0))
(Val 1) (Op (*) (app fact (Op (-) x (Val 1))) x))
In this new version, ``expr`` declares that the next expression will
be overloaded. We can take this further, using idiom brackets, by
declaring:
.. code-block:: idris
(<*>) : (f : Lazy (Expr G (TyFun a t))) -> Expr G a -> Expr G t
(<*>) f a = App f a
pure : Expr G a -> Expr G a
pure = id
Note that there is no need for these to be part of an implementation of
``Applicative``, since idiom bracket notation translates directly to
the names ``<*>`` and ``pure``, and ad-hoc type-directed overloading
is allowed. We can now say:
.. code-block:: idris
fact : Expr G (TyFun TyInt TyInt)
fact = expr (\x => If (Op (==) x (Val 0))
(Val 1) (Op (*) [| fact (Op (-) x (Val 1)) |] x))
With some more ad-hoc overloading and use of interfaces, and a new
syntax rule, we can even go as far as:
.. code-block:: idris
syntax "IF" [x] "THEN" [t] "ELSE" [e] = If x t e
fact : Expr G (TyFun TyInt TyInt)
fact = expr (\x => IF x == 0 THEN 1 ELSE [| fact (x - 1) |] * x)
.. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems
programming with embedded domain specific languages. In
Proceedings of the 14th international conference on Practical
Aspects of Declarative Languages (PADL'12), Claudio Russo and
Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
242-257. DOI=10.1007/978-3-642-27694-1_18
http://dx.doi.org/10.1007/978-3-642-27694-1_18
.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
dependent types. In Proceedings of the 5th ACM workshop on
Programming languages meets program verification (PLPV
'11). ACM, New York, NY, USA,
43-54. DOI=10.1145/1929529.1929536
http://doi.acm.org/10.1145/1929529.1929536
.. [3] Edwin Brady and Kevin Hammond. 2010. Correct-by-Construction
Concurrency: Using Dependent Types to Verify Implementations of
Effectful Resource Usage Protocols. Fundam. Inf. 102, 2 (April
2010), 145-176. http://dl.acm.org/citation.cfm?id=1883636