mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Removed docs directory for adding new docs.
This commit is contained in:
parent
db25e81d48
commit
5175743e78
2
.gitignore
vendored
2
.gitignore
vendored
@ -10,7 +10,7 @@
|
||||
|
||||
/dist/idris2.c
|
||||
|
||||
/docs/_build/
|
||||
/docs/build/
|
||||
|
||||
/libs/**/build
|
||||
/tests/**/output
|
||||
|
10
docs/LICENSE
10
docs/LICENSE
@ -1,10 +0,0 @@
|
||||
#+TITLE: Licensing Information
|
||||
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, /The
|
||||
Idris Community/ has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at:
|
||||
|
||||
https://creativecommons.org/publicdomain/zero/1.0/
|
183
docs/Makefile
183
docs/Makefile
@ -1,183 +0,0 @@
|
||||
# Makefile for Sphinx documentation
|
||||
#
|
||||
|
||||
# You can set these variables from the command line.
|
||||
SPHINXOPTS =
|
||||
SPHINXBUILD = sphinx-build
|
||||
PAPER =
|
||||
BUILDDIR = _build
|
||||
|
||||
# User-friendly check for sphinx-build
|
||||
ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)
|
||||
$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from https://www.sphinx-doc.org/)
|
||||
endif
|
||||
|
||||
# Internal variables.
|
||||
PAPEROPT_a4 = -D latex_paper_size=a4
|
||||
PAPEROPT_letter = -D latex_paper_size=letter
|
||||
ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
|
||||
# the i18n builder cannot share the environment and doctrees with the others
|
||||
I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
|
||||
|
||||
.PHONY: help clean html dirhtml singlehtml pickle json htmlhelp qthelp devhelp epub latex latexpdf text man changes linkcheck doctest coverage gettext
|
||||
|
||||
help:
|
||||
@echo "Please use \`make <target>' where <target> is one of"
|
||||
@echo " html to make standalone HTML files"
|
||||
@echo " dirhtml to make HTML files named index.html in directories"
|
||||
@echo " singlehtml to make a single large HTML file"
|
||||
@echo " pickle to make pickle files"
|
||||
@echo " json to make JSON files"
|
||||
@echo " htmlhelp to make HTML files and a HTML help project"
|
||||
@echo " qthelp to make HTML files and a qthelp project"
|
||||
@echo " devhelp to make HTML files and a Devhelp project"
|
||||
@echo " epub to make an epub"
|
||||
@echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
|
||||
@echo " latexpdf to make LaTeX files and run them through pdflatex"
|
||||
@echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx"
|
||||
@echo " text to make text files"
|
||||
@echo " man to make manual pages"
|
||||
@echo " texinfo to make Texinfo files"
|
||||
@echo " info to make Texinfo files and run them through makeinfo"
|
||||
@echo " gettext to make PO message catalogs"
|
||||
@echo " changes to make an overview of all changed/added/deprecated items"
|
||||
@echo " xml to make Docutils-native XML files"
|
||||
@echo " pseudoxml to make pseudoxml-XML files for display purposes"
|
||||
@echo " linkcheck to check all external links for integrity"
|
||||
@echo " doctest to run all doctests embedded in the documentation (if enabled)"
|
||||
@echo " coverage to run coverage check of the documentation (if enabled)"
|
||||
|
||||
clean:
|
||||
rm -rf $(BUILDDIR)/*
|
||||
|
||||
html:
|
||||
$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
|
||||
@echo
|
||||
@echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
|
||||
|
||||
dirhtml:
|
||||
$(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml
|
||||
@echo
|
||||
@echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
|
||||
|
||||
singlehtml:
|
||||
$(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml
|
||||
@echo
|
||||
@echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
|
||||
|
||||
pickle:
|
||||
$(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle
|
||||
@echo
|
||||
@echo "Build finished; now you can process the pickle files."
|
||||
|
||||
json:
|
||||
$(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json
|
||||
@echo
|
||||
@echo "Build finished; now you can process the JSON files."
|
||||
|
||||
htmlhelp:
|
||||
$(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp
|
||||
@echo
|
||||
@echo "Build finished; now you can run HTML Help Workshop with the" \
|
||||
".hhp project file in $(BUILDDIR)/htmlhelp."
|
||||
|
||||
qthelp:
|
||||
$(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp
|
||||
@echo
|
||||
@echo "Build finished; now you can run "qcollectiongenerator" with the" \
|
||||
".qhcp project file in $(BUILDDIR)/qthelp, like this:"
|
||||
@echo "# qcollectiongenerator $(BUILDDIR)/qthelp/IdrisManual.qhcp"
|
||||
@echo "To view the help file:"
|
||||
@echo "# assistant -collectionFile $(BUILDDIR)/qthelp/IdrisManual.qhc"
|
||||
|
||||
devhelp:
|
||||
$(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp
|
||||
@echo
|
||||
@echo "Build finished."
|
||||
@echo "To view the help file:"
|
||||
@echo "# mkdir -p $$HOME/.local/share/devhelp/IdrisManual"
|
||||
@echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/IdrisManual"
|
||||
@echo "# devhelp"
|
||||
|
||||
epub:
|
||||
$(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub
|
||||
@echo
|
||||
@echo "Build finished. The epub file is in $(BUILDDIR)/epub."
|
||||
|
||||
latex:
|
||||
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
|
||||
@echo
|
||||
@echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex."
|
||||
@echo "Run \`make' in that directory to run these through (pdf)latex" \
|
||||
"(use \`make latexpdf' here to do that automatically)."
|
||||
|
||||
latexpdf:
|
||||
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
|
||||
@echo "Running LaTeX files through pdflatex..."
|
||||
$(MAKE) -C $(BUILDDIR)/latex all-pdf
|
||||
@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
|
||||
|
||||
latexpdfja:
|
||||
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
|
||||
@echo "Running LaTeX files through platex and dvipdfmx..."
|
||||
$(MAKE) -C $(BUILDDIR)/latex all-pdf-ja
|
||||
@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
|
||||
|
||||
text:
|
||||
$(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text
|
||||
@echo
|
||||
@echo "Build finished. The text files are in $(BUILDDIR)/text."
|
||||
|
||||
man:
|
||||
$(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man
|
||||
@echo
|
||||
@echo "Build finished. The manual pages are in $(BUILDDIR)/man."
|
||||
|
||||
texinfo:
|
||||
$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
|
||||
@echo
|
||||
@echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo."
|
||||
@echo "Run \`make' in that directory to run these through makeinfo" \
|
||||
"(use \`make info' here to do that automatically)."
|
||||
|
||||
info:
|
||||
$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
|
||||
@echo "Running Texinfo files through makeinfo..."
|
||||
make -C $(BUILDDIR)/texinfo info
|
||||
@echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo."
|
||||
|
||||
gettext:
|
||||
$(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale
|
||||
@echo
|
||||
@echo "Build finished. The message catalogs are in $(BUILDDIR)/locale."
|
||||
|
||||
changes:
|
||||
$(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes
|
||||
@echo
|
||||
@echo "The overview file is in $(BUILDDIR)/changes."
|
||||
|
||||
linkcheck:
|
||||
$(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck
|
||||
@echo
|
||||
@echo "Link check complete; look for any errors in the above output " \
|
||||
"or in $(BUILDDIR)/linkcheck/output.txt."
|
||||
|
||||
doctest:
|
||||
$(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest
|
||||
@echo "Testing of doctests in the sources finished, look at the " \
|
||||
"results in $(BUILDDIR)/doctest/output.txt."
|
||||
|
||||
coverage:
|
||||
$(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage
|
||||
@echo "Testing of coverage in the sources finished, look at the " \
|
||||
"results in $(BUILDDIR)/coverage/python.txt."
|
||||
|
||||
xml:
|
||||
$(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml
|
||||
@echo
|
||||
@echo "Build finished. The XML files are in $(BUILDDIR)/xml."
|
||||
|
||||
pseudoxml:
|
||||
$(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml
|
||||
@echo
|
||||
@echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml."
|
@ -1,56 +0,0 @@
|
||||
# Documentation for the Idris Language.
|
||||
|
||||
|
||||
This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](https://www.sphinx-doc.org) for future inclusion on [Read The Docs](https://readthedocs.org).
|
||||
|
||||
## Dependencies
|
||||
|
||||
To build the manual the following dependencies must be met. We assume that you have standard build automation tools already install i.e. `make`.
|
||||
|
||||
### Sphinx-Doc
|
||||
|
||||
Python should be installed by default on most systems.
|
||||
Sphinx can be installed either through your hosts package manager or using pip/easy_install.
|
||||
Recommended way is to use virtual environment for building documentation.
|
||||
|
||||
*Note* [ReadTheDocs](https://readthedocs.org) works with Sphinx
|
||||
`v1.2.2`. If you install a more recent version of sphinx then
|
||||
'incorrectly' marked up documentation may get passed the build system
|
||||
of readthedocs and be ignored. In the past we had several code-blocks
|
||||
disappear because of that.
|
||||
|
||||
The ReadTheDocs theme can be installed in virtual environment using pip as follows:
|
||||
|
||||
```sh
|
||||
python3 -m venv idris2docs_venv
|
||||
source idris2docs_venv/bin/activate
|
||||
pip install --upgrade pip
|
||||
pip install sphinx_rtd_theme
|
||||
```
|
||||
|
||||
### LaTeX
|
||||
|
||||
LaTeX can be install either using your systems package manager or direct from TeXLive.
|
||||
|
||||
|
||||
## Build Instructions
|
||||
|
||||
```sh
|
||||
cd docs
|
||||
make html
|
||||
make latexpdf
|
||||
```
|
||||
|
||||
## Contributing
|
||||
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, /The
|
||||
Idris Community/ has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at:
|
||||
|
||||
https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
|
||||
When contributing material to the manual please bear in mind that the work will be licensed as above.
|
@ -1,49 +0,0 @@
|
||||
.. _app-index:
|
||||
|
||||
################################
|
||||
Structuring Idris 2 Applications
|
||||
################################
|
||||
|
||||
A tutorial on structuring Idris 2 applications using ``Control.App``.
|
||||
|
||||
.. note::
|
||||
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
Idris applications have ``main : IO ()`` as an entry point. A type ``IO a`` is
|
||||
a description of interactive actions which produce a value of type ``a``. This
|
||||
is fine for primitives, but ``IO`` does not support exceptions so we have to be
|
||||
explicit about how an operation handles failure. Also, if we do
|
||||
want to support exceptions, we also want to explain how exceptions and linearity
|
||||
(see Section :ref:`sect-multiplicities`) interact.
|
||||
|
||||
In this tutorial, we describe a parameterised type ``App`` and a related
|
||||
parameterised type ``App1``, which together allow us to structure larger
|
||||
applications, taking into account both exceptions and linearity. The aims of
|
||||
``App`` and ``App1`` are that they should:
|
||||
|
||||
* make it possible to express what interactions a function does, in its type,
|
||||
without too much notational overhead.
|
||||
* have little or no performance overhead compared to writing in *IO*.
|
||||
* be compatible with other libraries and techniques for describing effects,
|
||||
such as algebraic effects or monad transformers.
|
||||
* be sufficiently easy to use and performant that it can be the basis of
|
||||
*all* libraries that make foreign function calls, much as *IO*
|
||||
is in Idris 1 and Haskell
|
||||
* be compatible with linear types, meaning that they should express whether a
|
||||
section of code is linear (guaranteed to execute exactly once without
|
||||
throwing an exception) or whether it might throw an exception.
|
||||
|
||||
We begin by introducing ``App``, with some small example
|
||||
programs, then show how to extend it with exceptions, state, and other
|
||||
interfaces.
|
||||
|
||||
[To be continued...]
|
@ -1,47 +0,0 @@
|
||||
**************************
|
||||
Chez Scheme Code Generator
|
||||
**************************
|
||||
|
||||
The Chez Scheme code generator is the default, or it can be accessed via a REPL
|
||||
command:
|
||||
|
||||
::
|
||||
|
||||
Main> :set cg chez
|
||||
|
||||
By default, therefore, to run Idris programs you will need to install
|
||||
`Chez Scheme <https://www.scheme.com/>`_. Chez Scheme is open source, and
|
||||
available via most OS package managers.
|
||||
|
||||
You can compile an expression ``expr`` of type ``IO ()`` to an executable as
|
||||
follows, at the REPL:
|
||||
|
||||
::
|
||||
|
||||
Main> :c execname expr
|
||||
|
||||
...where ``execname`` is the name of the executable file. This will generate
|
||||
the following:
|
||||
|
||||
* A shell script ``build/exec/execname`` which invokes the program
|
||||
* A subdirectory ``build/exec/execname_app`` which contains all the data necessary
|
||||
to run the program. This includes the Chez Scheme source (``execname.ss``),
|
||||
the compiled Chez Scheme code (``execname.so``) and any shared libraries needed
|
||||
for foreign function definitions.
|
||||
|
||||
The executable ``execname`` is relocatable to any subdirectory, provided that
|
||||
``execname_app`` is also in the same subdirectory.
|
||||
|
||||
You can also execute an expression directly:
|
||||
|
||||
::
|
||||
|
||||
Main> :exec expr
|
||||
|
||||
Again, ``expr`` must have type ``IO ()``. This will generate a temporary
|
||||
executable script ``_tmpchez`` in the ``build/exec`` directory, and execute
|
||||
that.
|
||||
|
||||
Chez Scheme is the default code generator, so if you invoke ``idris2`` with the
|
||||
``-o execname`` flag, it will generate an executable script
|
||||
``build/exec/execname``, again with support files in ``build/exec/execname_app``.
|
@ -1,49 +0,0 @@
|
||||
.. _sect-execs:
|
||||
|
||||
************************
|
||||
Compiling to Executables
|
||||
************************
|
||||
|
||||
.. note::
|
||||
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
Idris 2 (the language) is designed to be independent of any specific code
|
||||
generator. Still, since the point of writing a program is to be able to run it,
|
||||
it's important to know how to do so! By default, Idris compiles to executables
|
||||
via `Chez Scheme <https://www.scheme.com/>`_.
|
||||
|
||||
You can compile to an executable as follows, at the REPL:
|
||||
|
||||
::
|
||||
|
||||
Main> :c execname expr
|
||||
|
||||
...where ``execname`` is the name of the executable file to generate, and
|
||||
``expr`` is the Idris expression which will be executed. ``expr`` must have
|
||||
type ``IO ()``. This will result in an executable file ``execname``, in a
|
||||
directory ``build/exec``, relative to the current working directory.
|
||||
|
||||
You can also execute expressions directly:
|
||||
|
||||
::
|
||||
|
||||
Main> :exec expr
|
||||
|
||||
Again, ``expr`` must have type ``IO ()``.
|
||||
|
||||
There are two code generators provided in Idris 2, and (later) there will be
|
||||
a system for plugging in new code generators for a variety of targets. The
|
||||
default is to compile via Chez Scheme, with an alternative via Racket.
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
chez
|
||||
racket
|
||||
|
@ -1,11 +0,0 @@
|
||||
*********************
|
||||
Racket Code Generator
|
||||
*********************
|
||||
|
||||
The Racket code generator is accessed via a REPL command:
|
||||
|
||||
::
|
||||
|
||||
Main> :set cg racket
|
||||
|
||||
[More details TODO]
|
430
docs/conf.py
430
docs/conf.py
@ -1,430 +0,0 @@
|
||||
# -*- coding: utf-8 -*-
|
||||
#
|
||||
# Idris Manual documentation build configuration file, created by
|
||||
# sphinx-quickstart on Sat Feb 28 20:41:47 2015.
|
||||
#
|
||||
# This file is execfile()d with the current directory set to its
|
||||
# containing dir.
|
||||
#
|
||||
# Note that not all possible configuration values are present in this
|
||||
# autogenerated file.
|
||||
#
|
||||
# All configuration values have a default; values that are commented out
|
||||
# serve to show the default.
|
||||
|
||||
import sys
|
||||
import os
|
||||
|
||||
# True if the readthedocs theme is locally installed
|
||||
on_rtd = os.environ.get('READTHEDOCS', None) == 'True'
|
||||
|
||||
# If extensions (or modules to document with autodoc) are in another directory,
|
||||
# add these directories to sys.path here. If the directory is relative to the
|
||||
# documentation root, use os.path.abspath to make it absolute, like shown here.
|
||||
#sys.path.insert(0, os.path.abspath('.'))
|
||||
|
||||
# -- General configuration ------------------------------------------------
|
||||
|
||||
# If your documentation needs a minimal Sphinx version, state it here.
|
||||
#needs_sphinx = '1.0'
|
||||
|
||||
# Add any Sphinx extension module names here, as strings. They can be
|
||||
# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
|
||||
# ones.
|
||||
extensions = [
|
||||
'sphinx.ext.todo',
|
||||
# 'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.
|
||||
'sphinx.ext.ifconfig',
|
||||
]
|
||||
|
||||
# Add any paths that contain templates here, relative to this directory.
|
||||
templates_path = ['_templates']
|
||||
|
||||
# The suffix of source filenames.
|
||||
source_suffix = ['.rst','.md']
|
||||
|
||||
# The encoding of source files.
|
||||
#source_encoding = 'utf-8-sig'
|
||||
|
||||
# The master toctree document.
|
||||
master_doc = 'index'
|
||||
|
||||
# General information about the project.
|
||||
project = u'Idris2'
|
||||
copyright = u'2019, The Idris Community'
|
||||
author = u'The Idris Community'
|
||||
|
||||
# The version info for the project you're documenting, acts as replacement for
|
||||
# |version| and |release|, also used in various other places throughout the
|
||||
# built documents.
|
||||
#
|
||||
# The short X.Y version.
|
||||
version = '0.0'
|
||||
# The full version, including alpha/beta/rc tags.
|
||||
release = '0.0'
|
||||
|
||||
# The language for content autogenerated by Sphinx. Refer to documentation
|
||||
# for a list of supported languages.
|
||||
#
|
||||
# This is also used if you do content translation via gettext catalogs.
|
||||
# Usually you set "language" from the command line for these cases.
|
||||
language = None
|
||||
|
||||
# There are two options for replacing |today|: either, you set today to some
|
||||
# non-false value, then it is used:
|
||||
#today = ''
|
||||
# Else, today_fmt is used as the format for a strftime call.
|
||||
#today_fmt = '%B %d, %Y'
|
||||
|
||||
# List of patterns, relative to source directory, that match files and
|
||||
# directories to ignore when looking for source files.
|
||||
exclude_patterns = ['_build', 'README.md']
|
||||
|
||||
# The reST default role (used for this markup: `text`) to use for all
|
||||
# documents.
|
||||
#default_role = None
|
||||
|
||||
# If true, '()' will be appended to :func: etc. cross-reference text.
|
||||
#add_function_parentheses = True
|
||||
|
||||
# If true, the current module name will be prepended to all description
|
||||
# unit titles (such as .. function::).
|
||||
#add_module_names = True
|
||||
|
||||
# If true, sectionauthor and moduleauthor directives will be shown in the
|
||||
# output. They are ignored by default.
|
||||
#show_authors = False
|
||||
|
||||
# The name of the Pygments (syntax highlighting) style to use.
|
||||
pygments_style = 'sphinx'
|
||||
|
||||
# A list of ignored prefixes for module index sorting.
|
||||
#modindex_common_prefix = []
|
||||
|
||||
# If true, keep warnings as "system message" paragraphs in the built documents.
|
||||
#keep_warnings = False
|
||||
|
||||
# If true, `todo` and `todoList` produce output, else they produce nothing.
|
||||
todo_include_todos = True
|
||||
|
||||
|
||||
# -- Options for HTML output ----------------------------------------------
|
||||
|
||||
# The theme to use for HTML and HTML Help pages. See the documentation for
|
||||
# a list of builtin themes.
|
||||
html_theme = "default"
|
||||
|
||||
if not on_rtd: # only import and set the theme if we're building docs locally
|
||||
try:
|
||||
import sphinx_rtd_theme
|
||||
html_theme = 'sphinx_rtd_theme'
|
||||
html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]
|
||||
except ImportError:
|
||||
html_theme = "default"
|
||||
|
||||
# Theme options are theme-specific and customize the look and feel of a theme
|
||||
# further. For a list of options available for each theme, see the
|
||||
# documentation.
|
||||
#html_theme_options = {}
|
||||
|
||||
# Add any paths that contain custom themes here, relative to this directory.
|
||||
#html_theme_path = []
|
||||
|
||||
# The name for this set of Sphinx documents. If None, it defaults to
|
||||
# "<project> v<release> documentation".
|
||||
#html_title = None
|
||||
|
||||
# A shorter title for the navigation bar. Default is the same as html_title.
|
||||
#html_short_title = None
|
||||
|
||||
# The name of an image file (relative to this directory) to place at the top
|
||||
# of the sidebar.
|
||||
#html_logo = None
|
||||
|
||||
# The name of an image file (within the static path) to use as favicon of the
|
||||
# docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32
|
||||
# pixels large.
|
||||
#html_favicon = None
|
||||
|
||||
# Add any paths that contain custom static files (such as style sheets) here,
|
||||
# relative to this directory. They are copied after the builtin static files,
|
||||
# so a file named "default.css" will overwrite the builtin "default.css".
|
||||
html_static_path = ['_static']
|
||||
|
||||
# Add any extra paths that contain custom files (such as robots.txt or
|
||||
# .htaccess) here, relative to this directory. These files are copied
|
||||
# directly to the root of the documentation.
|
||||
#html_extra_path = []
|
||||
|
||||
# If not '', a 'Last updated on:' timestamp is inserted at every page bottom,
|
||||
# using the given strftime format.
|
||||
#html_last_updated_fmt = '%b %d, %Y'
|
||||
|
||||
# If true, SmartyPants will be used to convert quotes and dashes to
|
||||
# typographically correct entities.
|
||||
#html_use_smartypants = True
|
||||
|
||||
# Custom sidebar templates, maps document names to template names.
|
||||
#html_sidebars = {}
|
||||
|
||||
# Additional templates that should be rendered to pages, maps page names to
|
||||
# template names.
|
||||
#html_additional_pages = {}
|
||||
|
||||
# If false, no module index is generated.
|
||||
#html_domain_indices = True
|
||||
|
||||
# If false, no index is generated.
|
||||
#html_use_index = True
|
||||
|
||||
# If true, the index is split into individual pages for each letter.
|
||||
#html_split_index = False
|
||||
|
||||
# If true, links to the reST sources are added to the pages.
|
||||
#html_show_sourcelink = True
|
||||
|
||||
# If true, "Created using Sphinx" is shown in the HTML footer. Default is True.
|
||||
#html_show_sphinx = True
|
||||
|
||||
# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True.
|
||||
#html_show_copyright = True
|
||||
|
||||
# If true, an OpenSearch description file will be output, and all pages will
|
||||
# contain a <link> tag referring to it. The value of this option must be the
|
||||
# base URL from which the finished HTML is served.
|
||||
#html_use_opensearch = ''
|
||||
|
||||
# This is the file name suffix for HTML files (e.g. ".xhtml").
|
||||
#html_file_suffix = None
|
||||
|
||||
# Language to be used for generating the HTML full-text search index.
|
||||
# Sphinx supports the following languages:
|
||||
# 'da', 'de', 'en', 'es', 'fi', 'fr', 'hu', 'it', 'ja'
|
||||
# 'nl', 'no', 'pt', 'ro', 'ru', 'sv', 'tr'
|
||||
#html_search_language = 'en'
|
||||
|
||||
# A dictionary with options for the search language support, empty by default.
|
||||
# Now only 'ja' uses this config value
|
||||
#html_search_options = {'type': 'default'}
|
||||
|
||||
# The name of a javascript file (relative to the configuration directory) that
|
||||
# implements a search results scorer. If empty, the default will be used.
|
||||
#html_search_scorer = 'scorer.js'
|
||||
|
||||
# Output file base name for HTML help builder.
|
||||
htmlhelp_basename = 'IdrisManualdoc'
|
||||
|
||||
# -- Options for LaTeX output ---------------------------------------------
|
||||
|
||||
latex_title_page = r'''
|
||||
\begin{titlepage}
|
||||
\vspace*{\fill}
|
||||
\begin{center}
|
||||
\includegraphics[width=0.25\textwidth]{idris-512x512.png}\par
|
||||
\vspace{1cm}
|
||||
{\huge\sffamily\bfseries \makeatletter\@title\makeatother\par}
|
||||
\vspace{1cm}
|
||||
{\Large Version \version\par}
|
||||
\end{center}
|
||||
\vspace*{\fill}
|
||||
\end{titlepage}
|
||||
'''
|
||||
|
||||
latex_elements = {
|
||||
# The paper size ('letterpaper' or 'a4paper').
|
||||
'papersize': 'a4paper',
|
||||
|
||||
'fontpkg': '',
|
||||
'inputenc': '',
|
||||
'utf8extra': '',
|
||||
'releasename': 'Version',
|
||||
|
||||
# The font size ('10pt', '11pt' or '12pt').
|
||||
'pointsize': '10pt',
|
||||
|
||||
# Additional stuff for the LaTeX preamble.
|
||||
'preamble': r'''
|
||||
\usepackage{lmodern}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[utf8x]{inputenc}
|
||||
\usepackage{titlesec}
|
||||
%
|
||||
\usepackage{fancyhdr}
|
||||
\fancypagestyle{plain}{%
|
||||
\renewcommand{\headrulewidth}{0pt}%
|
||||
\fancyhf{}%
|
||||
\fancyfoot[C]{\textsf{\thepage}}
|
||||
}
|
||||
\pagestyle{fancy}
|
||||
\fancyhf{}
|
||||
\fancyhead[LE,RO]{\textsf{\bfseries{v\version}}}
|
||||
\fancyhead[LO,RE]{\textsf{\bfseries\leftmark}}
|
||||
%\fancyhead[LO]{\textsf{\bfseries{\leftmark}}}
|
||||
%\fancyhead[RO]{\textsf{\bfseries{v\version}}}
|
||||
%\fancyhead[RE]{\textsf{\bfseries{\leftmark}}}
|
||||
%\fancyhead[LE]{\textsf{\bfseries{v\version}}}
|
||||
\fancyfoot[C]{\textsf{\thepage}}
|
||||
\renewcommand{\footrulewidth}{0pt}
|
||||
\renewcommand{\headrulewidth}{0pt}
|
||||
%
|
||||
\usepackage[font={small,it}]{caption}
|
||||
\titleformat{\section}
|
||||
{\normalfont\sffamily\Large\bfseries\color{black}}
|
||||
{\thesection}{1em}{}
|
||||
\titleformat{\subsection}
|
||||
{\sffamily\large\bfseries\color{black}}
|
||||
{\thesubsection}{1em}{}
|
||||
\titleformat{\subsubsection}
|
||||
{\sffamily\normalsize\bfseries\color{black}}
|
||||
{\thesubsubsection}{1em}{}
|
||||
\titleformat{\paragraph}{\normalfont\normalsize\slshape}{\theparagraph}{1em}{}
|
||||
\setlength{\parskip}{1em}
|
||||
%
|
||||
\hypersetup{colorlinks = false}
|
||||
\definecolor{VerbatimBorderColor}{rgb}{1,1,1}
|
||||
''',
|
||||
|
||||
'maketitle': latex_title_page,
|
||||
'tableofcontents': "\\tableofcontents"
|
||||
# Latex figure (float) alignment
|
||||
#'figure_align': 'htbp',
|
||||
}
|
||||
|
||||
# Grouping the document tree into LaTeX files. List of tuples
|
||||
# (source start file, target name, title,
|
||||
# author, documentclass [howto, manual, or own class]).
|
||||
latex_documents = [
|
||||
('index', 'idris-documentation-complete.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report'),
|
||||
('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),
|
||||
]
|
||||
|
||||
|
||||
latex_show_pagerefs = True
|
||||
latex_show_url = 'footnote'
|
||||
|
||||
# The name of an image file (relative to this directory) to place at the top of
|
||||
# the title page.
|
||||
latex_logo = '../icons/idris-512x512.png'
|
||||
|
||||
# For "manual" documents, if this is true, then toplevel headings are parts,
|
||||
# not chapters.
|
||||
#latex_use_parts = True
|
||||
|
||||
# If true, show page references after internal links.
|
||||
#latex_show_pagerefs = False
|
||||
|
||||
# If true, show URL addresses after external links.
|
||||
#latex_show_urls = False
|
||||
|
||||
# Documents to append as an appendix to all manuals.
|
||||
#latex_appendices = []
|
||||
|
||||
# If false, no module index is generated.
|
||||
#latex_domain_indices = True
|
||||
|
||||
|
||||
# -- Options for manual page output ---------------------------------------
|
||||
|
||||
# One entry per manual page. List of tuples
|
||||
# (source start file, name, description, authors, manual section).
|
||||
man_pages = [
|
||||
(master_doc, 'idrismanual', u'Idris Manual Documentation',
|
||||
[author], 1)
|
||||
]
|
||||
|
||||
# If true, show URL addresses after external links.
|
||||
#man_show_urls = False
|
||||
|
||||
|
||||
# -- Options for Texinfo output -------------------------------------------
|
||||
|
||||
# Grouping the document tree into Texinfo files. List of tuples
|
||||
# (source start file, target name, title, author,
|
||||
# dir menu entry, description, category)
|
||||
texinfo_documents = [
|
||||
(master_doc, 'IdrisManual', u'Idris Manual Documentation',
|
||||
author, 'IdrisManual', 'One line description of project.',
|
||||
'Miscellaneous'),
|
||||
]
|
||||
|
||||
# Documents to append as an appendix to all manuals.
|
||||
#texinfo_appendices = []
|
||||
|
||||
# If false, no module index is generated.
|
||||
#texinfo_domain_indices = True
|
||||
|
||||
# How to display URL addresses: 'footnote', 'no', or 'inline'.
|
||||
#texinfo_show_urls = 'footnote'
|
||||
|
||||
# If true, do not generate a @detailmenu in the "Top" node's menu.
|
||||
#texinfo_no_detailmenu = False
|
||||
|
||||
|
||||
# -- Options for Epub output ----------------------------------------------
|
||||
|
||||
# Bibliographic Dublin Core info.
|
||||
epub_title = project
|
||||
epub_author = author
|
||||
epub_publisher = author
|
||||
epub_copyright = copyright
|
||||
|
||||
# The basename for the epub file. It defaults to the project name.
|
||||
#epub_basename = project
|
||||
|
||||
# The HTML theme for the epub output. Since the default themes are not optimized
|
||||
# for small screen space, using the same theme for HTML and epub output is
|
||||
# usually not wise. This defaults to 'epub', a theme designed to save visual
|
||||
# space.
|
||||
#epub_theme = 'epub'
|
||||
|
||||
# The language of the text. It defaults to the language option
|
||||
# or 'en' if the language is not set.
|
||||
#epub_language = ''
|
||||
|
||||
# The scheme of the identifier. Typical schemes are ISBN or URL.
|
||||
#epub_scheme = ''
|
||||
|
||||
# The unique identifier of the text. This can be a ISBN number
|
||||
# or the project homepage.
|
||||
#epub_identifier = ''
|
||||
|
||||
# A unique identification for the text.
|
||||
#epub_uid = ''
|
||||
|
||||
# A tuple containing the cover image and cover page html template filenames.
|
||||
#epub_cover = ()
|
||||
|
||||
# A sequence of (type, uri, title) tuples for the guide element of content.opf.
|
||||
#epub_guide = ()
|
||||
|
||||
# HTML files that should be inserted before the pages created by sphinx.
|
||||
# The format is a list of tuples containing the path and title.
|
||||
#epub_pre_files = []
|
||||
|
||||
# HTML files shat should be inserted after the pages created by sphinx.
|
||||
# The format is a list of tuples containing the path and title.
|
||||
#epub_post_files = []
|
||||
|
||||
# A list of files that should not be packed into the epub file.
|
||||
epub_exclude_files = ['search.html']
|
||||
|
||||
# The depth of the table of contents in toc.ncx.
|
||||
#epub_tocdepth = 3
|
||||
|
||||
# Allow duplicate toc entries.
|
||||
#epub_tocdup = True
|
||||
|
||||
# Choose between 'default' and 'includehidden'.
|
||||
#epub_tocscope = 'default'
|
||||
|
||||
# Fix unsupported image types using the Pillow.
|
||||
#epub_fix_images = False
|
||||
|
||||
# Scale large images.
|
||||
#epub_max_image_width = 0
|
||||
|
||||
# How to display URL addresses: 'footnote', 'no', or 'inline'.
|
||||
#epub_show_urls = 'inline'
|
||||
|
||||
# If false, no index is generated.
|
||||
#epub_use_index = True
|
@ -1,12 +0,0 @@
|
||||
**************************
|
||||
Frequently Asked Questions
|
||||
**************************
|
||||
|
||||
Can Idris 2 compile itself?
|
||||
===========================
|
||||
|
||||
Not yet. Although it is written in Idris, there are several changes to the
|
||||
language which are not fully backwards compatible (see Section
|
||||
:ref:`updates-index`) so, although we hope to get there fairly soon - especially
|
||||
since we are resisting using any of the more sophisticated language features -
|
||||
it's not automatically the case that it will be able to compile itself.
|
411
docs/ffi/ffi.rst
411
docs/ffi/ffi.rst
@ -1,411 +0,0 @@
|
||||
************
|
||||
FFI Overview
|
||||
************
|
||||
|
||||
Foreign functions are declared with the ``%foreign`` directive, which takes the
|
||||
following general form:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign [specifiers]
|
||||
name : t
|
||||
|
||||
The specifier is an Idris ``String`` which says in which language the foreign
|
||||
function is written, what it's called, and where to find it. There may be more
|
||||
than one specifier, and a code generator is free to choose any specifier it
|
||||
understands - or even ignore the specifiers completely and use their own
|
||||
approach. In general, a specifier has the form "Language:name,library". For
|
||||
example, in C:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign "C:puts,libc"
|
||||
puts : String -> PrimIO Int
|
||||
|
||||
It is up to specific code generators to decide how to locate the function and
|
||||
the library. In this document, we will assume the default Chez Scheme code
|
||||
generator (the examples also work with the Racket code generator) and that the
|
||||
foreign language is C.
|
||||
|
||||
Example
|
||||
-------
|
||||
|
||||
As a running example, we are going to work with a small C file. Save the
|
||||
following content to a file ``smallc.c``
|
||||
|
||||
::
|
||||
|
||||
#include <stdio.h>
|
||||
|
||||
int add(int x, int y) {
|
||||
return x+y;
|
||||
}
|
||||
|
||||
int addWithMessage(char* msg, int x, int y) {
|
||||
printf("%s: %d + %d = %d\n", msg, x, y, x+y);
|
||||
return x+y;
|
||||
}
|
||||
|
||||
Then, compile it to a shared library with::
|
||||
|
||||
cc -shared smallc.c -o libsmall.so
|
||||
|
||||
We can now write an Idris program which calls each of these. First, we'll
|
||||
write a small program which uses ``add`` to add two integers:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign "C:add,libsmall"
|
||||
add : Int -> Int -> Int
|
||||
|
||||
main : IO ()
|
||||
main = printLn (add 70 24)
|
||||
|
||||
The ``%foreign`` declaration states that ``add`` is written in C, with the
|
||||
name ``add`` in the library ``libsmall``. As long as the run time is able
|
||||
to locate ``libsmall.so`` (in practice it looks in the current directory and
|
||||
the system library paths) we can run this at the REPL:
|
||||
|
||||
::
|
||||
|
||||
Main> :exec main
|
||||
94
|
||||
|
||||
Note that it is the programmer's responsibility to make sure that the
|
||||
Idris function and C function have corresponding types. There is no way for
|
||||
the machine to check this! If you get it wrong, you will get unpredictable
|
||||
behaviour.
|
||||
|
||||
Since ``add`` has no side effects, we've given it a return type of ``Int``.
|
||||
But what if the function has some effect on the outside world, like
|
||||
``addWithMessage``? In this case, we use ``PrimIO Int`` to say that it
|
||||
returns a primitive IO action:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign "C:addWithMessage,libsmall"
|
||||
prim_addWithMessage : String -> Int -> Int -> PrimIO Int
|
||||
|
||||
Internally, ``PrimIO Int`` is a function which takes the current (linear)
|
||||
state of the world, and returns an ``Int`` with an updated state of the world.
|
||||
We can convert this into an ``IO`` action using ``primIO``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
primIO : PrimIO a -> IO a
|
||||
|
||||
So, we can extend our program as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
addWithMessage : String -> Int -> Int -> IO Int
|
||||
addWithMessage s x y = primIO $ prim_addWithMessage s x y
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do printLn (add 70 24)
|
||||
addWithMessage "Sum" 70 24
|
||||
pure ()
|
||||
|
||||
It is up to the programmer to declare which functions are pure, and which have
|
||||
side effects, via ``PrimIO``. Executing this gives:
|
||||
|
||||
::
|
||||
|
||||
Main> :exec main
|
||||
94
|
||||
Sum: 70 + 24 = 94
|
||||
|
||||
We have seen two specifiers for foreign functions:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign "C:add,libsmall"
|
||||
%foreign "C:addWithMessage,libsmall"
|
||||
|
||||
These both have the same form: ``"C:[name],libsmall"`` so instead of writing
|
||||
the concrete ``String``, we write a function to compute the specifier, and
|
||||
use that instead:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
libsmall : String -> String
|
||||
libsmall fn = "C:" ++ fn ++ ",libsmall"
|
||||
|
||||
%foreign (libsmall "add")
|
||||
add : Int -> Int -> Int
|
||||
|
||||
%foreign (libsmall "addWithMessage")
|
||||
prim_addWithMessage : String -> Int -> Int -> PrimIO Int
|
||||
|
||||
.. _sect-ffi-string:
|
||||
|
||||
Primitive FFI Types
|
||||
-------------------
|
||||
|
||||
The types which can be passed to and returned from foreign functions are
|
||||
restricted to those which it is reasonable to assume any back end can handle.
|
||||
In practice, this means most primitive types, and a limited selection of
|
||||
others. Argument types can be any of the following primitives:
|
||||
|
||||
* ``Int``
|
||||
* ``Char``
|
||||
* ``Double`` (as ``double`` in C)
|
||||
* ``String`` (as ``char*`` in C)
|
||||
* ``Ptr t`` and ``AnyPtr`` (both as ``void*`` in C)
|
||||
|
||||
Return types can be any of the above, plus:
|
||||
|
||||
* ``()``
|
||||
* ``PrimIO t``, where ``t`` is a valid return type other than a ``PrimIO``.
|
||||
|
||||
Handling ``String`` leads to some complications, for a number of reasons:
|
||||
|
||||
* Strings can have multiple encodings. In the Idris run time, Strings are
|
||||
encoded as UTF-8, but C makes no assumptions.
|
||||
* It is not always clear who is responsible for freeing a ``String`` allocated
|
||||
by a C function.
|
||||
* In C, strings can be ``NULL``, but Idris strings always have a value.
|
||||
|
||||
So, when passing ``String`` to and from C, remember the following:
|
||||
|
||||
* A ``char*`` returned by a C function will be copied to the Idris heap, and
|
||||
the Idris run time immediately calls ``free`` with the returned ``char*``.
|
||||
* If a ``char*`` might be ``NULL`` in ``C``, use ``Ptr String`` rather than
|
||||
``String``.
|
||||
|
||||
When using ``Ptr String``, the value will be passed as a ``void*``, and
|
||||
therefore not accessible directly by Idris code. This is to protect against
|
||||
accidentally trying to use ``NULL`` as a ``String``. You can nevertheless
|
||||
work with them and convert to ``String`` via foreign functions of the following
|
||||
form:
|
||||
|
||||
::
|
||||
|
||||
char* getString(void *p) {
|
||||
return (char*)p;
|
||||
}
|
||||
|
||||
void* mkString(char* str) {
|
||||
return (void*)str;
|
||||
}
|
||||
|
||||
int isNullString(void* str) {
|
||||
return str == NULL;
|
||||
}
|
||||
|
||||
For an example, see the sample :ref:`sect-readline` bindings.
|
||||
|
||||
Additionally, foreign functions can take *callbacks*, and take and return
|
||||
C ``struct`` pointers.
|
||||
|
||||
.. _sect-callbacks:
|
||||
|
||||
Callbacks
|
||||
---------
|
||||
|
||||
It is often useful in C for a function to take a *callback*, that is a function
|
||||
which is called after doing some work. For example, we can write a function
|
||||
which takes a callback that takes a ``char*`` and an ``int`` and returns a
|
||||
``char*``, in C, as follows (added to ``smallc.c`` above):
|
||||
|
||||
::
|
||||
|
||||
typedef char*(*StringFn)(char*, int);
|
||||
|
||||
char* applyFn(char* x, int y, StringFn f) {
|
||||
printf("Applying callback to %s %d\n", x, y);
|
||||
return f(x, y);
|
||||
}
|
||||
|
||||
Then, we can access this from Idris by declaring it as a ``%foreign``
|
||||
function and wrapping it in ``IO``, with the C function calling the Idris
|
||||
function as the callback:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (libsmall "applyFn")
|
||||
prim_applyFn : String -> Int -> (String -> Int -> String) -> PrimIO String
|
||||
|
||||
applyFn : String -> Int -> (String -> Int -> String) -> IO String
|
||||
applyFn c i f = primIO $ prim_applyFn c i f
|
||||
|
||||
For example, we can try this as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
pluralise : String -> Int -> String
|
||||
pluralise str x
|
||||
= show x ++ " " ++
|
||||
if x == 1
|
||||
then str
|
||||
else str ++ "s"
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do str1 <- applyFn "Biscuit" 10 pluralise
|
||||
putStrLn str1
|
||||
str2 <- applyFn "Tree" 1 pluralise
|
||||
putStrLn str2
|
||||
|
||||
As a variant, the callback could have a side effect:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (libsmall "applyFn")
|
||||
prim_applyFnIO : String -> Int -> (String -> Int -> PrimIO String) ->
|
||||
PrimIO String
|
||||
|
||||
This is a little more fiddly to lift to an ``IO`` function, due to the callback,
|
||||
but we can do so using ``toPrim : IO a -> PrimIO a``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
applyFnIO : String -> Int -> (String -> Int -> IO String) -> IO String
|
||||
applyFnIO c i f = primIO $ prim_applyFnIO c i (\s, i => toPrim $ f s i)
|
||||
|
||||
For example, we can extend the above ``pluralise`` example to print a message
|
||||
in the callback:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
pluralise : String -> Int -> IO String
|
||||
pluralise str x
|
||||
= do putStrLn "Pluralising"
|
||||
pure $ show x ++ " " ++
|
||||
if x == 1
|
||||
then str
|
||||
else str ++ "s"
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do str1 <- applyFnIO "Biscuit" 10 pluralise
|
||||
putStrLn str1
|
||||
str2 <- applyFnIO "Tree" 1 pluralise
|
||||
putStrLn str2
|
||||
|
||||
Structs
|
||||
-------
|
||||
|
||||
Many C APIs pass around more complex data structures, as a ``struct``.
|
||||
We do not aim to be completely general in the C types we support, because
|
||||
this will make it harder to write code which is portable across multiple
|
||||
back ends. However, it is still often useful to be able to access a ``struct``
|
||||
directly. For example, add the following to the top of ``smallc.c``, and
|
||||
rebuild ``libsmall.so``:
|
||||
|
||||
::
|
||||
|
||||
#include <stdlib.h>
|
||||
|
||||
typedef struct {
|
||||
int x;
|
||||
int y;
|
||||
} point;
|
||||
|
||||
point* mkPoint(int x, int y) {
|
||||
point* pt = malloc(sizeof(point));
|
||||
pt->x = x;
|
||||
pt->y = y;
|
||||
return pt;
|
||||
}
|
||||
|
||||
void freePoint(point* pt) {
|
||||
free(pt);
|
||||
}
|
||||
|
||||
We can define a type for accessing ``point`` in Idris by importing
|
||||
``System.FFI`` and using the ``Struct`` type, as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Point : Type
|
||||
Point = Struct "point" [("x", Int), ("y", Int)]
|
||||
|
||||
%foreign (libsmall "mkPoint")
|
||||
mkPoint : Int -> Int -> Point
|
||||
|
||||
%foreign (libsmall "freePoint")
|
||||
prim_freePoint : Point -> PrimIO ()
|
||||
|
||||
freePoint : Point -> IO ()
|
||||
freePoint p = primIO $ prim_freePoint p
|
||||
|
||||
The ``Point`` type in Idris now corresponds to ``point*`` in C. Fields can
|
||||
be read and written using the following, also from ``System.FFI``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
getField : Struct s fs -> (n : String) ->
|
||||
FieldType n ty fs => ty
|
||||
setField : Struct s fs -> (n : String) ->
|
||||
FieldType n ty fs => ty -> IO ()
|
||||
|
||||
Notice that fields are accessed by name, and must be available in the
|
||||
struct, given the constraint ``FieldType n ty fs``, which states that the
|
||||
field named ``n`` has type ``ty`` in the structure fields ``fs``.
|
||||
So, we can display a ``Point`` as follows by accessing the fields directly:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
showPoint : Point -> String
|
||||
showPoint pt
|
||||
= let x : Int = getField pt "x"
|
||||
y : Int = getField pt "y" in
|
||||
show (x, y)
|
||||
|
||||
And, as a complete example, we can initialise, update, display and
|
||||
delete a ``Point`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
main : IO ()
|
||||
main = do let pt = mkPoint 20 30
|
||||
setField pt "x" (the Int 40)
|
||||
putStrLn $ showPoint pt
|
||||
freePoint pt
|
||||
|
||||
The field types of a ``Struct`` can be any of the following:
|
||||
|
||||
* ``Int``
|
||||
* ``Char``
|
||||
* ``Double`` (``double`` in C)
|
||||
* ``Ptr a`` or ``AnyPtr`` (``void*`` in C)
|
||||
* Another ``Struct``, which is a pointer to a ``struct`` in C
|
||||
|
||||
Note that this doesn't include ``String`` or function types! This is primarily
|
||||
because these aren't directly supported by the Chez back end. However, you can
|
||||
use another pointer type and convert. For example, assuming you have, in C:
|
||||
|
||||
::
|
||||
|
||||
typedef struct {
|
||||
char* name;
|
||||
point* pt;
|
||||
} namedpoint;
|
||||
|
||||
You can represent this in Idris as:
|
||||
|
||||
::
|
||||
|
||||
NamedPoint : Type
|
||||
NamedPoint
|
||||
= Struct "namedpoint"
|
||||
[("name", Ptr String),
|
||||
("pt", Point)]
|
||||
|
||||
That is, using a ``Ptr String`` instead of a ``String`` directly. Then you
|
||||
can convert between a ``void*`` and a ``char*`` in C:
|
||||
|
||||
::
|
||||
|
||||
char* getString(void *p) {
|
||||
return (char*)p;
|
||||
}
|
||||
|
||||
...and use this to convert to a ``String`` in Idris:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (pfn "getString")
|
||||
getString : Ptr String -> String
|
@ -1,30 +0,0 @@
|
||||
**************************
|
||||
Foreign Function Interface
|
||||
**************************
|
||||
|
||||
.. note::
|
||||
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
Idris 2 is designed to support multiple code generators. The default target is
|
||||
Chez Scheme, with a Racket code generator also supported. However, the
|
||||
intention is, as with Idris 1, to support multiple targets on multiple platforms,
|
||||
including e.g. JavaScript, JVM, .NET, and others yet to be invented.
|
||||
This makes the design of a foreign function interface (FFI), which calls
|
||||
functions in other languages, a little challenging, since ideally it will
|
||||
support all possible targets!
|
||||
|
||||
To this end, the Idris 2 FFI aims to be flexible and adaptable, while still
|
||||
supporting most common requirements without too much need for "glue" code in
|
||||
the foreign language.
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
ffi
|
||||
readline
|
@ -1,307 +0,0 @@
|
||||
.. _sect-readline:
|
||||
|
||||
**********************************
|
||||
Example: Minimal Readline Bindings
|
||||
**********************************
|
||||
|
||||
In this section, we'll see how to create bindings for a C library (the `GNU
|
||||
Readline <https://tiswww.case.edu/php/chet/readline/rltop.html>`_ library) in
|
||||
Idris, and make them available in a package. We'll only create the most minimal
|
||||
bindings, but nevertheless they demonstrate some of the trickier problems in
|
||||
creating bindings to a C library, in that they need to handle memory allocation
|
||||
of ``String``.
|
||||
|
||||
You can find the example in full in the Idris 2 source repository,
|
||||
in `samples/FFI-readline
|
||||
<https://github.com/edwinb/Idris2/tree/master/samples/FFI-readline>`_. As a
|
||||
minimal example, this can be used as a starting point for other C library
|
||||
bindings.
|
||||
|
||||
We are going to provide bindings to the following functions in the Readline
|
||||
API, available via ``#include <readline/readline.h>``:
|
||||
|
||||
::
|
||||
|
||||
char* readline (const char *prompt);
|
||||
void add_history(const char *string);
|
||||
|
||||
Additionally, we are going to support tab completion, which in the Readline
|
||||
API is achieved by setting a global variable to a callback function
|
||||
(see Section :ref:`sect-callbacks`) which explains how to handle the
|
||||
completion:
|
||||
|
||||
::
|
||||
|
||||
typedef char *rl_compentry_func_t (const char *, int);
|
||||
rl_compentry_func_t * rl_completion_entry_function;
|
||||
|
||||
A completion function takes a ``String``, which is the text to complete, and
|
||||
an ``Int``, which is the number of times it has asked for a completion so far.
|
||||
In Idris, this could be a function ``complete : String -> Int -> IO String``.
|
||||
So, for example, if the text so far is ``"id"``, and the possible completions
|
||||
are ``idiomatic`` and ``idris``, then ``complete "id" 0`` would produce the
|
||||
string ``"idiomatic"`` and ``complete "id" 1`` would produce ``"idris"``.
|
||||
|
||||
We will define *glue* functions in a C file ``idris_readline.c``, which compiles
|
||||
to a shared object ``libidrisreadline``, so we write a function for locating
|
||||
the C functions:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
rlib : String -> String
|
||||
rlib fn = "C:" ++ fn ++ ",libidrisreadline"
|
||||
|
||||
Each of the foreign bindings will have a ``%foreign`` specifier which locates
|
||||
functions via ``rlib``.
|
||||
|
||||
Basic behaviour: Reading input, and history
|
||||
-------------------------------------------
|
||||
|
||||
We can start by writing a binding for ``readline`` directly. It's interactive,
|
||||
so needs to return a ``PrimIO``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "readline")
|
||||
prim_readline : String -> PrimIO String
|
||||
|
||||
Then, we can write an ``IO`` wrapper:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
readline : String -> IO String
|
||||
readline prompt = primIO $ readline prompt
|
||||
|
||||
Unfortunately, this isn't quite good enough! The C ``readline`` function
|
||||
returns a ``NULL`` string if there is no input due to encountering an
|
||||
end of file. So, we need to handle that - if we don't, we'll get a crash
|
||||
on encountering end of file (remember: it's the Idris programmer's responsibility
|
||||
to give an appropriate type to the C binding!)
|
||||
|
||||
Instead, we need to use a ``Ptr`` to say that it might be a ``NULL``
|
||||
pointer (see Section :ref:`sect-ffi-string`):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "readline")
|
||||
prim_readline : String -> PrimIO (Ptr String)
|
||||
|
||||
We also need to provide a way to check whether the returned ``Ptr String`` is
|
||||
``NULL``. To do so, we'll write some glue code to convert back and forth
|
||||
between ``Ptr String`` and ``String``, in a file ``idris_readline.c`` and a
|
||||
corresponding header ``idris_readline.h``. In ``idris_readline.h`` we have:
|
||||
|
||||
::
|
||||
|
||||
int isNullString(void* str); // return 0 if a string in NULL, non zero otherwise
|
||||
char* getString(void* str); // turn a non-NULL Ptr String into a String (assuming not NULL)
|
||||
void* mkString(char* str); // turn a String into a Ptr String
|
||||
void* nullString(); // create a new NULL String
|
||||
|
||||
Correspondingly, in ``idris_readline.c``:
|
||||
|
||||
::
|
||||
|
||||
int isNullString(void* str) {
|
||||
return str == NULL;
|
||||
}
|
||||
|
||||
char* getString(void* str) {
|
||||
return (char*)str;
|
||||
}
|
||||
|
||||
void* mkString(char* str) {
|
||||
return (void*)str;
|
||||
}
|
||||
|
||||
void* nullString() {
|
||||
return NULL;
|
||||
}
|
||||
|
||||
Now, we can use ``prim_readline`` as follows, with a safe API, checking
|
||||
whether the result it returns is ``NULL`` or a concrete ``String``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "isNullString")
|
||||
prim_isNullString : Ptr String -> Int
|
||||
|
||||
export
|
||||
isNullString : Ptr String -> Bool
|
||||
isNullString str = if prim_isNullString str == 0 then False else True
|
||||
|
||||
export
|
||||
readline : String -> IO (Maybe String)
|
||||
readline s
|
||||
= do mstr <- primIO $ prim_readline s
|
||||
if isNullString mstr
|
||||
then pure $ Nothing
|
||||
else pure $ Just (getString mstr)
|
||||
|
||||
We'll need ``nullString`` and ``mkString`` later, for dealing with completions.
|
||||
|
||||
Once we've read a string, we'll want to add it to the input history. We can
|
||||
provide a binding to ``add_history`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "add_history")
|
||||
prim_add_history : String -> PrimIO ()
|
||||
|
||||
export
|
||||
addHistory : String -> IO ()
|
||||
addHistory s = primIO $ prim_add_history s
|
||||
|
||||
In this case, since Idris is in control of the ``String``, we know it's not
|
||||
going to be ``NULL``, so we can add it directly.
|
||||
|
||||
A small ``readline`` program that reads input, and echoes it, recording input
|
||||
history for non-empty inputs, can be written as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
echoLoop : IO ()
|
||||
echoLoop
|
||||
= do Just x <- readline "> "
|
||||
| Nothing => putStrLn "EOF"
|
||||
putStrLn ("Read: " ++ x)
|
||||
when (x /= "") $ addHistory x
|
||||
if x /= "quit"
|
||||
then echoLoop
|
||||
else putStrLn "Done"
|
||||
|
||||
This gives us command history, and command line editing, but Readline becomes
|
||||
much more useful when we add tab completion. The default tab completion, which
|
||||
is available even in the small example above, is to tab complete file names
|
||||
in the current working directory. But for any realistic application, we probably
|
||||
want to tab complete other commands, such as function names, references to
|
||||
local data, or anything that is appropriate for the application.
|
||||
|
||||
Completions
|
||||
-----------
|
||||
|
||||
Readline has a large API, with several ways of supporting tab completion,
|
||||
typically involving setting a global variable to an appropriate completion
|
||||
function. We'll use the following:
|
||||
|
||||
::
|
||||
|
||||
typedef char *rl_compentry_func_t (const char *, int);
|
||||
rl_compentry_func_t * rl_completion_entry_function;
|
||||
|
||||
The completion function takes the prefix of the completion, and the number
|
||||
of times it has been called so far on this prefix, and returns the next
|
||||
completion, or ``NULL`` if there are no more completions. An Idris equivalent
|
||||
would therefore have the following type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
|
||||
|
||||
The function returns ``Nothing`` if there are no more completions, or
|
||||
``Just str`` for some ``str`` if there is another one for the current
|
||||
input.
|
||||
|
||||
We might hope that it's a matter of defining a function to assign the
|
||||
completion function...
|
||||
|
||||
::
|
||||
|
||||
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
|
||||
rl_completion_entry_function = fn;
|
||||
}
|
||||
|
||||
...then defining the Idris binding, which needs to take into account that
|
||||
the Readline library expects ``NULL`` when there are no more completions:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%foreign (rlib "idrisrl_setCompletion")
|
||||
prim_setCompletion : (String -> Int -> PrimIO (Ptr String)) -> PrimIO ()
|
||||
|
||||
export
|
||||
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
|
||||
setCompletionFn fn
|
||||
= primIO $ prim_setCompletion $ \s, i => toPrim $
|
||||
do mstr <- fn s i
|
||||
case mstr of
|
||||
Nothing => pure nullString // need to return a Ptr String to readline!
|
||||
Just str => pure (mkString str)
|
||||
|
||||
So, we turn ``Nothing`` into ``nullString`` and ``Just str`` into ``mkString
|
||||
str``. Unfortunately, this doesn't quite work. To see what goes wrong, let's
|
||||
try it for the most basic completion function that returns one completion no
|
||||
matter what the input:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
testComplete : String -> Int -> IO (Maybe String)
|
||||
testComplete text 0 = pure $ Just "hamster"
|
||||
testComplete text st = pure Nothing
|
||||
|
||||
We'll try this in a small modification of ``echoLoop`` above, setting a
|
||||
completion function first:
|
||||
|
||||
.. code-block :: idris
|
||||
|
||||
main : IO ()
|
||||
main = do setCompletionFn testComplete
|
||||
echoLoop
|
||||
|
||||
We see that there is a problem when we try running it, and hitting TAB before
|
||||
entering anything:
|
||||
|
||||
::
|
||||
|
||||
Main> :exec main
|
||||
> free(): invalid pointer
|
||||
|
||||
The Idris code which sets up the completion is fine, but there is a problem
|
||||
with the memory allocation in the C glue code.
|
||||
|
||||
This problem arises because we haven't thought carefully enough about which
|
||||
parts of our program are responsible for allocating and freeing strings.
|
||||
When Idris calls a foreign function that returns a string, it copies the
|
||||
string to the Idris heap and frees it immediately. But, if the foreign
|
||||
library also frees the string, it ends up being freed twice. This is what's
|
||||
happening here: the callback passed to ``prim_setCompletion`` frees the string
|
||||
and puts it onto the Idris heap, but Readline also frees the string returned
|
||||
by ``prim_setCompletion`` once it has processed it. We can solve this
|
||||
problem by writing a wrapper for the completion function which reallocates
|
||||
the string, and using that in ``idrisrl_setCompletion`` instead.
|
||||
|
||||
::
|
||||
|
||||
rl_compentry_func_t* my_compentry;
|
||||
|
||||
char* compentry_wrapper(const char* text, int i) {
|
||||
char* res = my_compentry(text, i); // my_compentry is an Idris function, so res is on the Idris heap,
|
||||
// and freed on return
|
||||
if (res != NULL) {
|
||||
char* comp = malloc(strlen(res)+1); // comp is passed back to readline, which frees it when
|
||||
// it is finished with it
|
||||
strcpy(comp, res);
|
||||
return comp;
|
||||
}
|
||||
else {
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
|
||||
void idrisrl_setCompletion(rl_compentry_func_t* fn) {
|
||||
rl_completion_entry_function = compentry_wrapper;
|
||||
my_compentry = fn; // fn is an Idris function, called by compentry_wrapper
|
||||
}
|
||||
|
||||
So, we define the completion function in C, which calls the Idris completion
|
||||
function then makes sure the string returned by the Idris function is copied
|
||||
to the C heap.
|
||||
|
||||
We now have a primitive API that covers the most fundamental features of the
|
||||
readline API:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
readline : String -> IO (Maybe String)
|
||||
addHistory : String -> IO ()
|
||||
setCompletionFn : (String -> Int -> IO (Maybe String)) -> IO ()
|
@ -1,29 +0,0 @@
|
||||
.. Idris Manual documentation master file, created by
|
||||
sphinx-quickstart on Sat Feb 28 20:41:47 2015.
|
||||
You can adapt this file completely to your liking, but it should at least
|
||||
contain the root `toctree` directive.
|
||||
|
||||
Documentation for the Idris 2 Language
|
||||
======================================
|
||||
|
||||
.. note::
|
||||
|
||||
The documentation for Idris 2 has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
tutorial/index
|
||||
backends/index
|
||||
updates/updates
|
||||
typedd/typedd
|
||||
app/index
|
||||
ffi/index
|
||||
proofs/index
|
||||
faq/faq
|
||||
reference/index
|
@ -1,15 +0,0 @@
|
||||
$ idris hello.idr
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.1.0
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||
|
||||
Welcome to Idris 2. Enjoy yourself!
|
||||
Main> :t main
|
||||
Main.main : IO ()
|
||||
Main> :c hello main
|
||||
compiling hello.ss with output to hello.so
|
||||
File hello.so written
|
||||
Main> :q
|
||||
Bye for now!
|
@ -1,11 +0,0 @@
|
||||
$ idris2 interp.idr
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.1.0
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||
|
||||
Welcome to Idris 2. Enjoy yourself!
|
||||
Main> :exec main
|
||||
Enter a number: 6
|
||||
720
|
@ -1,9 +0,0 @@
|
||||
$ idris2
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.1.0
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/ Type :? for help
|
||||
|
||||
Welcome to Idris 2. Enjoy yourself!
|
||||
Main>
|
263
docs/make.bat
263
docs/make.bat
@ -1,263 +0,0 @@
|
||||
@ECHO OFF
|
||||
|
||||
REM Command file for Sphinx documentation
|
||||
|
||||
if "%SPHINXBUILD%" == "" (
|
||||
set SPHINXBUILD=sphinx-build
|
||||
)
|
||||
set BUILDDIR=_build
|
||||
set ALLSPHINXOPTS=-d %BUILDDIR%/doctrees %SPHINXOPTS% .
|
||||
set I18NSPHINXOPTS=%SPHINXOPTS% .
|
||||
if NOT "%PAPER%" == "" (
|
||||
set ALLSPHINXOPTS=-D latex_paper_size=%PAPER% %ALLSPHINXOPTS%
|
||||
set I18NSPHINXOPTS=-D latex_paper_size=%PAPER% %I18NSPHINXOPTS%
|
||||
)
|
||||
|
||||
if "%1" == "" goto help
|
||||
|
||||
if "%1" == "help" (
|
||||
:help
|
||||
echo.Please use `make ^<target^>` where ^<target^> is one of
|
||||
echo. html to make standalone HTML files
|
||||
echo. dirhtml to make HTML files named index.html in directories
|
||||
echo. singlehtml to make a single large HTML file
|
||||
echo. pickle to make pickle files
|
||||
echo. json to make JSON files
|
||||
echo. htmlhelp to make HTML files and a HTML help project
|
||||
echo. qthelp to make HTML files and a qthelp project
|
||||
echo. devhelp to make HTML files and a Devhelp project
|
||||
echo. epub to make an epub
|
||||
echo. latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter
|
||||
echo. text to make text files
|
||||
echo. man to make manual pages
|
||||
echo. texinfo to make Texinfo files
|
||||
echo. gettext to make PO message catalogs
|
||||
echo. changes to make an overview over all changed/added/deprecated items
|
||||
echo. xml to make Docutils-native XML files
|
||||
echo. pseudoxml to make pseudoxml-XML files for display purposes
|
||||
echo. linkcheck to check all external links for integrity
|
||||
echo. doctest to run all doctests embedded in the documentation if enabled
|
||||
echo. coverage to run coverage check of the documentation if enabled
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "clean" (
|
||||
for /d %%i in (%BUILDDIR%\*) do rmdir /q /s %%i
|
||||
del /q /s %BUILDDIR%\*
|
||||
goto end
|
||||
)
|
||||
|
||||
|
||||
REM Check if sphinx-build is available and fallback to Python version if any
|
||||
%SPHINXBUILD% 2> nul
|
||||
if errorlevel 9009 goto sphinx_python
|
||||
goto sphinx_ok
|
||||
|
||||
:sphinx_python
|
||||
|
||||
set SPHINXBUILD=python -m sphinx.__init__
|
||||
%SPHINXBUILD% 2> nul
|
||||
if errorlevel 9009 (
|
||||
echo.
|
||||
echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
|
||||
echo.installed, then set the SPHINXBUILD environment variable to point
|
||||
echo.to the full path of the 'sphinx-build' executable. Alternatively you
|
||||
echo.may add the Sphinx directory to PATH.
|
||||
echo.
|
||||
echo.If you don't have Sphinx installed, grab it from
|
||||
echo.https://www.sphinx-doc.org/
|
||||
exit /b 1
|
||||
)
|
||||
|
||||
:sphinx_ok
|
||||
|
||||
|
||||
if "%1" == "html" (
|
||||
%SPHINXBUILD% -b html %ALLSPHINXOPTS% %BUILDDIR%/html
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The HTML pages are in %BUILDDIR%/html.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "dirhtml" (
|
||||
%SPHINXBUILD% -b dirhtml %ALLSPHINXOPTS% %BUILDDIR%/dirhtml
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The HTML pages are in %BUILDDIR%/dirhtml.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "singlehtml" (
|
||||
%SPHINXBUILD% -b singlehtml %ALLSPHINXOPTS% %BUILDDIR%/singlehtml
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The HTML pages are in %BUILDDIR%/singlehtml.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "pickle" (
|
||||
%SPHINXBUILD% -b pickle %ALLSPHINXOPTS% %BUILDDIR%/pickle
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; now you can process the pickle files.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "json" (
|
||||
%SPHINXBUILD% -b json %ALLSPHINXOPTS% %BUILDDIR%/json
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; now you can process the JSON files.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "htmlhelp" (
|
||||
%SPHINXBUILD% -b htmlhelp %ALLSPHINXOPTS% %BUILDDIR%/htmlhelp
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; now you can run HTML Help Workshop with the ^
|
||||
.hhp project file in %BUILDDIR%/htmlhelp.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "qthelp" (
|
||||
%SPHINXBUILD% -b qthelp %ALLSPHINXOPTS% %BUILDDIR%/qthelp
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; now you can run "qcollectiongenerator" with the ^
|
||||
.qhcp project file in %BUILDDIR%/qthelp, like this:
|
||||
echo.^> qcollectiongenerator %BUILDDIR%\qthelp\IdrisManual.qhcp
|
||||
echo.To view the help file:
|
||||
echo.^> assistant -collectionFile %BUILDDIR%\qthelp\IdrisManual.ghc
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "devhelp" (
|
||||
%SPHINXBUILD% -b devhelp %ALLSPHINXOPTS% %BUILDDIR%/devhelp
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "epub" (
|
||||
%SPHINXBUILD% -b epub %ALLSPHINXOPTS% %BUILDDIR%/epub
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The epub file is in %BUILDDIR%/epub.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "latex" (
|
||||
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; the LaTeX files are in %BUILDDIR%/latex.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "latexpdf" (
|
||||
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
|
||||
cd %BUILDDIR%/latex
|
||||
make all-pdf
|
||||
cd %~dp0
|
||||
echo.
|
||||
echo.Build finished; the PDF files are in %BUILDDIR%/latex.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "latexpdfja" (
|
||||
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
|
||||
cd %BUILDDIR%/latex
|
||||
make all-pdf-ja
|
||||
cd %~dp0
|
||||
echo.
|
||||
echo.Build finished; the PDF files are in %BUILDDIR%/latex.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "text" (
|
||||
%SPHINXBUILD% -b text %ALLSPHINXOPTS% %BUILDDIR%/text
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The text files are in %BUILDDIR%/text.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "man" (
|
||||
%SPHINXBUILD% -b man %ALLSPHINXOPTS% %BUILDDIR%/man
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The manual pages are in %BUILDDIR%/man.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "texinfo" (
|
||||
%SPHINXBUILD% -b texinfo %ALLSPHINXOPTS% %BUILDDIR%/texinfo
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The Texinfo files are in %BUILDDIR%/texinfo.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "gettext" (
|
||||
%SPHINXBUILD% -b gettext %I18NSPHINXOPTS% %BUILDDIR%/locale
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The message catalogs are in %BUILDDIR%/locale.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "changes" (
|
||||
%SPHINXBUILD% -b changes %ALLSPHINXOPTS% %BUILDDIR%/changes
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.The overview file is in %BUILDDIR%/changes.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "linkcheck" (
|
||||
%SPHINXBUILD% -b linkcheck %ALLSPHINXOPTS% %BUILDDIR%/linkcheck
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Link check complete; look for any errors in the above output ^
|
||||
or in %BUILDDIR%/linkcheck/output.txt.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "doctest" (
|
||||
%SPHINXBUILD% -b doctest %ALLSPHINXOPTS% %BUILDDIR%/doctest
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Testing of doctests in the sources finished, look at the ^
|
||||
results in %BUILDDIR%/doctest/output.txt.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "coverage" (
|
||||
%SPHINXBUILD% -b coverage %ALLSPHINXOPTS% %BUILDDIR%/coverage
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Testing of coverage in the sources finished, look at the ^
|
||||
results in %BUILDDIR%/coverage/python.txt.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "xml" (
|
||||
%SPHINXBUILD% -b xml %ALLSPHINXOPTS% %BUILDDIR%/xml
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The XML files are in %BUILDDIR%/xml.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "pseudoxml" (
|
||||
%SPHINXBUILD% -b pseudoxml %ALLSPHINXOPTS% %BUILDDIR%/pseudoxml
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The pseudo-XML files are in %BUILDDIR%/pseudoxml.
|
||||
goto end
|
||||
)
|
||||
|
||||
:end
|
@ -1,210 +0,0 @@
|
||||
Before we discuss the details of theorem proving in Idris, we will describe
|
||||
some fundamental concepts:
|
||||
|
||||
- Propositions and judgments
|
||||
- Boolean and constructive logic
|
||||
- Curry-Howard correspondence
|
||||
- Definitional and propositional equalities
|
||||
- Axiomatic and constructive approaches
|
||||
|
||||
Propositions and Judgments
|
||||
==========================
|
||||
|
||||
Propositions are the subject of our proofs. Before the proof, we can't
|
||||
formally say if they are true or not. If the proof is successful then the
|
||||
result is a 'judgment'. For instance, if the ``proposition`` is,
|
||||
|
||||
+-------+
|
||||
| 1+1=2 |
|
||||
+-------+
|
||||
|
||||
When we prove it, the ``judgment`` is,
|
||||
|
||||
+------------+
|
||||
| 1+1=2 true |
|
||||
+------------+
|
||||
|
||||
Or if the ``proposition`` is,
|
||||
|
||||
+-------+
|
||||
| 1+1=3 |
|
||||
+-------+
|
||||
|
||||
we can't prove it is true, but it is still a valid proposition and perhaps we
|
||||
can prove it is false so the ``judgment`` is,
|
||||
|
||||
+-------------+
|
||||
| 1+1=3 false |
|
||||
+-------------+
|
||||
|
||||
This may seem a bit pedantic but it is important to be careful: in mathematics
|
||||
not every proposition is true or false. For instance, a proposition may be
|
||||
unproven or even unprovable.
|
||||
|
||||
So the logic here is different from the logic that comes from boolean algebra.
|
||||
In that case what is not true is false and what is not false is true. The logic
|
||||
we are using here does not have this law, the "Law of Excluded Middle", so we
|
||||
cannot use it.
|
||||
|
||||
A false proposition is taken to be a contradiction and if we have a
|
||||
contradiction then we can prove anything, so we need to avoid this. Some
|
||||
languages, used in proof assistants, prevent contradictions.
|
||||
|
||||
The logic we are using is called constructive (or sometimes intuitional)
|
||||
because we are constructing a 'database' of judgments.
|
||||
|
||||
Curry-Howard correspondence
|
||||
---------------------------
|
||||
|
||||
So how do we relate these proofs to Idris programs? It turns out that there is
|
||||
a correspondence between constructive logic and type theory. They have the same
|
||||
structure and we can switch back and forth between the two notations.
|
||||
|
||||
The way that this works is that a proposition is a type so...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> 1 + 1 = 2
|
||||
2 = 2
|
||||
|
||||
Main> :t 1 + 1 = 2
|
||||
(fromInteger 1 + fromInteger 1) === fromInteger 2 : Type
|
||||
|
||||
...is a proposition and it is also a type. The
|
||||
following will also produce an equality type:
|
||||
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> 1 + 1 = 3
|
||||
2 = 3
|
||||
|
||||
Both of these are valid propositions so both are valid equality types. But how
|
||||
do we represent a true judgment? That is, how do we denote 1+1=2 is true but not
|
||||
1+1=3? A type that is true is inhabited, that is, it can be constructed. An
|
||||
equality type has only one constructor 'Refl' so a proof of 1+1=2 is
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
onePlusOne : 1+1=2
|
||||
onePlusOne = Refl
|
||||
|
||||
Now that we can represent propositions as types other aspects of
|
||||
propositional logic can also be translated to types as follows:
|
||||
|
||||
+----------+-------------------+--------------------------+
|
||||
| | propositions | example of possible type |
|
||||
+----------+-------------------+--------------------------+
|
||||
| A | x=y | |
|
||||
+----------+-------------------+--------------------------+
|
||||
| B | y=z | |
|
||||
+----------+-------------------+--------------------------+
|
||||
| and | A /\ B | Pair(x=y,y=z) |
|
||||
+----------+-------------------+--------------------------+
|
||||
| or | A \/ B | Either(x=y,y=z) |
|
||||
+----------+-------------------+--------------------------+
|
||||
| implies | A -> B | (x=y) -> (y=x) |
|
||||
+----------+-------------------+--------------------------+
|
||||
| for all | y=z | |
|
||||
+----------+-------------------+--------------------------+
|
||||
| exists | y=z | |
|
||||
+----------+-------------------+--------------------------+
|
||||
|
||||
|
||||
And (conjunction)
|
||||
-----------------
|
||||
|
||||
We can have a type which corresponds to conjunction:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
AndIntro : a -> b -> A a b
|
||||
|
||||
There is a built in type called 'Pair'.
|
||||
|
||||
Or (disjunction)
|
||||
----------------
|
||||
|
||||
We can have a type which corresponds to disjunction:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Or : Type -> Type -> Type where
|
||||
OrIntroLeft : a -> A a b
|
||||
OrIntroRight : b -> A a b
|
||||
|
||||
There is a built in type called 'Either'.
|
||||
|
||||
Definitional and Propositional Equalities
|
||||
-----------------------------------------
|
||||
|
||||
We have seen that we can 'prove' a type by finding a way to construct a term.
|
||||
In the case of equality types there is only one constructor which is ``Refl``.
|
||||
We have also seen that each side of the equation does not have to be identical
|
||||
like '2=2'. It is enough that both sides are *definitionally equal* like this:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
onePlusOne : 1+1=2
|
||||
onePlusOne = Refl
|
||||
|
||||
Both sides of this equation normalise to 2 and so Refl matches and the
|
||||
proposition is proved.
|
||||
|
||||
We don't have to stick to terms; we can also use symbolic parameters so the
|
||||
following type checks:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
varIdentity : m = m
|
||||
varIdentity = Refl
|
||||
|
||||
If a proposition/equality type is not definitionally equal but is still true
|
||||
then it is *propositionally equal*. In this case we may still be able to prove
|
||||
it but some steps in the proof may require us to add something into the terms
|
||||
or at least to take some sideways steps to get to a proof.
|
||||
|
||||
Especially when working with equalities containing variable terms (inside
|
||||
functions) it can be hard to know which equality types are definitionally equal,
|
||||
in this example ``plusReducesL`` is *definitionally equal* but ``plusReducesR`` is
|
||||
not (although it is *propositionally equal*). The only difference between
|
||||
them is the order of the operands.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesL : (n:Nat) -> plus Z n = n
|
||||
plusReducesL n = Refl
|
||||
|
||||
plusReducesR : (n:Nat) -> plus n Z = n
|
||||
plusReducesR n = Refl
|
||||
|
||||
Checking ``plusReducesR`` gives the following error:
|
||||
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Proofs.idr:21:18--23:1:While processing right hand side of Main.plusReducesR at Proofs.idr:21:1--23:1:
|
||||
Can't solve constraint between:
|
||||
plus n Z
|
||||
and
|
||||
n
|
||||
|
||||
So why is ``Refl`` able to prove some equality types but not others?
|
||||
|
||||
The first answer is that ``plus`` is defined by recursion on its first
|
||||
argument. So, when the first argument is ``Z``, it reduces, but not when the
|
||||
second argument is ``Z``.
|
||||
|
||||
If an equality type can be proved/constructed by using ``Refl`` alone it is known
|
||||
as a *definitional equality*. In order to be definitionally equal both sides
|
||||
of the equation must normalise to the same value.
|
||||
|
||||
So when we type ``1+1`` in Idris it is immediately reduced to 2 because
|
||||
definitional equality is built in
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> 1+1
|
||||
2
|
||||
|
||||
In the following pages we discuss how to resolve propositional equalities.
|
@ -1,25 +0,0 @@
|
||||
.. _proofs-index:
|
||||
|
||||
###############
|
||||
Theorem Proving
|
||||
###############
|
||||
|
||||
A tutorial on theorem proving in Idris 2.
|
||||
|
||||
.. note::
|
||||
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
definitional
|
||||
pluscomm
|
||||
inductive
|
||||
patterns
|
||||
propositional
|
@ -1,102 +0,0 @@
|
||||
.. _sect-inductive:
|
||||
|
||||
****************
|
||||
Inductive Proofs
|
||||
****************
|
||||
|
||||
Before embarking on proving ``plus_commutes`` in Idris itself, let us
|
||||
consider the overall structure of a proof of some property of natural
|
||||
numbers. Recall that they are defined recursively, as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
A *total* function over natural numbers must both terminate, and cover
|
||||
all possible inputs. Idris checks functions for totality by checking that
|
||||
all inputs are covered, and that all recursive calls are on
|
||||
*structurally smaller* values (so recursion will always reach a base
|
||||
case). Recalling ``plus``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z m = m
|
||||
plus (S k) m = S (plus k m)
|
||||
|
||||
This is total because it covers all possible inputs (the first argument
|
||||
can only be ``Z`` or ``S k`` for some ``k``, and the second argument
|
||||
``m`` covers all possible ``Nat``) and in the recursive call, ``k``
|
||||
is structurally smaller than ``S k`` so the first argument will always
|
||||
reach the base case ``Z`` in any sequence of recursive calls.
|
||||
|
||||
In some sense, this resembles a mathematical proof by induction (and
|
||||
this is no coincidence!). For some property ``P`` of a natural number
|
||||
``x``, we can show that ``P`` holds for all ``x`` if:
|
||||
|
||||
- ``P`` holds for zero (the base case).
|
||||
|
||||
- Assuming that ``P`` holds for ``k``, we can show ``P`` also holds for
|
||||
``S k`` (the inductive step).
|
||||
|
||||
In ``plus``, the property we are trying to show is somewhat trivial (for
|
||||
all natural numbers ``x``, there is a ``Nat`` which need not have any
|
||||
relation to ``x``). However, it still takes the form of a base case and
|
||||
an inductive step. In the base case, we show that there is a ``Nat``
|
||||
arising from ``plus n m`` when ``n = Z``, and in the inductive step we
|
||||
show that there is a ``Nat`` arising when ``n = S k`` and we know we can
|
||||
get a ``Nat`` inductively from ``plus k m``. We could even write a
|
||||
function capturing all such inductive definitions:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
nat_induction :
|
||||
(prop : Nat -> Type) -> -- Property to show
|
||||
(prop Z) -> -- Base case
|
||||
((k : Nat) -> prop k -> prop (S k)) -> -- Inductive step
|
||||
(x : Nat) -> -- Show for all x
|
||||
prop x
|
||||
nat_induction prop p_Z p_S Z = p_Z
|
||||
nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k)
|
||||
|
||||
Using ``nat_induction``, we can implement an equivalent inductive
|
||||
version of ``plus``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_ind : Nat -> Nat -> Nat
|
||||
plus_ind n m
|
||||
= nat_induction (\x => Nat)
|
||||
m -- Base case, plus_ind Z m
|
||||
(\k, k_rec => S k_rec) -- Inductive step plus_ind (S k) m
|
||||
-- where k_rec = plus_ind k m
|
||||
n
|
||||
|
||||
To prove that ``plus n m = plus m n`` for all natural numbers ``n`` and
|
||||
``m``, we can also use induction. Either we can fix ``m`` and perform
|
||||
induction on ``n``, or vice versa. We can sketch an outline of a proof;
|
||||
performing induction on ``n``, we have:
|
||||
|
||||
- Property ``prop`` is ``\x => plus x m = plus m x``.
|
||||
|
||||
- Show that ``prop`` holds in the base case and inductive step:
|
||||
|
||||
- | Base case: ``prop Z``, i.e.
|
||||
| ``plus Z m = plus m Z``, which reduces to
|
||||
| ``m = plus m Z`` due to the definition of ``plus``.
|
||||
|
||||
- | Inductive step: Inductively, we know that ``prop k`` holds for a specific, fixed ``k``, i.e.
|
||||
| ``plus k m = plus m k`` (the induction hypothesis). Given this, show ``prop (S k)``, i.e.
|
||||
| ``plus (S k) m = plus m (S k)``, which reduces to
|
||||
| ``S (plus k m) = plus m (S k)``. From the induction hypothesis, we can rewrite this to
|
||||
| ``S (plus m k) = plus m (S k)``.
|
||||
|
||||
To complete the proof we therefore need to show that ``m = plus m Z``
|
||||
for all natural numbers ``m``, and that ``S (plus m k) = plus m (S k)``
|
||||
for all natural numbers ``m`` and ``k``. Each of these can also be
|
||||
proved by induction, this time on ``m``.
|
||||
|
||||
We are now ready to embark on a proof of commutativity of ``plus``
|
||||
formally in Idris.
|
@ -1,320 +0,0 @@
|
||||
***********************
|
||||
Pattern Matching Proofs
|
||||
***********************
|
||||
|
||||
In this section, we will provide a proof of ``plus_commutes`` directly,
|
||||
by writing a pattern matching definition. We will use interactive
|
||||
editing features extensively, since it is significantly easier to
|
||||
produce a proof when the machine can give the types of intermediate
|
||||
values and construct components of the proof itself. The commands we
|
||||
will use are summarised below. Where we refer to commands
|
||||
directly, we will use the Vim version, but these commands have a direct
|
||||
mapping to Emacs commands.
|
||||
|
||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||
|Command | Vim binding | Emacs binding | Explanation |
|
||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||
| Check type | ``\t`` | ``C-c C-t`` | Show type of identifier or hole under the cursor. |
|
||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||
| Proof search | ``\s`` | ``C-c C-a`` | Attempt to solve hole under the cursor by applying simple proof search. |
|
||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||
| Make new definition | ``\a`` | ``C-c C-s`` | Add a template definition for the type defined under the cursor. |
|
||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||
| Make lemma | ``\l`` | ``C-c C-e`` | Add a top level function with a type which solves the hole under the cursor. |
|
||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||
| Split cases | ``\c`` | ``C-c C-c`` | Create new constructor patterns for each possible case of the variable under the cursor. |
|
||||
+---------------------+-----------------+---------------+--------------------------------------------------------------------------------------------+
|
||||
|
||||
|
||||
Creating a Definition
|
||||
=====================
|
||||
|
||||
To begin, create a file ``pluscomm.idr`` containing the following type
|
||||
declaration:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||
|
||||
To create a template definition for the proof, press ``\a`` (or the
|
||||
equivalent in your editor of choice) on the line with the type
|
||||
declaration. You should see:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||
plus_commutes n m = ?plus_commutes_rhs
|
||||
|
||||
To prove this by induction on ``n``, as we sketched in Section
|
||||
:ref:`sect-inductive`, we begin with a case split on ``n`` (press
|
||||
``\c`` with the cursor over the ``n`` in the definition.) You
|
||||
should see:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||
plus_commutes Z m = ?plus_commutes_rhs_1
|
||||
plus_commutes (S k) m = ?plus_commutes_rhs_2
|
||||
|
||||
If we inspect the types of the newly created holes,
|
||||
``plus_commutes_rhs_1`` and ``plus_commutes_rhs_2``, we see that the
|
||||
type of each reflects that ``n`` has been refined to ``Z`` and ``S k``
|
||||
in each respective case. Pressing ``\t`` over
|
||||
``plus_commutes_rhs_1`` shows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
m : Nat
|
||||
-------------------------------------
|
||||
plus_commutes_rhs_1 : m = plus m Z
|
||||
|
||||
Similarly, for ``plus_commutes_rhs_2``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
m : Nat
|
||||
--------------------------------------
|
||||
plus_commutes_rhs_2 : (S (plus k m)) = (plus m (S k))
|
||||
|
||||
It is a good idea to give these slightly more meaningful names:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||
plus_commutes Z m = ?plus_commutes_Z
|
||||
plus_commutes (S k) m = ?plus_commutes_S
|
||||
|
||||
Base Case
|
||||
=========
|
||||
|
||||
We can create a separate lemma for the base case interactively, by
|
||||
pressing ``\l`` with the cursor over ``plus_commutes_Z``. This
|
||||
yields:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
|
||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||
plus_commutes Z m = plus_commutes_Z m
|
||||
plus_commutes (S k) m = ?plus_commutes_S
|
||||
|
||||
That is, the hole has been filled with a call to a top level
|
||||
function ``plus_commutes_Z``, applied to the variable in scope ``m``.
|
||||
|
||||
Unfortunately, we cannot prove this lemma directly, since ``plus`` is
|
||||
defined by matching on its *first* argument, and here ``plus m Z`` has a
|
||||
concrete value for its *second argument* (in fact, the left hand side of
|
||||
the equality has been reduced from ``plus Z m``.) Again, we can prove
|
||||
this by induction, this time on ``m``.
|
||||
|
||||
First, create a template definition with ``\d``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z m = ?plus_commutes_Z_rhs
|
||||
|
||||
Now, case split on ``m`` with ``\c``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z Z = ?plus_commutes_Z_rhs_1
|
||||
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
|
||||
|
||||
Checking the type of ``plus_commutes_Z_rhs_1`` shows the following,
|
||||
which is provable by ``Refl``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
--------------------------------------
|
||||
plus_commutes_Z_rhs_1 : Z = Z
|
||||
|
||||
For such immediate proofs, we can let write the proof automatically by
|
||||
pressing ``\s`` with the cursor over ``plus_commutes_Z_rhs_1``.
|
||||
This yields:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z Z = Refl
|
||||
plus_commutes_Z (S k) = ?plus_commutes_Z_rhs_2
|
||||
|
||||
For ``plus_commutes_Z_rhs_2``, we are not so lucky:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
-------------------------------------
|
||||
plus_commutes_Z_rhs_2 : S k = S (plus k Z)
|
||||
|
||||
Inductively, we should know that ``k = plus k Z``, and we can get access
|
||||
to this inductive hypothesis by making a recursive call on k, as
|
||||
follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z Z = Refl
|
||||
plus_commutes_Z (S k)
|
||||
= let rec = plus_commutes_Z k in
|
||||
?plus_commutes_Z_rhs_2
|
||||
|
||||
For ``plus_commutes_Z_rhs_2``, we now see:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
rec : k = plus k Z
|
||||
-------------------------------------
|
||||
plus_commutes_Z_rhs_2 : S k = S (plus k Z)
|
||||
|
||||
So we know that ``k = plus k Z``, but how do we use this to update the goal to
|
||||
``S k = S k``?
|
||||
|
||||
To achieve this, Idris provides a ``replace`` function as part of the
|
||||
prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> :t replace
|
||||
Builtin.replace : (0 rule : x = y) -> p x -> p y
|
||||
|
||||
Given a proof that ``x = y``, and a property ``p`` which holds for
|
||||
``x``, we can get a proof of the same property for ``y``, because we
|
||||
know ``x`` and ``y`` must be the same. Note the multiplicity on ``rule``
|
||||
means that it's guaranteed to be erased at run time.
|
||||
In practice, this function can be
|
||||
a little tricky to use because in general the implicit argument ``p``
|
||||
can be hard to infer by unification, so Idris provides a high level
|
||||
syntax which calculates the property and applies ``replace``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
rewrite prf in expr
|
||||
|
||||
If we have ``prf : x = y``, and the required type for ``expr`` is some
|
||||
property of ``x``, the ``rewrite ... in`` syntax will search for all
|
||||
occurrences of ``x``
|
||||
in the required type of ``expr`` and replace them with ``y``. We want
|
||||
to replace ``plus k Z`` with ``k``, so we need to apply our rule
|
||||
``rec`` in reverse, which we can do using ``sym`` from the Prelude
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> :t sym
|
||||
Builtin.sym : (0 rule : x = y) -> y = x
|
||||
|
||||
Concretely, in our example, we can say:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z (S k)
|
||||
= let rec = plus_commutes_Z k in
|
||||
rewrite sym rec in ?plus_commutes_Z_rhs_2
|
||||
|
||||
Checking the type of ``plus_commutes_Z_rhs_2`` now gives:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
rec : k = plus k Z
|
||||
-------------------------------------
|
||||
plus_commutes_Z_rhs_2 : S k = S k
|
||||
|
||||
Using the rewrite rule ``rec``, the goal type has been updated with ``plus k Z``
|
||||
replaced by ``k``.
|
||||
|
||||
We can use proof search (``\s``) to complete the proof, giving:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_Z : (m : Nat) -> m = plus m Z
|
||||
plus_commutes_Z Z = Refl
|
||||
plus_commutes_Z (S k)
|
||||
= let rec = plus_commutes_Z k in
|
||||
rewrite sym rec in Refl
|
||||
|
||||
The base case of ``plus_commutes`` is now complete.
|
||||
|
||||
Inductive Step
|
||||
==============
|
||||
|
||||
Our main theorem, ``plus_commutes`` should currently be in the following
|
||||
state:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||
plus_commutes Z m = plus_commutes_Z m
|
||||
plus_commutes (S k) m = ?plus_commutes_S
|
||||
|
||||
Looking again at the type of ``plus_commutes_S``, we have:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
m : Nat
|
||||
-------------------------------------
|
||||
plus_commutes_S : S (plus k m) = plus m (S k)
|
||||
|
||||
Conveniently, by induction we can immediately tell that
|
||||
``plus k m = plus m k``, so let us rewrite directly by making a
|
||||
recursive call to ``plus_commutes``. We add this directly, by hand, as
|
||||
follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
|
||||
plus_commutes Z m = plus_commutes_Z
|
||||
plus_commutes (S k) m = rewrite plus_commutes k m in ?plus_commutes_S
|
||||
|
||||
Checking the type of ``plus_commutes_S`` now gives:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
k : Nat
|
||||
m : Nat
|
||||
-------------------------------------
|
||||
plus_commutes_S : S (plus m k) = plus m (S k)
|
||||
|
||||
The good news is that ``m`` and ``k`` now appear in the correct order.
|
||||
However, we still have to show that the successor symbol ``S`` can be
|
||||
moved to the front in the right hand side of this equality. This
|
||||
remaining lemma takes a similar form to the ``plus_commutes_Z``; we
|
||||
begin by making a new top level lemma with ``\l``. This gives:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
|
||||
|
||||
Again, we make a template definition with ``\a``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
|
||||
plus_commutes_S k m = ?plus_commutes_S_rhs
|
||||
|
||||
Like ``plus_commutes_Z``, we can define this by induction over ``m``, since
|
||||
``plus`` is defined by matching on its first argument. The complete definition
|
||||
is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
total
|
||||
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
|
||||
plus_commutes_S k Z = Refl
|
||||
plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
|
||||
|
||||
All holes have now been solved.
|
||||
|
||||
The ``total`` annotation means that we require the final function to
|
||||
pass the totality checker; i.e. it will terminate on all possible
|
||||
well-typed inputs. This is important for proofs, since it provides a
|
||||
guarantee that the proof is valid in *all* cases, not just those for
|
||||
which it happens to be well-defined.
|
||||
|
||||
Now that ``plus_commutes`` has a ``total`` annotation, we have completed the
|
||||
proof of commutativity of addition on natural numbers.
|
@ -1,185 +0,0 @@
|
||||
********************************************
|
||||
Running example: Addition of Natural Numbers
|
||||
********************************************
|
||||
|
||||
Throughout this tutorial, we will be working with the following
|
||||
function, defined in the Idris prelude, which defines addition on
|
||||
natural numbers:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z m = m
|
||||
plus (S k) m = S (plus k m)
|
||||
|
||||
It is defined by the above equations, meaning that we have for free the
|
||||
properties that adding ``m`` to zero always results in ``m``, and that
|
||||
adding ``m`` to any non-zero number ``S k`` always results in
|
||||
``S (plus k m)``. We can see this by evaluation at the Idris REPL (i.e.
|
||||
the prompt, the read-eval-print loop):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> \m => plus Z m
|
||||
\m => m
|
||||
|
||||
Idris> \k,m => plus (S k) m
|
||||
\k => \m => S (plus k m)
|
||||
|
||||
Note that unlike many other language REPLs, the Idris REPL performs
|
||||
evaluation on *open* terms, meaning that it can reduce terms which
|
||||
appear inside lambda bindings, like those above. Therefore, we can
|
||||
introduce unknowns ``k`` and ``m`` as lambda bindings and see how
|
||||
``plus`` reduces.
|
||||
|
||||
The ``plus`` function has a number of other useful properties, for
|
||||
example:
|
||||
|
||||
- It is *commutative*, that is for all ``Nat`` inputs ``n`` and ``m``,
|
||||
we know that ``plus n m = plus m n``.
|
||||
|
||||
- It is *associative*, that is for all ``Nat`` inputs ``n``, ``m`` and
|
||||
``p``, we know that ``plus n (plus m p) = plus (plus m n) p``.
|
||||
|
||||
We can use these properties in an Idris program, but in order to do so
|
||||
we must *prove* them.
|
||||
|
||||
Equality Proofs
|
||||
===============
|
||||
|
||||
Idris defines a propositional equality type as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Equal : a -> b -> Type where
|
||||
Refl : Equal x x
|
||||
|
||||
As syntactic sugar, ``Equal x y`` can be written as ``x = y``.
|
||||
|
||||
It is *propositional* equality, where the type states that any two
|
||||
values in different types ``a`` and ``b`` may be proposed to be equal.
|
||||
There is only one way to *prove* equality, however, which is by
|
||||
reflexivity (``Refl``).
|
||||
|
||||
We have a *type* for propositional equality here, and correspondingly a
|
||||
*program* inhabiting an instance of this type can be seen as a proof of
|
||||
the corresponding proposition [1]_. So, trivially, we can prove that
|
||||
``4`` equals ``4``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
four_eq : 4 = 4
|
||||
four_eq = Refl
|
||||
|
||||
However, trying to prove that ``4 = 5`` results in failure:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
four_eq_five : 4 = 5
|
||||
four_eq_five = Refl
|
||||
|
||||
The type ``4 = 5`` is a perfectly valid type, but is uninhabited, so
|
||||
when trying to type check this definition, Idris gives the following
|
||||
error:
|
||||
|
||||
::
|
||||
|
||||
When unifying 4 = 4 and (fromInteger 4) = (fromInteger 5)
|
||||
Mismatch between:
|
||||
4
|
||||
and
|
||||
5
|
||||
|
||||
Type checking equality proofs
|
||||
-----------------------------
|
||||
|
||||
An important step in type checking Idris programs is *unification*,
|
||||
which attempts to resolve implicit arguments such as the implicit
|
||||
argument ``x`` in ``Refl``. As far as our understanding of type checking
|
||||
proofs is concerned, it suffices to know that unifying two terms
|
||||
involves reducing both to normal form then trying to find an assignment
|
||||
to implicit arguments which will make those normal forms equal.
|
||||
|
||||
When type checking ``Refl``, Idris requires that the type is of the form
|
||||
``x = x``, as we see from the type of ``Refl``. In the case of
|
||||
``four_eq_five``, Idris will try to unify the expected type ``4 = 5``
|
||||
with the type of ``Refl``, ``x = x``, notice that a solution requires
|
||||
that ``x`` be both ``4`` and ``5``, and therefore fail.
|
||||
|
||||
Since type checking involves reduction to normal form, we can write the
|
||||
following equalities directly:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
twoplustwo_eq_four : 2 + 2 = 4
|
||||
twoplustwo_eq_four = Refl
|
||||
|
||||
plus_reduces_Z : (m : Nat) -> plus Z m = m
|
||||
plus_reduces_Z m = Refl
|
||||
|
||||
plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
|
||||
plus_reduces_Sk k m = Refl
|
||||
|
||||
Heterogeneous Equality
|
||||
======================
|
||||
|
||||
Equality in Idris is *heterogeneous*, meaning that we can even propose
|
||||
equalities between values in different types:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
idris_not_php : Z = "Z"
|
||||
|
||||
The type ``Z = "Z"`` is uninhabited, and one might wonder why it is useful to
|
||||
be able to propose equalities between values in different types. However, with
|
||||
dependent types, such equalities can arise naturally. For example, if two
|
||||
vectors are equal, their lengths must be equal:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) ->
|
||||
(xs = ys) -> n = m
|
||||
|
||||
In the above declaration, ``xs`` and ``ys`` have different types because
|
||||
their lengths are different, but we would still like to draw a
|
||||
conclusion about the lengths if they happen to be equal. We can define
|
||||
``vect_eq_length`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vect_eq_length xs xs Refl = Refl
|
||||
|
||||
By matching on ``Refl`` for the third argument, we know that the only
|
||||
valid value for ``ys`` is ``xs``, because they must be equal, and
|
||||
therefore their types must be equal, so the lengths must be equal.
|
||||
|
||||
Alternatively, we can put an underscore for the second ``xs``, since
|
||||
there is only one value which will type check:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vect_eq_length xs _ Refl = Refl
|
||||
|
||||
Properties of ``plus``
|
||||
======================
|
||||
|
||||
Using the ``(=)`` type, we can now state the properties of ``plus``
|
||||
given above as Idris type declarations:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plus_commutes : (n, m : Nat) -> plus n m = plus m n
|
||||
plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p
|
||||
|
||||
Both of these properties (and many others) are proved for natural number
|
||||
addition in the Idris standard library, using ``(+)`` from the ``Num``
|
||||
interface rather than using ``plus`` directly. They have the names
|
||||
``plusCommutative`` and ``plusAssociative`` respectively.
|
||||
|
||||
In the remainder of this tutorial, we will explore several different
|
||||
ways of proving ``plus_commutes`` (or, to put it another way, writing
|
||||
the function.) We will also discuss how to use such equality proofs, and
|
||||
see where the need for them arises in practice.
|
||||
|
||||
.. [1]
|
||||
This is known as the Curry-Howard correspondence.
|
@ -1,135 +0,0 @@
|
||||
This page attempts to explain some of the techniques used in Idris to prove
|
||||
propositional equalities.
|
||||
|
||||
Proving Propositional Equality
|
||||
==============================
|
||||
|
||||
We have seen that definitional equalities can be proved using ``Refl`` since they
|
||||
always normalise to values that can be compared directly.
|
||||
|
||||
However with propositional equalities we are using symbolic variables, which do
|
||||
not always normalse.
|
||||
|
||||
So to take the previous example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesR : (n : Nat) -> plus n Z = n
|
||||
|
||||
In this case ``plus n Z`` does not normalise to n. Even though both sides of
|
||||
the equality are provably equal we cannot claim ``Refl`` as a proof.
|
||||
|
||||
If the pattern match cannot match for all ``n`` then we need to
|
||||
match all possible values of ``n``. In this case
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesR : (n : Nat) -> plus n Z = n
|
||||
plusReducesR Z = Refl
|
||||
plusReducesR (S k)
|
||||
= let rec = plusReducesR k in
|
||||
rewrite sym rec in Refl
|
||||
|
||||
we can't use ``Refl`` to prove ``n = plus n 0`` for all ``n``. Instead, we call
|
||||
it for each case separately. So, in the second line for example, the type checker
|
||||
substitutes ``Z`` for ``n`` in the type being matched, and reduces the type
|
||||
accordingly.
|
||||
|
||||
Replace
|
||||
=======
|
||||
|
||||
This implements the 'indiscernability of identicals' principle, if two terms
|
||||
are equal then they have the same properties. In other words, if ``x=y``, then we
|
||||
can substitute y for x in any expression. In our proofs we can express this as:
|
||||
|
||||
if x=y
|
||||
then prop x = prop y
|
||||
|
||||
where prop is a pure function representing the property. In the examples below
|
||||
prop is an expression in some variable with a type like this: ``prop: n -> Type``
|
||||
|
||||
So if ``n`` is a natural number variable then ``prop`` could be something
|
||||
like ``\n => 2*n + 3``.
|
||||
|
||||
To use this in our proofs there is the following function in the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
||| Perform substitution in a term according to some equality.
|
||||
replace : forall x, y, prop . (0 rule : x = y) -> prop x -> prop y
|
||||
replace Refl prf = prf
|
||||
|
||||
If we supply an equality (x=y) and a proof of a property of x (``prop x``) then we get
|
||||
a proof of a property of y (``prop y``).
|
||||
So, in the following example, if we supply ``p1 x`` which is a proof that ``x=2`` and
|
||||
the equality ``x=y`` then we get a proof that ``y=2``.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
p1: Nat -> Type
|
||||
p1 n = (n=2)
|
||||
|
||||
testReplace: (x=y) -> (p1 x) -> (p1 y)
|
||||
testReplace a b = replace a b
|
||||
|
||||
Rewrite
|
||||
=======
|
||||
|
||||
In practice, ``replace`` can be
|
||||
a little tricky to use because in general the implicit argument ``prop``
|
||||
can be hard to infer for the machine, so Idris provides a high level
|
||||
syntax which calculates the property and applies ``replace``.
|
||||
|
||||
Example: again we supply ``p1`` which is a proof that ``x=2`` and the equality
|
||||
``x=y`` then we get a proof that ``y=2``.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
p1: Nat -> Type
|
||||
p1 x = (x=2)
|
||||
|
||||
testRewrite2: (x=y) -> (p1 y) -> (p1 x)
|
||||
testRewrite2 a b = rewrite a in b
|
||||
|
||||
We can think of ``rewrite`` as working in this way:
|
||||
|
||||
* Start with a equation ``x=y`` and a property ``prop : x -> Type``
|
||||
* Search for ``x`` in ``prop``
|
||||
* Replaces all occurrences of ``x`` with ``y`` in ``prop``.
|
||||
|
||||
That is, we are doing a substitution.
|
||||
|
||||
Symmetry and Transitivity
|
||||
=========================
|
||||
|
||||
In addition to 'reflexivity' equality also obeys 'symmetry' and 'transitivity'
|
||||
and these are also included in the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
||| Symmetry of propositional equality
|
||||
sym : forall x, y . (0 rule : x = y) -> y = x
|
||||
sym Refl = Refl
|
||||
|
||||
||| Transitivity of propositional equality
|
||||
trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
|
||||
trans Refl Refl = Refl
|
||||
|
||||
Heterogeneous Equality
|
||||
======================
|
||||
|
||||
Also included in the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
||| Explicit heterogeneous ("John Major") equality. Use this when Idris
|
||||
||| incorrectly chooses homogeneous equality for `(=)`.
|
||||
||| @ a the type of the left side
|
||||
||| @ b the type of the right side
|
||||
||| @ x the left side
|
||||
||| @ y the right side
|
||||
(~=~) : (x : a) -> (y : b) -> Type
|
||||
(~=~) x y = (x = y)
|
||||
|
||||
|
||||
|
@ -1,7 +0,0 @@
|
||||
.. _ref-sect-envvars:
|
||||
|
||||
*********************
|
||||
Environment Variables
|
||||
*********************
|
||||
|
||||
[TODO: Fill in the environment variables recognised by Idris 2]
|
@ -1,20 +0,0 @@
|
||||
**********************
|
||||
Idris2 Reference Guide
|
||||
**********************
|
||||
|
||||
.. note::
|
||||
|
||||
The documentation for Idris 2 has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
This is a placeholder, to get set up with readthedocs.
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
packages
|
||||
envvars
|
@ -1,106 +0,0 @@
|
||||
.. _ref-sect-packages:
|
||||
|
||||
********
|
||||
Packages
|
||||
********
|
||||
|
||||
Idris includes a simple system for building packages from a package
|
||||
description file. These files can be used with the Idris compiler to
|
||||
manage the development process of your Idris programmes and packages.
|
||||
|
||||
Package Descriptions
|
||||
====================
|
||||
|
||||
A package description includes the following:
|
||||
|
||||
+ A header, consisting of the keyword package followed by the package
|
||||
name. Package names can be any valid Idris identifier. The iPKG
|
||||
format also takes a quoted version that accepts any valid filename.
|
||||
+ Fields describing package contents, ``<field> = <value>``
|
||||
|
||||
At least one field must be the modules field, where the value is a
|
||||
comma separated list of modules. For example, a library test which
|
||||
has two modules ``Foo.idr`` and ``Bar.idr`` as source files would be
|
||||
written as follows::
|
||||
|
||||
package test
|
||||
|
||||
modules = Foo, Bar
|
||||
|
||||
Other examples of package files can be found in the ``libs`` directory
|
||||
of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
|
||||
|
||||
Metadata
|
||||
--------
|
||||
|
||||
The `iPKG` format supports additional metadata associated with the package.
|
||||
The added fields are:
|
||||
|
||||
+ ``brief = "<text>"``, a string literal containing a brief description
|
||||
of the package.
|
||||
|
||||
+ ``version = "<text>""``, a version string to associate with the package.
|
||||
|
||||
+ ``readme = "<file>""``, location of the README file.
|
||||
|
||||
+ ``license = "<text>"``, a string description of the licensing
|
||||
information.
|
||||
|
||||
+ ``authors = "<text>"``, the author information.
|
||||
|
||||
+ ``maintainers = "<text>"``, Maintainer information.
|
||||
|
||||
+ ``homepage = "<url>"``, the website associated with the package.
|
||||
|
||||
+ ``sourceloc = "<url>"``, the location of the DVCS where the source
|
||||
can be found.
|
||||
|
||||
+ ``bugtracker = "<url>"``, the location of the project's bug tracker.
|
||||
|
||||
|
||||
Common Fields
|
||||
-------------
|
||||
|
||||
Other common fields which may be present in an ``ipkg`` file are:
|
||||
|
||||
+ ``executable = <output>``, which takes the name of the executable
|
||||
file to generate. Executable names can be any valid Idris
|
||||
identifier. the iPKG format also takes a quoted version that accepts
|
||||
any valid filename.
|
||||
|
||||
Executables are placed in ``build/exec``, relative to the top level
|
||||
source directory.
|
||||
|
||||
+ ``main = <module>``, which takes the name of the main module, and
|
||||
must be present if the executable field is present.
|
||||
|
||||
+ ``opts = "<idris options>"``, which allows options to be passed to
|
||||
Idris.
|
||||
|
||||
+ ``depends = <pkg name> (',' <pkg name>)+``, a comma separated list of
|
||||
package names that the Idris package requires.
|
||||
|
||||
|
||||
Comments
|
||||
---------
|
||||
|
||||
Package files support comments using the standard Idris singleline ``--`` and multiline ``{- -}`` format.
|
||||
|
||||
Using Package files
|
||||
===================
|
||||
|
||||
Given an Idris package file ``test.ipkg`` it can be used with the Idris compiler as follows:
|
||||
|
||||
+ ``idris2 --build test.ipkg`` will build all modules in the package
|
||||
|
||||
+ ``idris2 --install test.ipkg`` will install the package, making it
|
||||
accessible by other Idris libraries and programs. Note that this doesn't
|
||||
install any executables, just library modules.
|
||||
|
||||
+ ``idris2 --clean test.ipkg`` will clean the intermediate build files.
|
||||
|
||||
Once the test package has been installed, the command line option
|
||||
``--package test`` makes it accessible (abbreviated to ``-p test``).
|
||||
For example::
|
||||
|
||||
idris -p test Main.idr
|
@ -1,59 +0,0 @@
|
||||
.. _sect-concs:
|
||||
|
||||
***************
|
||||
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.
|
||||
|
||||
* The IRC channel ``#idris``, on
|
||||
`webchat.freenode.net <https://webchat.freenode.net/>`__.
|
||||
|
||||
* The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further
|
||||
user provided information, in particular:
|
||||
|
||||
* https://github.com/idris-lang/Idris-dev/wiki/Manual
|
||||
|
||||
* https://github.com/idris-lang/Idris-dev/wiki/Language-Features
|
||||
|
||||
* Examining the prelude and exploring the ``samples`` in the
|
||||
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.
|
||||
|
||||
* Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_). Although these mostly
|
||||
describe older versions of Idris.
|
||||
|
||||
.. [#BradyHammond2012] 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
|
||||
|
||||
.. [#Brady] 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
|
||||
|
||||
.. [#BradyHammond2010] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
|
||||
inefficient engine: using partial evaluation to improve
|
||||
domain-specific language implementation. In Proceedings of the
|
||||
15th ACM SIGPLAN international conference on Functional
|
||||
programming (ICFP '10). ACM, New York, NY, USA,
|
||||
297-308. DOI=10.1145/1863543.1863587
|
||||
http://doi.acm.org/10.1145/1863543.1863587
|
@ -1,40 +0,0 @@
|
||||
.. _tutorial-index:
|
||||
|
||||
#########################
|
||||
A Crash Course in Idris 2
|
||||
#########################
|
||||
|
||||
This is a crash course in Idris 2 (sort of a tutorial, but rather less
|
||||
gentle I'm afraid!).
|
||||
It provides a brief introduction to programming in the Idris Language.
|
||||
It covers the core language features, assuming some experience with an
|
||||
existing functional programming language such as Haskell or OCaml.
|
||||
|
||||
This has been revised and updated from the Idris 1 tutorial. For details of
|
||||
changes since Idris 1, see :ref:`updates-index`.
|
||||
|
||||
.. note::
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
introduction
|
||||
starting
|
||||
typesfuns
|
||||
interfaces
|
||||
modules
|
||||
multiplicities
|
||||
packages
|
||||
interp
|
||||
views
|
||||
theorems
|
||||
interactive
|
||||
miscellany
|
||||
conclusions
|
@ -1,256 +0,0 @@
|
||||
.. _sect-interactive:
|
||||
|
||||
*******************
|
||||
Interactive Editing
|
||||
*******************
|
||||
|
||||
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 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 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
|
||||
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/edwinb/idris2-vim>`_. An interactive mode
|
||||
for `Emacs <https://github.com/idris-hackers/idris-mode>`_ is also
|
||||
available (though not yet updated for Idris 2).
|
||||
|
||||
Editing at the REPL
|
||||
===================
|
||||
|
||||
The REPL provides a number of commands, which we will describe
|
||||
shortly, which generate new program fragments based on the currently
|
||||
loaded module. These take the general form:
|
||||
|
||||
::
|
||||
|
||||
:command [line number] [name]
|
||||
|
||||
That is, each command acts on a specific source line, at a specific
|
||||
name, and outputs a new program fragment. Each command has an
|
||||
alternative form, which *updates* the source file in-place:
|
||||
|
||||
::
|
||||
|
||||
:command! [line number] [name]
|
||||
|
||||
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:
|
||||
|
||||
::
|
||||
|
||||
$ 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.
|
||||
|
||||
Editing Commands
|
||||
================
|
||||
|
||||
:addclause
|
||||
----------
|
||||
|
||||
The ``:addclause n f`` command, abbreviated ``:ac n f``, creates a
|
||||
template definition for the function named ``f`` declared on line
|
||||
``n``. For example, if the code beginning on line 94 contains:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vzipWith : (a -> b -> c) ->
|
||||
Vect n a -> Vect n b -> Vect n c
|
||||
|
||||
then ``:ac 94 vzipWith`` will give:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vzipWith f xs ys = ?vzipWith_rhs
|
||||
|
||||
The names are chosen according to hints which may be given by a
|
||||
programmer, and then made unique by the machine by adding a digit if
|
||||
necessary. Hints can be given as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%name Vect xs, ys, zs, ws
|
||||
|
||||
This declares that any names generated for types in the ``Vect`` family
|
||||
should be chosen in the order ``xs``, ``ys``, ``zs``, ``ws``.
|
||||
|
||||
:casesplit
|
||||
----------
|
||||
|
||||
The ``:casesplit n x`` command, abbreviated ``:cs n x``, splits the
|
||||
pattern variable ``x`` on line ``n`` into the various pattern forms it
|
||||
may take, removing any cases which are impossible due to unification
|
||||
errors. For example, if the code beginning on line 94 is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vzipWith : (a -> b -> c) ->
|
||||
Vect n a -> Vect n b -> Vect n c
|
||||
vzipWith f xs ys = ?vzipWith_rhs
|
||||
|
||||
then ``:cs 96 xs`` will give:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vzipWith f [] ys = ?vzipWith_rhs_1
|
||||
vzipWith f (x :: xs) ys = ?vzipWith_rhs_2
|
||||
|
||||
That is, the pattern variable ``xs`` has been split into the two
|
||||
possible cases ``[]`` and ``x :: xs``. Again, the names are chosen
|
||||
according to the same heuristic. If we update the file (using
|
||||
``:cs!``) then case split on ``ys`` on the same line, we get:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vzipWith f [] [] = ?vzipWith_rhs_3
|
||||
|
||||
That is, the pattern variable ``ys`` has been split into one case
|
||||
``[]``, Idris having noticed that the other possible case ``y ::
|
||||
ys`` would lead to a unification error.
|
||||
|
||||
:addmissing
|
||||
-----------
|
||||
|
||||
The ``:addmissing n f`` command, abbreviated ``:am n f``, adds the
|
||||
clauses which are required to make the function ``f`` on line ``n``
|
||||
cover all inputs. For example, if the code beginning on line 94 is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vzipWith : (a -> b -> c) ->
|
||||
Vect n a -> Vect n b -> Vect n c
|
||||
vzipWith f [] [] = ?vzipWith_rhs_1
|
||||
|
||||
then ``:am 96 vzipWith`` gives:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
|
||||
|
||||
That is, it notices that there are no cases for empty vectors,
|
||||
generates the required clauses, and eliminates the clauses which would
|
||||
lead to unification errors.
|
||||
|
||||
:proofsearch
|
||||
------------
|
||||
|
||||
The ``:proofsearch n f`` command, abbreviated ``:ps n f``, attempts to
|
||||
find a value for the hole ``f`` on line ``n`` by proof search,
|
||||
trying values of local variables, recursive calls and constructors of
|
||||
the required family. Optionally, it can take a list of *hints*, which
|
||||
are functions it can try applying to solve the hole. For
|
||||
example, if the code beginning on line 94 is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vzipWith : (a -> b -> c) ->
|
||||
Vect n a -> Vect n b -> Vect n c
|
||||
vzipWith f [] [] = ?vzipWith_rhs_1
|
||||
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
|
||||
|
||||
then ``:ps 96 vzipWith_rhs_1`` will give
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
[]
|
||||
|
||||
This works because it is searching for a ``Vect`` of length 0, of
|
||||
which the empty vector is the only possibility. Similarly, and perhaps
|
||||
surprisingly, there is only one possibility if we try to solve ``:ps
|
||||
97 vzipWith_rhs_2``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
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
|
||||
must have type ``c`` and the only way to get this is to apply ``f`` to
|
||||
``x`` and ``y``; finally, the tail of the vector can only be built
|
||||
recursively.
|
||||
|
||||
:makewith
|
||||
---------
|
||||
|
||||
The ``:makewith n f`` command, abbreviated ``:mw n f``, adds a
|
||||
``with`` to a pattern clause. For example, recall ``parity``. If line
|
||||
10 is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity (S k) = ?parity_rhs
|
||||
|
||||
then ``:mw 10 parity`` will give:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity (S k) with (_)
|
||||
parity (S k) | with_pat = ?parity_rhs
|
||||
|
||||
If we then fill in the placeholder ``_`` with ``parity k`` and case
|
||||
split on ``with_pat`` using ``:cs 11 with_pat`` we get the following
|
||||
patterns:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity (S (plus n n)) | even = ?parity_rhs_1
|
||||
parity (S (S (plus n n))) | odd = ?parity_rhs_2
|
||||
|
||||
Note that case splitting has normalised the patterns here (giving
|
||||
``plus`` rather than ``+``). In any case, we see that using
|
||||
interactive editing significantly simplifies the implementation of
|
||||
dependent pattern matching by showing a programmer exactly what the
|
||||
valid patterns are.
|
||||
|
||||
Interactive Editing in Vim
|
||||
==========================
|
||||
|
||||
The editor mode for Vim provides syntax highlighting, indentation and
|
||||
interactive editing support using the commands described above.
|
||||
Interactive editing is achieved using the following editor commands,
|
||||
each of which update the buffer directly:
|
||||
|
||||
- ``\a`` adds a template definition for the name declared on the
|
||||
current line (using ``:addclause``).
|
||||
|
||||
- ``\c`` case splits the variable at the cursor (using
|
||||
``:casesplit``).
|
||||
|
||||
- ``\m`` adds the missing cases for the name at the cursor (using
|
||||
``:addmissing``).
|
||||
|
||||
- ``\w`` adds a ``with`` clause (using ``:makewith``).
|
||||
|
||||
- ``\s`` invokes a proof search 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
|
||||
cursor. In the case of a hole, this displays the context
|
||||
and the expected type.
|
||||
|
||||
- ``\e`` prompts for an expression to evaluate.
|
||||
|
||||
- ``\r`` reloads and type checks the buffer.
|
||||
|
||||
Corresponding commands are also available in the Emacs mode. Support
|
||||
for other editors can be added in a relatively straightforward manner
|
||||
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>`_.
|
||||
|
@ -1,659 +0,0 @@
|
||||
.. _sect-interfaces:
|
||||
|
||||
**********
|
||||
Interfaces
|
||||
**********
|
||||
|
||||
We often want to define functions which work across several different
|
||||
data types. For example, we would like arithmetic operators to work on
|
||||
``Int``, ``Integer`` and ``Double`` at the very least. We would like
|
||||
``==`` to work on the majority of data types. We would like to be able
|
||||
to display different types in a uniform way.
|
||||
|
||||
To achieve this, we use *interfaces*, which are similar to type classes in
|
||||
Haskell or traits in Rust. To define an interface, we provide a collection of
|
||||
overloadable functions. A simple example is the ``Show``
|
||||
interface, which is defined in the prelude and provides an interface for
|
||||
converting values to ``String``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Show a where
|
||||
show : a -> String
|
||||
|
||||
This generates a function of the following type (which we call a
|
||||
*method* of the ``Show`` interface):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
show : Show a => a -> String
|
||||
|
||||
We can read this as: “under the constraint that ``a`` has an implementation
|
||||
of ``Show``, take an input ``a`` and return a ``String``.” An implementation
|
||||
of an interface is defined by giving definitions of the methods of the interface.
|
||||
For example, the ``Show`` implementation for ``Nat`` could be defined as:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Show Nat where
|
||||
show Z = "Z"
|
||||
show (S k) = "s" ++ show k
|
||||
|
||||
::
|
||||
|
||||
Main> show (S (S (S Z)))
|
||||
"sssZ" : String
|
||||
|
||||
Only one implementation of an interface can be given for a type — implementations may
|
||||
not overlap. Implementation declarations can themselves have constraints.
|
||||
To help with resolution, the arguments of an implementation must be
|
||||
constructors (either data or type constructors) or variables
|
||||
(i.e. you cannot give an implementation for a function). For
|
||||
example, to define a ``Show`` implementation for vectors, we need to know
|
||||
that there is a ``Show`` implementation for the element type, because we are
|
||||
going to use it to convert each element to a ``String``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Show a => Show (Vect n a) where
|
||||
show xs = "[" ++ show' xs ++ "]" where
|
||||
show' : forall n . Vect n a -> String
|
||||
show' Nil = ""
|
||||
show' (x :: Nil) = show x
|
||||
show' (x :: xs) = show x ++ ", " ++ show' xs
|
||||
|
||||
Note that we need the explicit ``forall n .`` in the ``show'`` function
|
||||
because otherwise the ``n`` is already in scope, and fixed to the value of
|
||||
the top level ``n``.
|
||||
|
||||
Default Definitions
|
||||
===================
|
||||
|
||||
The Prelude defines an ``Eq`` interface which provides methods for
|
||||
comparing values for equality or inequality, with implementations for all of
|
||||
the built-in types:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Eq a where
|
||||
(==) : a -> a -> Bool
|
||||
(/=) : a -> a -> Bool
|
||||
|
||||
To declare an implementation for a type, we have to give definitions of all
|
||||
of the methods. For example, for an implementation of ``Eq`` for ``Nat``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Eq Nat where
|
||||
Z == Z = True
|
||||
(S x) == (S y) = x == y
|
||||
Z == (S y) = False
|
||||
(S x) == Z = False
|
||||
|
||||
x /= y = not (x == y)
|
||||
|
||||
It is hard to imagine many cases where the ``/=`` method will be
|
||||
anything other than the negation of the result of applying the ``==``
|
||||
method. It is therefore convenient to give a default definition for
|
||||
each method in the interface declaration, in terms of the other method:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Eq a where
|
||||
(==) : a -> a -> Bool
|
||||
(/=) : a -> a -> Bool
|
||||
|
||||
x /= y = not (x == y)
|
||||
x == y = not (x /= y)
|
||||
|
||||
A minimal complete implementation of ``Eq`` requires either
|
||||
``==`` or ``/=`` to be defined, but does not require both. If a method
|
||||
definition is missing, and there is a default definition for it, then
|
||||
the default is used instead.
|
||||
|
||||
Extending Interfaces
|
||||
====================
|
||||
|
||||
Interfaces can also be extended. A logical next step from an equality
|
||||
relation ``Eq`` is to define an ordering relation ``Ord``. We can
|
||||
define an ``Ord`` interface which inherits methods from ``Eq`` as well as
|
||||
defining some of its own:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Ordering = LT | EQ | GT
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Eq a => Ord a where
|
||||
compare : a -> a -> Ordering
|
||||
|
||||
(<) : a -> a -> Bool
|
||||
(>) : a -> a -> Bool
|
||||
(<=) : a -> a -> Bool
|
||||
(>=) : a -> a -> Bool
|
||||
max : a -> a -> a
|
||||
min : a -> a -> a
|
||||
|
||||
The ``Ord`` interface allows us to compare two values and determine their
|
||||
ordering. Only the ``compare`` method is required; every other method
|
||||
has a default definition. Using this we can write functions such as
|
||||
``sort``, a function which sorts a list into increasing order,
|
||||
provided that the element type of the list is in the ``Ord`` interface. We
|
||||
give the constraints on the type variables left of the fat arrow
|
||||
``=>``, and the function type to the right of the fat arrow:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sort : Ord a => List a -> List a
|
||||
|
||||
Functions, interfaces and implementations can have multiple
|
||||
constraints. Multiple constraints are written in brackets in a comma
|
||||
separated list, for example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sortAndShow : (Ord a, Show a) => List a -> String
|
||||
sortAndShow xs = show (sort xs)
|
||||
|
||||
Constraints are, like types, first class objects in the language. You can
|
||||
see this at the REPL:
|
||||
|
||||
::
|
||||
|
||||
Main> :t Ord
|
||||
Prelude.Ord : Type -> Type
|
||||
|
||||
So, ``(Ord a, Show a)`` is an ordinary pair of ``Types``, with two constraints
|
||||
as the first and second element of the pair.
|
||||
|
||||
Note: Interfaces and ``mutual`` blocks
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
Idris is strictly "define before use", except in ``mutual`` blocks.
|
||||
In a ``mutual`` block, Idris elaborates in two passes: types on the first
|
||||
pass and definitions on the second. When the mutual block contains an
|
||||
interface declaration, it elaborates the interface header but none of the
|
||||
method types on the first pass, and elaborates the method types and any
|
||||
default definitions on the second pass.
|
||||
|
||||
Functors and Applicatives
|
||||
=========================
|
||||
|
||||
So far, we have seen single parameter interfaces, where the parameter
|
||||
is of type ``Type``. In general, there can be any number of parameters
|
||||
(even zero), and the parameters can have *any* type. If the type
|
||||
of the parameter is not ``Type``, we need to give an explicit type
|
||||
declaration. For example, the ``Functor`` interface is defined in the
|
||||
prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Functor (f : Type -> Type) where
|
||||
map : (m : a -> b) -> f a -> f b
|
||||
|
||||
A functor allows a function to be applied across a structure, for
|
||||
example to apply a function to every element in a ``List``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Functor List where
|
||||
map f [] = []
|
||||
map f (x::xs) = f x :: map f xs
|
||||
|
||||
::
|
||||
|
||||
Idris> map (*2) [1..10]
|
||||
[2, 4, 6, 8, 10, 12, 14, 16, 18, 20] : List Integer
|
||||
|
||||
Having defined ``Functor``, we can define ``Applicative`` which
|
||||
abstracts the notion of function application:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
infixl 2 <*>
|
||||
|
||||
interface Functor f => Applicative (f : Type -> Type) where
|
||||
pure : a -> f a
|
||||
(<*>) : f (a -> b) -> f a -> f b
|
||||
|
||||
.. _monadsdo:
|
||||
|
||||
Monads and ``do``-notation
|
||||
==========================
|
||||
|
||||
The ``Monad`` interface allows us to encapsulate binding and computation,
|
||||
and is the basis of ``do``-notation introduced in Section
|
||||
:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
|
||||
defined as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Applicative m => Monad (m : Type -> Type) where
|
||||
(>>=) : m a -> (a -> m b) -> m b
|
||||
|
||||
Inside a ``do`` block, the following syntactic transformations are
|
||||
applied:
|
||||
|
||||
- ``x <- v; e`` becomes ``v >>= (\x => e)``
|
||||
|
||||
- ``v; e`` becomes ``v >>= (\_ => e)``
|
||||
|
||||
- ``let x = v; e`` becomes ``let x = v in e``
|
||||
|
||||
``IO`` has an implementation of ``Monad``, defined using primitive functions.
|
||||
We can also define an implementation for ``Maybe``, as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Monad Maybe where
|
||||
Nothing >>= k = Nothing
|
||||
(Just x) >>= k = k x
|
||||
|
||||
Using this we can, for example, define a function which adds two
|
||||
``Maybe Int``, using the monad to encapsulate the error handling:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
m_add : Maybe Int -> Maybe Int -> Maybe Int
|
||||
m_add x y = do x' <- x -- Extract value from x
|
||||
y' <- y -- Extract value from y
|
||||
pure (x' + y') -- Add them
|
||||
|
||||
This function will extract the values from ``x`` and ``y``, if they
|
||||
are both available, or return ``Nothing`` if one or both are not ("fail fast"). Managing the
|
||||
``Nothing`` cases is achieved by the ``>>=`` operator, hidden by the
|
||||
``do`` notation.
|
||||
|
||||
::
|
||||
|
||||
Main> m_add (Just 82) (Just 22)
|
||||
Just 94
|
||||
Main> m_add (Just 82) Nothing
|
||||
Nothing
|
||||
|
||||
Pattern Matching Bind
|
||||
~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
Sometimes we want to pattern match immediately on the result of a function
|
||||
in ``do`` notation. For example, let's say we have a function ``readNumber``
|
||||
which reads a number from the console, returning a value of the form
|
||||
``Just x`` if the number is valid, or ``Nothing`` otherwise:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
readNumber : IO (Maybe Nat)
|
||||
readNumber = do
|
||||
input <- getLine
|
||||
if all isDigit (unpack input)
|
||||
then pure (Just (cast input))
|
||||
else pure Nothing
|
||||
|
||||
If we then use it to write a function to read two numbers, returning
|
||||
``Nothing`` if neither are valid, then we would like to pattern match
|
||||
on the result of ``readNumber``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
readNumbers : IO (Maybe (Nat, Nat))
|
||||
readNumbers =
|
||||
do x <- readNumber
|
||||
case x of
|
||||
Nothing => pure Nothing
|
||||
Just x_ok => do y <- readNumber
|
||||
case y of
|
||||
Nothing => pure Nothing
|
||||
Just y_ok => pure (Just (x_ok, y_ok))
|
||||
|
||||
If there's a lot of error handling, this could get deeply nested very quickly!
|
||||
So instead, we can combine the bind and the pattern match in one line. For example,
|
||||
we could try pattern matching on values of the form ``Just x_ok``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
readNumbers : IO (Maybe (Nat, Nat))
|
||||
readNumbers
|
||||
= do Just x_ok <- readNumber
|
||||
Just y_ok <- readNumber
|
||||
pure (Just (x_ok, y_ok))
|
||||
|
||||
There is still a problem, however, because we've now omitted the case for
|
||||
``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
|
||||
case back as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
readNumbers : IO (Maybe (Nat, Nat))
|
||||
readNumbers
|
||||
= do Just x_ok <- readNumber
|
||||
| Nothing => pure Nothing
|
||||
Just y_ok <- readNumber
|
||||
| Nothing => pure Nothing
|
||||
pure (Just (x_ok, y_ok))
|
||||
|
||||
The effect of this version of ``readNumbers`` is identical to the first (in
|
||||
fact, it is syntactic sugar for it and directly translated back into that form).
|
||||
The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
|
||||
the preferred binding - if this matches, execution will continue with the rest
|
||||
of the ``do`` block. The second part gives the alternative bindings, of which
|
||||
there may be more than one.
|
||||
|
||||
``!``-notation
|
||||
~~~~~~~~~~~~~~
|
||||
|
||||
In many cases, using ``do``-notation can make programs unnecessarily
|
||||
verbose, particularly in cases such as ``m_add`` above where the value
|
||||
bound is used once, immediately. In these cases, we can use a
|
||||
shorthand version, as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
m_add : Maybe Int -> Maybe Int -> Maybe Int
|
||||
m_add x y = pure (!x + !y)
|
||||
|
||||
The notation ``!expr`` means that the expression ``expr`` should be
|
||||
evaluated and then implicitly bound. Conceptually, we can think of
|
||||
``!`` as being a prefix function with the following type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
(!) : m a -> a
|
||||
|
||||
Note, however, that it is not really a function, merely syntax! In
|
||||
practice, a subexpression ``!expr`` will lift ``expr`` as high as
|
||||
possible within its current scope, bind it to a fresh name ``x``, and
|
||||
replace ``!expr`` with ``x``. Expressions are lifted depth first, left
|
||||
to right. In practice, ``!``-notation allows us to program in a more
|
||||
direct style, while still giving a notational clue as to which
|
||||
expressions are monadic.
|
||||
|
||||
For example, the expression:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
let y = 94 in f !(g !(print y) !x)
|
||||
|
||||
is lifted to:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
let y = 94 in do y' <- print y
|
||||
x' <- x
|
||||
g' <- g y' x'
|
||||
f g'
|
||||
|
||||
Monad comprehensions
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
The list comprehension notation we saw in Section
|
||||
:ref:`sect-more-expr` is more general, and applies to anything which
|
||||
has an implementation of both ``Monad`` and ``Alternative``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Applicative f => Alternative (f : Type -> Type) where
|
||||
empty : f a
|
||||
(<|>) : f a -> f a -> f a
|
||||
|
||||
In general, a comprehension takes the form ``[ exp | qual1, qual2, …,
|
||||
qualn ]`` where ``quali`` can be one of:
|
||||
|
||||
- A generator ``x <- e``
|
||||
|
||||
- A *guard*, which is an expression of type ``Bool``
|
||||
|
||||
- A let binding ``let x = e``
|
||||
|
||||
To translate a comprehension ``[exp | qual1, qual2, …, qualn]``, first
|
||||
any qualifier ``qual`` which is a *guard* is translated to ``guard
|
||||
qual``, using the following function:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
guard : Alternative f => Bool -> f ()
|
||||
|
||||
Then the comprehension is converted to ``do`` notation:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
do { qual1; qual2; ...; qualn; pure exp; }
|
||||
|
||||
Using monad comprehensions, an alternative definition for ``m_add``
|
||||
would be:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
m_add : Maybe Int -> Maybe Int -> Maybe Int
|
||||
m_add x y = [ x' + y' | x' <- x, y' <- y ]
|
||||
|
||||
Idiom brackets
|
||||
==============
|
||||
|
||||
While ``do`` notation gives an alternative meaning to sequencing,
|
||||
idioms give an alternative meaning to *application*. The notation and
|
||||
larger example in this section is inspired by Conor McBride and Ross
|
||||
Paterson’s paper “Applicative Programming with Effects” [#ConorRoss]_.
|
||||
|
||||
First, let us revisit ``m_add`` above. All it is really doing is
|
||||
applying an operator to two values extracted from ``Maybe Int``. We
|
||||
could abstract out the application:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
m_app : Maybe (a -> b) -> Maybe a -> Maybe b
|
||||
m_app (Just f) (Just a) = Just (f a)
|
||||
m_app _ _ = Nothing
|
||||
|
||||
Using this, we can write an alternative ``m_add`` which uses this
|
||||
alternative notion of function application, with explicit calls to
|
||||
``m_app``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
m_add' : Maybe Int -> Maybe Int -> Maybe Int
|
||||
m_add' x y = m_app (m_app (Just (+)) x) y
|
||||
|
||||
Rather than having to insert ``m_app`` everywhere there is an
|
||||
application, we can use idiom brackets to do the job for us.
|
||||
To do this, we can give ``Maybe`` an implementation of ``Applicative``
|
||||
as follows, where ``<*>`` is defined in the same way as ``m_app``
|
||||
above (this is defined in the Idris library):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Applicative Maybe where
|
||||
pure = Just
|
||||
|
||||
(Just f) <*> (Just a) = Just (f a)
|
||||
_ <*> _ = Nothing
|
||||
|
||||
Using ``<*>`` we can use this implementation as follows, where a function
|
||||
application ``[ f a1 …an |]`` is translated into ``pure f <*> a1 <*>
|
||||
… <*> an``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
m_add' : Maybe Int -> Maybe Int -> Maybe Int
|
||||
m_add' x y = [ x + y |]
|
||||
|
||||
An error-handling interpreter
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
Idiom notation is commonly useful when defining evaluators. McBride
|
||||
and Paterson describe such an evaluator [#ConorRoss]_, for a language similar
|
||||
to the following:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Expr = Var String -- variables
|
||||
| Val Int -- values
|
||||
| Add Expr Expr -- addition
|
||||
|
||||
Evaluation will take place relative to a context mapping variables
|
||||
(represented as ``String``\s) to ``Int`` values, and can possibly fail.
|
||||
We define a data type ``Eval`` to wrap an evaluator:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Eval : Type -> Type where
|
||||
MkEval : (List (String, Int) -> Maybe a) -> Eval a
|
||||
|
||||
Wrapping the evaluator in a data type means we will be able to provide
|
||||
implementations of interfaces for it later. We begin by defining a function to
|
||||
retrieve values from the context during evaluation:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
fetch : String -> Eval Int
|
||||
fetch x = MkEval (\e => fetchVal e) where
|
||||
fetchVal : List (String, Int) -> Maybe Int
|
||||
fetchVal [] = Nothing
|
||||
fetchVal ((v, val) :: xs) = if (x == v)
|
||||
then (Just val)
|
||||
else (fetchVal xs)
|
||||
|
||||
When defining an evaluator for the language, we will be applying functions in
|
||||
the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
|
||||
of ``Applicative``. Before ``Eval`` can have an implementation of
|
||||
``Applicative`` it is necessary for ``Eval`` to have an implementation of
|
||||
``Functor``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Functor Eval where
|
||||
map f (MkEval g) = MkEval (\e => map f (g e))
|
||||
|
||||
Applicative Eval where
|
||||
pure x = MkEval (\e => Just x)
|
||||
|
||||
(<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
|
||||
app : Maybe (a -> b) -> Maybe a -> Maybe b
|
||||
app (Just fx) (Just gx) = Just (fx gx)
|
||||
app _ _ = Nothing
|
||||
|
||||
Evaluating an expression can now make use of the idiomatic application
|
||||
to handle errors:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
eval : Expr -> Eval Int
|
||||
eval (Var x) = fetch x
|
||||
eval (Val x) = [| x |]
|
||||
eval (Add x y) = [| eval x + eval y |]
|
||||
|
||||
runEval : List (String, Int) -> Expr -> Maybe Int
|
||||
runEval env e = case eval e of
|
||||
MkEval envFn => envFn env
|
||||
|
||||
For example:
|
||||
|
||||
::
|
||||
|
||||
InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "y"))
|
||||
Just 94
|
||||
InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "z"))
|
||||
Nothing
|
||||
|
||||
Named Implementations
|
||||
=====================
|
||||
|
||||
It can be desirable to have multiple implementations of an interface for the
|
||||
same type, for example to provide alternative methods for sorting or printing
|
||||
values. To achieve this, implementations can be *named* as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
[myord] Ord Nat where
|
||||
compare Z (S n) = GT
|
||||
compare (S n) Z = LT
|
||||
compare Z Z = EQ
|
||||
compare (S x) (S y) = compare @{myord} x y
|
||||
|
||||
This declares an implementation as normal, but with an explicit name,
|
||||
``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
|
||||
``compare``, otherwise it would use the default implementation for ``Nat``. We
|
||||
can use this, for example, to sort a list of ``Nat`` in reverse.
|
||||
Given the following list:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
testList : List Nat
|
||||
testList = [3,4,1]
|
||||
|
||||
We can sort it using the default ``Ord`` implementation, by using the ``sort``
|
||||
function available with ``import Data.List``, then we can try with the named
|
||||
implementation ``myord`` as follows, at the Idris prompt:
|
||||
|
||||
::
|
||||
|
||||
Main> show (sort testList)
|
||||
"[1, 3, 4]"
|
||||
Main> show (sort @{myord} testList)
|
||||
"[4, 3, 1]"
|
||||
|
||||
Sometimes, we also need access to a named parent implementation. For example,
|
||||
the prelude defines the following ``Semigroup`` interface:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Semigroup ty where
|
||||
(<+>) : ty -> ty -> ty
|
||||
|
||||
Then it defines ``Monoid``, which extends ``Semigroup`` with a “neutral”
|
||||
value:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Semigroup ty => Monoid ty where
|
||||
neutral : ty
|
||||
|
||||
We can define two different implementations of ``Semigroup`` and
|
||||
``Monoid`` for ``Nat``, one based on addition and one on multiplication:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
[PlusNatSemi] Semigroup Nat where
|
||||
(<+>) x y = x + y
|
||||
|
||||
[MultNatSemi] Semigroup Nat where
|
||||
(<+>) x y = x * y
|
||||
|
||||
The neutral value for addition is ``0``, but the neutral value for multiplication
|
||||
is ``1``. It's important, therefore, that when we define implementations
|
||||
of ``Monoid`` they extend the correct ``Semigroup`` implementation. We can
|
||||
do this with a ``using`` clause in the implementation as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
[PlusNatMonoid] Monoid Nat using PlusNatSemi where
|
||||
neutral = 0
|
||||
|
||||
[MultNatMonoid] Monoid Nat using MultNatSemi where
|
||||
neutral = 1
|
||||
|
||||
The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should
|
||||
extend ``PlusNatSemi`` specifically.
|
||||
|
||||
Determining Parameters
|
||||
======================
|
||||
|
||||
When an interface has more than one parameter, it can help resolution if the
|
||||
parameters used to find an implementation are restricted. For example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Monad m => MonadState s (m : Type -> Type) | m where
|
||||
get : m s
|
||||
put : s -> m ()
|
||||
|
||||
In this interface, only ``m`` needs to be known to find an implementation of
|
||||
this interface, and ``s`` can then be determined from the implementation. This
|
||||
is declared with the ``| m`` after the interface declaration. We call ``m`` a
|
||||
*determining parameter* of the ``MonadState`` interface, because it is the
|
||||
parameter used to find an implementation.
|
||||
|
||||
|
||||
.. [#ConorRoss] Conor McBride and Ross Paterson. 2008. Applicative programming
|
||||
with effects. J. Funct. Program. 18, 1 (January 2008),
|
||||
1-13. DOI=10.1017/S0956796807006326
|
||||
http://dx.doi.org/10.1017/S0956796807006326
|
@ -1,292 +0,0 @@
|
||||
.. _sect-interp:
|
||||
|
||||
***********************************
|
||||
Example: The Well-Typed Interpreter
|
||||
***********************************
|
||||
|
||||
In this section, we’ll use the features we’ve seen so far to write a
|
||||
larger example, an interpreter for a simple functional programming
|
||||
language, with variables, function application, binary operators and
|
||||
an ``if...then...else`` construct. We will use the dependent type
|
||||
system to ensure that any programs which can be represented are
|
||||
well-typed.
|
||||
|
||||
Representing Languages
|
||||
======================
|
||||
|
||||
First, let us define the types in the language. We have integers,
|
||||
booleans, and functions, represented by ``Ty``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Ty = TyInt | TyBool | TyFun Ty Ty
|
||||
|
||||
We can write a function to translate these representations to a concrete
|
||||
Idris type — remember that types are first class, so can be
|
||||
calculated just like any other value:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interpTy : Ty -> Type
|
||||
interpTy TyInt = Integer
|
||||
interpTy TyBool = Bool
|
||||
interpTy (TyFun a t) = interpTy a -> interpTy t
|
||||
|
||||
We're going to define a representation of our language in such a way
|
||||
that only well-typed programs can be represented. We'll index the
|
||||
representations of expressions by their type, **and** the types of
|
||||
local variables (the context). The context can be represented using
|
||||
the ``Vect`` data type, so we'll need to import ``Data.Vect`` at the top of our
|
||||
source file:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import Data.Vect
|
||||
|
||||
Expressions are indexed by the types of the local
|
||||
variables, and the type of the expression itself:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Expr : Vect n Ty -> Ty -> Type
|
||||
|
||||
The full representation of expressions is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
|
||||
Stop : HasType FZ (t :: ctxt) t
|
||||
Pop : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
|
||||
|
||||
data Expr : Vect n Ty -> Ty -> Type where
|
||||
Var : HasType i ctxt t -> Expr ctxt t
|
||||
Val : (x : Integer) -> Expr ctxt TyInt
|
||||
Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
|
||||
App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
|
||||
Op : (interpTy a -> interpTy b -> interpTy c) ->
|
||||
Expr ctxt a -> Expr ctxt b -> Expr ctxt c
|
||||
If : Expr ctxt TyBool ->
|
||||
Lazy (Expr ctxt a) ->
|
||||
Lazy (Expr ctxt a) -> Expr ctxt a
|
||||
|
||||
The code above makes use of the ``Vect`` and ``Fin`` types from the
|
||||
base libraries. ``Fin`` is available as part of ``Data.Vect``. Throughout,
|
||||
``ctxt`` refers to the local variable context.
|
||||
|
||||
Since expressions are indexed by their type, we can read the typing
|
||||
rules of the language from the definitions of the constructors. Let us
|
||||
look at each constructor in turn.
|
||||
|
||||
We use a nameless representation for variables — they are *de Bruijn
|
||||
indexed*. Variables are represented by a proof of their membership in
|
||||
the context, ``HasType i ctxt T``, which is a proof that variable ``i``
|
||||
in context ``ctxt`` has type ``T``. This is defined as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
|
||||
Stop : HasType FZ (t :: ctxt) t
|
||||
Pop : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
|
||||
|
||||
We can treat *Stop* as a proof that the most recently defined variable
|
||||
is well-typed, and *Pop n* as a proof that, if the ``n``\ th most
|
||||
recently defined variable is well-typed, so is the ``n+1``\ th. In
|
||||
practice, this means we use ``Stop`` to refer to the most recently
|
||||
defined variable, ``Pop Stop`` to refer to the next, and so on, via
|
||||
the ``Var`` constructor:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Var : HasType i ctxt t -> Expr ctxt t
|
||||
|
||||
So, in an expression ``\x. \y. x y``, the variable ``x`` would have a
|
||||
de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
|
||||
represented as ``Stop``. We find these by counting the number of
|
||||
lambdas between the definition and the use.
|
||||
|
||||
A value carries a concrete representation of an integer:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Val : (x : Integer) -> Expr ctxt TyInt
|
||||
|
||||
A lambda creates a function. In the scope of a function of type ``a ->
|
||||
t``, there is a new local variable of type ``a``, which is expressed
|
||||
by the context index:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
|
||||
|
||||
Function application produces a value of type ``t`` given a function
|
||||
from ``a`` to ``t`` and a value of type ``a``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
|
||||
|
||||
We allow arbitrary binary operators, where the type of the operator
|
||||
informs what the types of the arguments must be:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Op : (interpTy a -> interpTy b -> interpTy c) ->
|
||||
Expr ctxt a -> Expr ctxt b -> Expr ctxt c
|
||||
|
||||
Finally, ``If`` expressions make a choice given a boolean. Each branch
|
||||
must have the same type, and we will evaluate the branches lazily so
|
||||
that only the branch which is taken need be evaluated:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
If : Expr ctxt TyBool ->
|
||||
Lazy (Expr ctxt a) ->
|
||||
Lazy (Expr ctxt a) ->
|
||||
Expr ctxt a
|
||||
|
||||
Writing the Interpreter
|
||||
=======================
|
||||
|
||||
When we evaluate an ``Expr``, we'll need to know the values in scope,
|
||||
as well as their types. ``Env`` is an environment, indexed over the
|
||||
types in scope. Since an environment is just another form of list,
|
||||
albeit with a strongly specified connection to the vector of local
|
||||
variable types, we use the usual ``::`` and ``Nil`` constructors so
|
||||
that we can use the usual list syntax. Given a proof that a variable
|
||||
is defined in the context, we can then produce a value from the
|
||||
environment:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Env : Vect n Ty -> Type where
|
||||
Nil : Env Nil
|
||||
(::) : interpTy a -> Env ctxt -> Env (a :: ctxt)
|
||||
|
||||
lookup : HasType i ctxt t -> Env ctxt -> interpTy t
|
||||
lookup Stop (x :: xs) = x
|
||||
lookup (Pop k) (x :: xs) = lookup k xs
|
||||
|
||||
Given this, an interpreter is a function which
|
||||
translates an ``Expr`` into a concrete Idris value with respect to a
|
||||
specific environment:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interp : Env ctxt -> Expr ctxt t -> interpTy t
|
||||
|
||||
The complete interpreter is defined as follows, for reference. For
|
||||
each constructor, we translate it into the corresponding Idris value:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interp env (Var i) = lookup i env
|
||||
interp env (Val x) = x
|
||||
interp env (Lam sc) = \x => interp (x :: env) sc
|
||||
interp env (App f s) = interp env f (interp env s)
|
||||
interp env (Op op x y) = op (interp env x) (interp env y)
|
||||
interp env (If x t e) = if interp env x then interp env t
|
||||
else interp env e
|
||||
|
||||
Let us look at each case in turn. To translate a variable, we simply look it
|
||||
up in the environment:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interp env (Var i) = lookup i env
|
||||
|
||||
To translate a value, we just return the concrete representation of the
|
||||
value:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interp env (Val x) = x
|
||||
|
||||
Lambdas are more interesting. In this case, we construct a function
|
||||
which interprets the scope of the lambda with a new value in the
|
||||
environment. So, a function in the object language is translated to an
|
||||
Idris function:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interp env (Lam sc) = \x => interp (x :: env) sc
|
||||
|
||||
For an application, we interpret the function and its argument and apply
|
||||
it directly. We know that interpreting ``f`` must produce a function,
|
||||
because of its type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interp env (App f s) = interp env f (interp env s)
|
||||
|
||||
Operators and conditionals are, again, direct translations into the
|
||||
equivalent Idris constructs. For operators, we apply the function to
|
||||
its operands directly, and for ``If``, we apply the Idris
|
||||
``if...then...else`` construct directly.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interp env (Op op x y) = op (interp env x) (interp env y)
|
||||
interp env (If x t e) = if interp env x then interp env t
|
||||
else interp env e
|
||||
|
||||
Testing
|
||||
=======
|
||||
|
||||
We can make some simple test functions. Firstly, adding two inputs
|
||||
``\x. \y. y + x`` is written as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
|
||||
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
|
||||
|
||||
More interestingly, a factorial function ``fact``
|
||||
(e.g. ``\x. if (x == 0) then 1 else (fact (x-1) * x)``),
|
||||
can be written as:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
fact : Expr ctxt (TyFun TyInt TyInt)
|
||||
fact = Lam (If (Op (==) (Var Stop) (Val 0))
|
||||
(Val 1)
|
||||
(Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
|
||||
(Var Stop)))
|
||||
|
||||
Running
|
||||
=======
|
||||
|
||||
To finish, we write a ``main`` program which interprets the factorial
|
||||
function on user input:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
main : IO ()
|
||||
main = do putStr "Enter a number: "
|
||||
x <- getLine
|
||||
printLn (interp [] fact (cast x))
|
||||
|
||||
Here, ``cast`` is an overloaded function which converts a value from
|
||||
one type to another if possible. Here, it converts a string to an
|
||||
integer, giving 0 if the input is invalid. An example run of this
|
||||
program at the Idris interactive environment is:
|
||||
|
||||
.. _factrun:
|
||||
.. literalinclude:: ../listing/idris-prompt-interp.txt
|
||||
|
||||
|
||||
Aside: ``cast``
|
||||
---------------
|
||||
|
||||
The prelude defines an interface ``Cast`` which allows conversion
|
||||
between types:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interface Cast from to where
|
||||
cast : from -> to
|
||||
|
||||
It is a *multi-parameter* interface, defining the source type and
|
||||
object type of the cast. It must be possible for the type checker to
|
||||
infer *both* parameters at the point where the cast is applied. There
|
||||
are casts defined between all of the primitive types, as far as they
|
||||
make sense.
|
@ -1,75 +0,0 @@
|
||||
.. _sect-intro:
|
||||
|
||||
************
|
||||
Introduction
|
||||
************
|
||||
|
||||
In conventional programming languages, there is a clear distinction
|
||||
between *types* and *values*. For example, in `Haskell
|
||||
<http://www.haskell.org>`_, the following are types, representing
|
||||
integers, characters, lists of characters, and lists of any value
|
||||
respectively:
|
||||
|
||||
- ``Int``, ``Char``, ``[Char]``, ``[a]``
|
||||
|
||||
Correspondingly, the following values are examples of inhabitants of
|
||||
those types:
|
||||
|
||||
- ``42``, ``’a’``, ``"Hello world!"``, ``[2,3,4,5,6]``
|
||||
|
||||
In a language with *dependent types*, however, the distinction is less
|
||||
clear. Dependent types allow types to “depend” on values — in other
|
||||
words, types are a *first class* language construct and can be
|
||||
manipulated like any other value. The standard example is the type of
|
||||
lists of a given length [#fn1]_, ``Vect n a``, where ``a`` is the element
|
||||
type and ``n`` is the length of the list and can be an arbitrary term.
|
||||
|
||||
When types can contain values, and where those values describe
|
||||
properties, for example the length of a list, the type of a function
|
||||
can begin to describe its own properties. Take for example the
|
||||
concatenation of two lists. This operation has the property that the
|
||||
resulting list's length is the sum of the lengths of the two input
|
||||
lists. We can therefore give the following type to the ``app``
|
||||
function, which concatenates vectors:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
app : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
|
||||
This tutorial introduces Idris, a general purpose functional
|
||||
programming language with dependent types. The goal of the Idris
|
||||
project is to build a dependently typed language suitable for
|
||||
verifiable general purpose programming. To this end, Idris is a compiled
|
||||
language which aims to generate efficient executable code. It also has
|
||||
a lightweight foreign function interface which allows easy interaction
|
||||
with external libraries.
|
||||
|
||||
Intended Audience
|
||||
=================
|
||||
|
||||
This tutorial is intended as a brief introduction to the language, and
|
||||
is aimed at readers already familiar with a functional language such
|
||||
as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
|
||||
In particular, a certain amount of familiarity with Haskell syntax is
|
||||
assumed, although most concepts will at least be explained
|
||||
briefly. The reader is also assumed to have some interest in using
|
||||
dependent types for writing and verifying software.
|
||||
|
||||
For a more in-depth introduction to Idris, which proceeds at a much slower
|
||||
pace, covering interactive program development, with many more examples, see
|
||||
`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>`_.
|
||||
|
||||
Example Code
|
||||
============
|
||||
|
||||
This tutorial includes some example code, which has been tested
|
||||
against Idris 2. These files are available with the Idris 2 distribution,
|
||||
so that you can try them out easily. They can be found under
|
||||
``samples``. It is, however, strongly recommended that you type
|
||||
them in yourself, rather than simply loading and reading them.
|
||||
|
||||
.. rubric:: Footnotes
|
||||
|
||||
.. [#fn1] Typically, and perhaps confusingly, referred to in the dependently
|
||||
typed programming literature as "vectors".
|
@ -1,165 +0,0 @@
|
||||
.. _sect-misc:
|
||||
|
||||
**********
|
||||
Miscellany
|
||||
**********
|
||||
|
||||
In this section we discuss a variety of additional features:
|
||||
|
||||
+ auto, implicit, and default arguments;
|
||||
+ 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 [#IdrisType]_, e.g.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
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
|
||||
constructing a proof. For example, the following definition of ``head``
|
||||
which requires a proof that the list is non-empty:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
isCons : List a -> Bool
|
||||
isCons [] = False
|
||||
isCons (x :: xs) = True
|
||||
|
||||
head : (xs : List a) -> (isCons xs = True) -> a
|
||||
head (x :: xs) _ = x
|
||||
|
||||
If the list is statically known to be non-empty, either because its
|
||||
value is known or because a proof already exists in the context, the
|
||||
proof can be constructed automatically. Auto implicit arguments allow
|
||||
this to happen silently. We define ``head`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
head : (xs : List a) -> {auto p : isCons xs = True} -> a
|
||||
head (x :: xs) = x
|
||||
|
||||
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. 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.
|
||||
- The constructors of the required type. If they have arguments, it will
|
||||
search recursively up to a maximum depth of 100.
|
||||
- Local variables with function types, searching recursively for the
|
||||
arguments.
|
||||
- Any function with the appropriate return type which is marked with the
|
||||
``%hint`` annotation.
|
||||
|
||||
In the case that a proof is not found, it can be provided explicitly as normal:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
head xs {p = ?headProof}
|
||||
|
||||
Default implicit arguments
|
||||
---------------------------
|
||||
|
||||
Besides having Idris automatically find a value of a given type, sometimes we
|
||||
want to have an implicit argument with a specific default value. In Idris, we can
|
||||
do this using the ``default`` annotation. While this is primarily intended to assist
|
||||
in automatically constructing a proof where auto fails, or finds an unhelpful value,
|
||||
it might be easier to first consider a simpler case, not involving proofs.
|
||||
|
||||
If we want to compute the n'th fibonacci number (and defining the 0th fibonacci
|
||||
number as 0), we could write:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
|
||||
fibonacci {lag} Z = lag
|
||||
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
|
||||
|
||||
After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
|
||||
and will return the 5th fibonacci number. Note that while this works, this is not the
|
||||
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.
|
||||
|
||||
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
|
||||
begins with a greater than sign ``>``, for example:
|
||||
|
||||
.. code-block:: literate-idris
|
||||
:force:
|
||||
|
||||
> module literate
|
||||
|
||||
This is a comment. The main program is below
|
||||
|
||||
> main : IO ()
|
||||
> main = putStrLn "Hello literate world!\n"
|
||||
|
||||
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).
|
||||
|
||||
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:
|
||||
|
||||
::
|
||||
|
||||
*universe> :t Nat
|
||||
Nat : Type
|
||||
*universe> :t Vect
|
||||
Vect : Nat -> Type -> Type
|
||||
|
||||
But what about the type of ``Type``? If we ask Idris it reports:
|
||||
|
||||
::
|
||||
|
||||
*universe> :t Type
|
||||
Type : Type 1
|
||||
|
||||
If ``Type`` were its own type, it would lead to an inconsistency due to
|
||||
`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
|
||||
so internally there is a *hierarchy* of types (or *universes*):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Type : Type 1 : Type 2 : Type 3 : ...
|
||||
|
||||
Universes are *cumulative*, that is, if ``x : Type n`` we can also have
|
||||
that ``x : Type m``, as long as ``n < m``. The typechecker generates
|
||||
such universe constraints and reports an error if any inconsistencies
|
||||
are found. Ordinarily, a programmer does not need to worry about this,
|
||||
but it does prevent (contrived) programs such as the following:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
myid : (a : Type) -> a -> a
|
||||
myid _ x = x
|
||||
|
||||
idid : (a : Type) -> a -> a
|
||||
idid = myid _ myid
|
||||
|
||||
The application of ``myid`` to itself leads to a cycle in the universe
|
||||
hierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot be
|
||||
at a lower level than required if it is applied to itself.
|
||||
|
||||
.. [#IdrisType] https://github.com/david-christiansen/idris-type-providers
|
@ -1,249 +0,0 @@
|
||||
.. _sect-namespaces:
|
||||
|
||||
**********************
|
||||
Modules and Namespaces
|
||||
**********************
|
||||
|
||||
An Idris program consists of a collection of modules. Each module
|
||||
includes an optional ``module`` declaration giving the name of the
|
||||
module, a list of ``import`` statements giving the other modules which
|
||||
are to be imported, and a collection of declarations and definitions of
|
||||
types, interfaces and functions. For example, the listing below gives a
|
||||
module which defines a binary tree type ``BTree`` (in a file
|
||||
``BTree.idr``):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
module BTree
|
||||
|
||||
public export
|
||||
data BTree a = Leaf
|
||||
| Node (BTree a) a (BTree a)
|
||||
|
||||
export
|
||||
insert : Ord a => a -> BTree a -> BTree a
|
||||
insert x Leaf = Node Leaf x Leaf
|
||||
insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
|
||||
else (Node l v (insert x r))
|
||||
|
||||
export
|
||||
toList : BTree a -> List a
|
||||
toList Leaf = []
|
||||
toList (Node l v r) = BTree.toList l ++ (v :: BTree.toList r)
|
||||
|
||||
export
|
||||
toTree : Ord a => List a -> BTree a
|
||||
toTree [] = Leaf
|
||||
toTree (x :: xs) = insert x (toTree xs)
|
||||
|
||||
The modifiers ``export`` and ``public export`` say which names are visible
|
||||
from other namespaces. These are explained further below.
|
||||
|
||||
Then, this gives a main program (in a file
|
||||
``bmain.idr``) which uses the ``BTree`` module to sort a list:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
module Main
|
||||
|
||||
import BTree
|
||||
|
||||
main : IO ()
|
||||
main = do let t = toTree [1,8,2,7,9,3]
|
||||
print (BTree.toList t)
|
||||
|
||||
The same names can be defined in multiple modules: names are *qualified* with
|
||||
the name of the module. The names defined in the ``BTree`` module are, in full:
|
||||
|
||||
+ ``BTree.BTree``
|
||||
+ ``BTree.Leaf``
|
||||
+ ``BTree.Node``
|
||||
+ ``BTree.insert``
|
||||
+ ``BTree.toList``
|
||||
+ ``BTree.toTree``
|
||||
|
||||
If names are otherwise unambiguous, there is no need to give the fully
|
||||
qualified name. Names can be disambiguated either by giving an explicit
|
||||
qualification, or according to their type.
|
||||
|
||||
There is no formal link between the module name and its filename,
|
||||
although it is generally advisable to use the same name for each. An
|
||||
``import`` statement refers to a filename, using dots to separate
|
||||
directories. For example, ``import foo.bar`` would import the file
|
||||
``foo/bar.idr``, which would conventionally have the module declaration
|
||||
``module foo.bar``. The only requirement for module names is that the
|
||||
main module, with the ``main`` function, must be called
|
||||
``Main`` — although its filename need not be ``Main.idr``.
|
||||
|
||||
Export Modifiers
|
||||
================
|
||||
|
||||
Idris allows for fine-grained control over the visibility of a
|
||||
namespace's contents. By default, all names defined in a namespace are kept
|
||||
private. This aids in specification of a minimal interface and for
|
||||
internal details to be left hidden. Idris allows for functions,
|
||||
types, and interfaces to be marked as: ``private``, ``export``, or
|
||||
``public export``. Their general meaning is as follows:
|
||||
|
||||
- ``private`` meaning that it is not exported at all. This is the default.
|
||||
|
||||
- ``export`` meaning that its top level type is exported.
|
||||
|
||||
- ``public export`` meaning that the entire definition is exported.
|
||||
|
||||
A further restriction in modifying the visibility is that definitions must not
|
||||
refer to anything within a lower level of visibility. For example, ``public
|
||||
export`` definitions cannot use ``private`` or ``export`` names, and ``export``
|
||||
types cannot use ``private`` names. This is to prevent private names leaking
|
||||
into a module's interface.
|
||||
|
||||
Meaning for Functions
|
||||
---------------------
|
||||
|
||||
- ``export`` the type is exported
|
||||
|
||||
- ``public export`` the type and definition are exported, and the
|
||||
definition can be used after it is imported. In other words, the
|
||||
definition itself is considered part of the module's interface. The
|
||||
long name ``public export`` is intended to make you think twice
|
||||
about doing this.
|
||||
|
||||
.. note::
|
||||
|
||||
Type synonyms in Idris are created by writing a function. When
|
||||
setting the visibility for a module, it is usually a good idea to
|
||||
``public export`` all type synonyms if they are to be used outside
|
||||
the module. Otherwise, Idris won't know what the synonym is a
|
||||
synonym for.
|
||||
|
||||
Since ``public export`` means that a function's definition is exported,
|
||||
this effectively makes the function definition part of the module's API.
|
||||
Therefore, it's generally a good idea to avoid using ``public export`` for
|
||||
functions unless you really mean to export the full definition.
|
||||
|
||||
Meaning for Data Types
|
||||
----------------------
|
||||
|
||||
For data types, the meanings are:
|
||||
|
||||
- ``export`` the type constructor is exported
|
||||
|
||||
- ``public export`` the type constructor and data constructors are exported
|
||||
|
||||
|
||||
Meaning for Interfaces
|
||||
----------------------
|
||||
|
||||
For interfaces, the meanings are:
|
||||
|
||||
- ``export`` the interface name is exported
|
||||
|
||||
- ``public export`` the interface name, method names and default
|
||||
definitions are exported
|
||||
|
||||
Propagating Inner Module API's
|
||||
-------------------------------
|
||||
|
||||
Additionally, a module can re-export a module it has imported, by using
|
||||
the ``public`` modifier on an ``import``. For example:
|
||||
|
||||
.. code-block:: idris
|
||||
:force:
|
||||
|
||||
module A
|
||||
|
||||
import B
|
||||
import public C
|
||||
|
||||
The module ``A`` will export the name ``a``, as well as any public or
|
||||
abstract names in module ``C``, but will not re-export anything from
|
||||
module ``B``.
|
||||
|
||||
Explicit Namespaces
|
||||
===================
|
||||
|
||||
Defining a module also defines a namespace implicitly. However,
|
||||
namespaces can also be given *explicitly*. This is most useful if you
|
||||
wish to overload names within the same module:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
module Foo
|
||||
|
||||
namespace X
|
||||
export
|
||||
test : Int -> Int
|
||||
test x = x * 2
|
||||
|
||||
namespace Y
|
||||
export
|
||||
test : String -> String
|
||||
test x = x ++ x
|
||||
|
||||
This (admittedly contrived) module defines two functions with fully
|
||||
qualified names ``Foo.X.test`` and ``Foo.Y.test``, which can be
|
||||
disambiguated by their types:
|
||||
|
||||
::
|
||||
|
||||
*Foo> test 3
|
||||
6 : Int
|
||||
*Foo> test "foo"
|
||||
"foofoo" : String
|
||||
|
||||
The export rules, ``public export`` and ``export``, are *per namespace*,
|
||||
not *per file*, so the two ``test`` definitions above need the ``export``
|
||||
flag to be visible outside their own namespaces.
|
||||
|
||||
Parameterised blocks
|
||||
====================
|
||||
|
||||
Groups of functions can be parameterised over a number of arguments
|
||||
using a ``parameters`` declaration, for example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parameters (x : Nat, y : Nat)
|
||||
addAll : Nat -> Nat
|
||||
addAll z = x + y + z
|
||||
|
||||
The effect of a ``parameters`` block is to add the declared parameters
|
||||
to every function, type and data constructor within the
|
||||
block. Specifically, adding the parameters to the front of the
|
||||
argument list. Outside the block, the parameters must be given
|
||||
explicitly. The ``addAll`` function, when called from the REPL, will
|
||||
thus have the following type signature.
|
||||
|
||||
::
|
||||
|
||||
*params> :t addAll
|
||||
addAll : Nat -> Nat -> Nat -> Nat
|
||||
|
||||
and the following definition.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat
|
||||
addAll x y z = x + y + z
|
||||
|
||||
Parameters blocks can be nested, and can also include data declarations,
|
||||
in which case the parameters are added explicitly to all type and data
|
||||
constructors. They may also be dependent types with implicit arguments:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parameters (y : Nat, xs : Vect x a)
|
||||
data Vects : Type -> Type where
|
||||
MkVects : Vect y a -> Vects a
|
||||
|
||||
append : Vects a -> Vect (x + y) a
|
||||
append (MkVects ys) = xs ++ ys
|
||||
|
||||
To use ``Vects`` or ``append`` outside the block, we must also give the
|
||||
``xs`` and ``y`` arguments. Here, we can use placeholders for the values
|
||||
which can be inferred by the type checker:
|
||||
|
||||
::
|
||||
|
||||
Main> show (append _ _ (MkVects _ [1,2,3] [4,5,6]))
|
||||
"[1, 2, 3, 4, 5, 6]"
|
@ -1,563 +0,0 @@
|
||||
.. _sect-multiplicities:
|
||||
|
||||
**************
|
||||
Multiplicities
|
||||
**************
|
||||
|
||||
Idris 2 is
|
||||
based on `Quantitative Type Theory (QTT)
|
||||
<https://bentnib.org/quantitative-type-theory.html>`_, a core language
|
||||
developed by Bob Atkey and Conor McBride. In practice, this means that every
|
||||
variable in Idris 2 has a *quantity* associated with it. A quantity is one of:
|
||||
|
||||
* ``0``, meaning that the variable is *erased* at run time
|
||||
* ``1``, meaning that the variable is used *exactly once* at run time
|
||||
* *Unrestricted*, which is the same behaviour as Idris 1
|
||||
|
||||
We can see the multiplicities of variables by inspecting holes. For example,
|
||||
if we have the following skeleton definition of ``append`` on vectors...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
append xs ys = ?append_rhs
|
||||
|
||||
...we can look at the hole ``append_rhs``:
|
||||
|
||||
::
|
||||
|
||||
Main> :t append_rhs
|
||||
0 m : Nat
|
||||
0 a : Type
|
||||
0 n : Nat
|
||||
ys : Vect m a
|
||||
xs : Vect n a
|
||||
-------------------------------------
|
||||
append_rhs : Vect (plus n m) a
|
||||
|
||||
The ``0`` next to ``m``, ``a`` and ``n`` mean that they are in scope, but there
|
||||
will be ``0`` occurrences at run-time. That is, it is **guaranteed** that they
|
||||
will be erased at run-time.
|
||||
|
||||
Multiplicities can be explicitly written in function types as follows:
|
||||
|
||||
* ``ignoreN : (0 n : Nat) -> Vect n a -> Nat`` - this function cannot look at
|
||||
``n`` at run time
|
||||
* ``duplicate : (1 x : a) -> (a, a)`` - this function must use ``x`` exactly
|
||||
once (so good luck implementing it, by the way. There is no implementation
|
||||
because it would need to use ``x`` twice!)
|
||||
|
||||
If there is no multiplicity annotation, the argument is unrestricted.
|
||||
If, on the other hand, a name is implicitly bound (like ``a`` in both examples above)
|
||||
the argument is erased. So, the above types could also be written as:
|
||||
|
||||
* ``ignoreN : {0 a : _} -> (0 n : Nat) -> Vect n a -> Nat``
|
||||
* ``duplicate : {0 a : _} -> (1 x : a) -> (a, a)``
|
||||
|
||||
This section describes what this means for your Idris 2 programs in practice,
|
||||
with several examples. In particular, it describes:
|
||||
|
||||
* :ref:`sect-erasure` - how to know what is relevant at run time and what is erased
|
||||
* :ref:`sect-linearity` - using the type system to encode *resource usage protocols*
|
||||
* :ref:`sect-pmtypes` - truly first class types
|
||||
|
||||
The most important of these for most programs, and the thing you'll need to
|
||||
know about if converting Idris 1 programs to work with Idris 2, is erasure_.
|
||||
The most interesting, however, and the thing which gives Idris 2 much more
|
||||
expressivity, is linearity_, so we'll start there.
|
||||
|
||||
.. _sect-linearity:
|
||||
|
||||
Linearity
|
||||
---------
|
||||
|
||||
The ``1`` multiplicity expresses that a variable must be used exactly once.
|
||||
First, we'll see how this works on some small examples of functions and
|
||||
data types, then see how it can be used to encode `resource protocols`_.
|
||||
|
||||
Above, we saw the type of ``duplicate``. Let's try to write it interactively,
|
||||
and see what goes wrong. We'll start by giving the type and a skeleton
|
||||
definition with a hole
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
duplicate : (1 x : a) -> (a, a)
|
||||
duplicate x = ?help
|
||||
|
||||
Checking the type of a hole tells us the multiplicity of each variable in
|
||||
scope. If we check the type of ``?help`` we'll see that we can't
|
||||
use ``a`` at run time, and we have to use ``x`` exactly once::
|
||||
|
||||
Main> :t help
|
||||
0 a : Type
|
||||
1 x : a
|
||||
-------------------------------------
|
||||
help : (a, a)
|
||||
|
||||
If we use ``x`` for one part of the pair...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
duplicate : (1 x : a) -> (a, a)
|
||||
duplicate x = (x, ?help)
|
||||
|
||||
...then the type of the remaining hole tells us we can't use it for the other::
|
||||
|
||||
Main> :t help
|
||||
0 a : Type
|
||||
0 x : a
|
||||
-------------------------------------
|
||||
help : a
|
||||
|
||||
The same happens if we try defining ``duplicate x = (?help, x)`` (try it!)
|
||||
The intution behind multiplicity ``1`` is that if we have a function with
|
||||
a type of the following form...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
f : (1 x : a) -> b
|
||||
|
||||
...then the guarantee given by the type system is that *if* ``f x`` *is used
|
||||
exactly once, then* ``x`` *is used exactly once*. So, if we insist on
|
||||
trying to define ``duplicate``...::
|
||||
|
||||
duplicate x = (x, x)
|
||||
|
||||
...then Idris will complain::
|
||||
|
||||
pmtype.idr:2:15--8:1:While processing right hand side of Main.duplicate at pmtype.idr:2:1--8:1:
|
||||
There are 2 uses of linear name x
|
||||
|
||||
A similar intuition applies for data types. Consider the following types,
|
||||
``Lin`` which wraps an argument that must be used once, and ``Unr`` which
|
||||
wraps an argument with unrestricted use
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Lin : Type -> Type where
|
||||
MkLin : (1 x : a) -> Lin a
|
||||
|
||||
data Unr : Type -> Type where
|
||||
MkUnr : (x : a) -> Unr a
|
||||
|
||||
If ``MkLin x`` is used once, then ``x`` is used once. But if ``MkUnr x`` is
|
||||
used once, there is no guarantee on how often ``x`` is used. We can see this a
|
||||
bit more clearly by starting to write projection functions for ``Lin`` and
|
||||
``Unr`` to extract the argument
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
getLin : (1 val : Lin a) -> a
|
||||
getLin (MkLin x) = ?howmanyLin
|
||||
|
||||
getUnr : (1 val : Unr a) -> a
|
||||
getUnr (MkUnr x) = ?howmanyUnr
|
||||
|
||||
Checking the types of the holes shows us that, for ``getLin``, we must use
|
||||
``x`` exactly once (Because the ``val`` argument is used once,
|
||||
by pattern matching on it as ``MkLin x``, and if ``MkLin x`` is used once,
|
||||
``x`` must be used once)::
|
||||
|
||||
Main> :t howmanyLin
|
||||
0 a : Type
|
||||
1 x : a
|
||||
-------------------------------------
|
||||
howmanyLin : a
|
||||
|
||||
For ``getUnr``, however, we still have to use ``val`` once, again by pattern
|
||||
matching on it, but using ``MkUnr x`` once doesn't place any restrictions on
|
||||
``x``. So, ``x`` has unrestricted use in the body of ``getUnr``::
|
||||
|
||||
Main> :t howmanyUnr
|
||||
0 a : Type
|
||||
x : a
|
||||
-------------------------------------
|
||||
howmanyUnr : a
|
||||
|
||||
If ``getLin`` has an unrestricted argument...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
getLin : (val : Lin a) -> a
|
||||
getLin (MkLin x) = ?howmanyLin
|
||||
|
||||
...then ``x`` is unrestricted in ``howmanyLin``::
|
||||
|
||||
Main> :t howmanyLin
|
||||
0 a : Type
|
||||
x : a
|
||||
-------------------------------------
|
||||
howmanyLin : a
|
||||
|
||||
Remember the intuition from the type of ``MkLin`` is that if ``MkLin x`` is
|
||||
used exactly once, ``x`` is used exactly once. But, we didn't say that
|
||||
``MkLin x`` would be used exactly once, so there is no restriction on ``x``.
|
||||
|
||||
Resource protocols
|
||||
~~~~~~~~~~~~~~~~~~
|
||||
|
||||
One way to take advantage of being able to express linear usage of an argument
|
||||
is in defining resource usage protocols, where we can use linearity to ensure
|
||||
that any unique external resource has only one instance, and we can use
|
||||
functions which are linear in their arguments to represent state transitions on
|
||||
that resource. A door, for example, can be in one of two states, ``Open`` or
|
||||
``Closed``
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data DoorState = Open | Closed
|
||||
|
||||
data Door : DoorState -> Type where
|
||||
MkDoor : (doorId : Int) -> Door st
|
||||
|
||||
(Okay, we're just pretending here - imagine the ``doorId`` is a reference
|
||||
to an external resource!)
|
||||
|
||||
We can define functions for opening and closing the door which explicitly
|
||||
describe how they change the state of a door, and that they are linear in
|
||||
the door
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
openDoor : (1 d : Door Closed) -> Door Open
|
||||
closeDoor : (1 d : Door Open) -> Door Closed
|
||||
|
||||
Remember, the intuition is that if ``openDoor d`` is used exactly once,
|
||||
then ``d`` is used exactly once. So, provided that a door ``d`` has
|
||||
multiplicity ``1`` when it's created, we *know* that once we call
|
||||
``openDoor`` on it, we won't be able to use ``d`` again. Given that
|
||||
``d`` is an external resource, and ``openDoor`` has changed it's state,
|
||||
this is a good thing!
|
||||
|
||||
We can ensure that any door we create has multiplicity ``1`` by
|
||||
creating them with a ``newDoor`` function with the following type
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()
|
||||
|
||||
That is, ``newDoor`` takes a function, which it runs exactly once. That
|
||||
function takes a door, which is used exactly once. We'll run it in
|
||||
``IO`` to suggest that there is some interaction with the outside world
|
||||
going on when we create the door. Since the multiplicity ``1`` means the
|
||||
door has to be used exactly once, we need to be able to delete the door
|
||||
when we're finished
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
deleteDoor : (1 d : Door Closed) -> IO ()
|
||||
|
||||
So an example correct door protocol usage would be
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
doorProg : IO ()
|
||||
doorProg
|
||||
= newDoor $ \d =>
|
||||
let d' = openDoor d
|
||||
d'' = closeDoor d' in
|
||||
deleteDoor d''
|
||||
|
||||
It's instructive to build this program interactively, with holes along
|
||||
the way, and see how the multiplicities of ``d``, ``d'`` etc change. For
|
||||
example
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
doorProg : IO ()
|
||||
doorProg
|
||||
= newDoor $ \d =>
|
||||
let d' = openDoor d in
|
||||
?whatnow
|
||||
|
||||
Checking the type of ``?whatnow`` shows that ``d`` is now spent, but we
|
||||
still have to use ``d'`` exactly once::
|
||||
|
||||
Main> :t whatnow
|
||||
0 d : Door Closed
|
||||
1 d' : Door Open
|
||||
-------------------------------------
|
||||
whatnow : IO ()
|
||||
|
||||
Note that the ``0`` multiplicity for ``d`` means that we can still *talk*
|
||||
about it - in particular, we can still reason about it in types - but we
|
||||
can't use it again in a relevant position in the rest of the program.
|
||||
It's also fine to shadow the name ``d`` throughout
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
doorProg : IO ()
|
||||
doorProg
|
||||
= newDoor $ \d =>
|
||||
let d = openDoor d
|
||||
d = closeDoor d in
|
||||
deleteDoor d
|
||||
|
||||
If we don't follow the protocol correctly - create the door, open it, close
|
||||
it, then delete it - then the program won't type check. For example, we
|
||||
can try not to delete the door before finishing
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
doorProg : IO ()
|
||||
doorProg
|
||||
= newDoor $ \d =>
|
||||
let d' = openDoor d
|
||||
d'' = closeDoor d' in
|
||||
putStrLn "What could possibly go wrong?"
|
||||
|
||||
This gives the following error::
|
||||
|
||||
Door.idr:15:19--15:38:While processing right hand side of Main.doorProg at Door.idr:13:1--17:1:
|
||||
There are 0 uses of linear name d''
|
||||
|
||||
There's a lot more to be said about the details here! But, this shows at
|
||||
a high level how we can use linearity to capture resource usage protocols
|
||||
at the type level. If we have an external resource which is guaranteed to
|
||||
be used linearly, like ``Door``, we don't need to run operations on that
|
||||
resource in an ``IO`` monad, since we're already enforcing an ordering on
|
||||
operations and don't have access to any out of date resource states. This is
|
||||
similar to the way interactive programs work in
|
||||
`the Clean programming language <https://clean.cs.ru.nl/Clean>`_, and in
|
||||
fact is how ``IO`` is implemented internally in Idris 2, with a special
|
||||
``%World`` type for representing the state of the outside world that is
|
||||
always used linearly
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
public export
|
||||
data IORes : Type -> Type where
|
||||
MkIORes : (result : a) -> (1 x : %World) -> IORes a
|
||||
|
||||
export
|
||||
data IO : Type -> Type where
|
||||
MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
|
||||
|
||||
Having multiplicities in the type system raises several interesting
|
||||
questions, such as:
|
||||
|
||||
* Can we use linearity information to inform memory management and, for
|
||||
example, have type level guarantees about functions which will not need
|
||||
to perform garbage collection?
|
||||
* How should multiplicities be incorporated into interfaces such as
|
||||
``Functor``, ``Applicative`` and ``Monad``?
|
||||
* If we have ``0``, and ``1`` as multiplicities, why stop there? Why not have
|
||||
``2``, ``3`` and more (like `Granule
|
||||
<https://granule-project.github.io/granule.html>`_)
|
||||
* What about multiplicity polymorphism, as in the `Linear Haskell proposal <https://arxiv.org/abs/1710.09756>`_?
|
||||
* Even without all of that, what can we do *now*?
|
||||
|
||||
.. _sect-erasure:
|
||||
|
||||
Erasure
|
||||
-------
|
||||
|
||||
The ``1`` multiplicity give us many possibilities in the kinds of
|
||||
properties we can express. But, the ``0`` multiplicity is perhaps more
|
||||
important in that it allows us to be precise about which values are
|
||||
relevant at run time, and which are compile time only (that is, which are
|
||||
erased). Using the ``0`` multiplicity means a function's type now tells us
|
||||
exactly what it needs at run time.
|
||||
|
||||
For example, in Idris 1 you could get the length of a vector as follows
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vlen : Vect n a -> Nat
|
||||
vlen {n} xs = n
|
||||
|
||||
This is fine, since it runs in constant time, but the trade off is that
|
||||
``n`` has to be available at run time, so at run time we always need the length
|
||||
of the vector to be available if we ever call ``vlen``. Idris 1 can infer whether
|
||||
the length is needed, but there's no easy way for a programmer to be sure.
|
||||
|
||||
In Idris 2, we need to state explicitly that ``n`` is needed at run time
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vlen : {n : Nat} -> Vect n a -> Nat
|
||||
vlen xs = n
|
||||
|
||||
(Incidentally, also note that in Idris 2, names bound in types are also available
|
||||
in the definition without explicitly rebinding them.)
|
||||
|
||||
This also means that when you call ``vlen``, you need the length available. For
|
||||
example, this will give an error
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sumLengths : Vect m a -> Vect n a —> Nat
|
||||
sumLengths xs ys = vlen xs + vlen ys
|
||||
|
||||
Idris 2 reports::
|
||||
|
||||
vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
|
||||
m is not accessible in this context
|
||||
|
||||
This means that it needs to use ``m`` as an argument to pass to ``vlen xs``,
|
||||
where it needs to be available at run time, but ``m`` is not available in
|
||||
``sumLengths`` because it has multiplicity ``0``.
|
||||
|
||||
We can see this more clearly by replacing the right hand side of
|
||||
``sumLengths`` with a hole...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sumLengths : Vect m a -> Vect n a -> Nat
|
||||
sumLengths xs ys = ?sumLengths_rhs
|
||||
|
||||
...then checking the hole's type at the REPL::
|
||||
|
||||
Main> :t sumLengths_rhs
|
||||
0 n : Nat
|
||||
0 a : Type
|
||||
0 m : Nat
|
||||
ys : Vect n a
|
||||
xs : Vect m a
|
||||
-------------------------------------
|
||||
sumLengths_rhs : Nat
|
||||
|
||||
Instead, we need to give bindings for ``m`` and ``n`` with
|
||||
unrestricted multiplicity
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
|
||||
sumLengths xs ys = vLen xs + vLen xs
|
||||
|
||||
Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,
|
||||
means that the variable has unrestricted usage.
|
||||
|
||||
If you're converting Idris 1 programs to work with Idris 2, this is probably the
|
||||
biggest thing you need to think about. It is important to note,
|
||||
though, that if you have bound implicits, such as...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
excitingFn : {t : _} -> Coffee t -> Moonbase t
|
||||
|
||||
...then it's a good idea to make sure ``t`` really is needed, or performance
|
||||
might suffer due to the run time building the instance of ``t`` unnecessarily!
|
||||
|
||||
One final note on erasure: it is an error to try to pattern match on an
|
||||
argument with multiplicity ``0``, unless its value is inferrable from
|
||||
elsewhere. So, the following definition is rejected
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
badNot : (0 x : Bool) -> Bool
|
||||
badNot False = True
|
||||
badNot True = False
|
||||
|
||||
This is rejected with the error::
|
||||
|
||||
badnot.idr:2:1--3:1:Attempt to match on erased argument False in
|
||||
Main.badNot
|
||||
|
||||
The following, however, is fine, because in ``sNot``, even though we appear
|
||||
to match on the erased argument ``x``, its value is uniquely inferrable from
|
||||
the type of the second argument
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data SBool : Bool -> Type where
|
||||
SFalse : SBool False
|
||||
STrue : SBool True
|
||||
|
||||
sNot : (0 x : Bool) -> SBool x -> Bool
|
||||
sNot False SFalse = True
|
||||
sNot True STrue = False
|
||||
|
||||
Experience with Idris 2 so far suggests that, most of the time, as long as
|
||||
you're using unbound implicits in your Idris 1 programs, they will work without
|
||||
much modification in Idris 2. The Idris 2 type checker will point out where you
|
||||
require an unbound implicit argument at run time - sometimes this is both
|
||||
surprising and enlightening!
|
||||
|
||||
.. _sect-pmtypes:
|
||||
|
||||
Pattern Matching on Types
|
||||
-------------------------
|
||||
|
||||
One way to think about dependent types is to think of them as "first class"
|
||||
objects in the language, in that they can be assigned to variables,
|
||||
passed around and returned from functions, just like any other construct.
|
||||
But, if they're truly first class, we should be able to pattern match on
|
||||
them too! Idris 2 allows us to do this. For example
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
showType : Type -> String
|
||||
showType Int = "Int"
|
||||
showType (List a) = "List of " ++ showType a
|
||||
showType _ = "something else"
|
||||
|
||||
We can try this as follows::
|
||||
|
||||
Main> showType Int
|
||||
"Int"
|
||||
Main> showType (List Int)
|
||||
"List of Int"
|
||||
Main> showType (List Bool)
|
||||
"List of something else"
|
||||
|
||||
Pattern matching on function types is interesting, because the return type
|
||||
may depend on the input value. For example, let's add a case to
|
||||
``showType``
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
showType (Nat -> a) = ?help
|
||||
|
||||
Inspecting the type of ``help`` tells us::
|
||||
|
||||
Main> :t help
|
||||
a : Nat -> Type
|
||||
-------------------------------------
|
||||
help : String
|
||||
|
||||
So, the return type ``a`` depends on the input value of type ``Nat``, and
|
||||
we'll need to come up with a value to use ``a``, for example
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
showType (Nat -> a) = "Function from Nat to " ++ showType (a Z)
|
||||
|
||||
Note that multiplicities on the binders, and the ability to pattern match
|
||||
on *non-erased* types mean that the following two types are distinct
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
id : a -> a
|
||||
notId : {a : Type} -> a -> a
|
||||
|
||||
In the case of ``notId``, we can match on ``a`` and get a function which
|
||||
is certainly not the identity function
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
notId {a = Int} x = x + 1
|
||||
notId x = x
|
||||
|
||||
::
|
||||
|
||||
Main> notId 93
|
||||
94
|
||||
Main> notId "???"
|
||||
"???"
|
||||
|
||||
There is an important consequence of being able to distinguish between relevant
|
||||
and irrelevant type arguments, which is that a function is *only* parametric in
|
||||
``a`` if ``a`` has multiplicity ``0``. So, in the case of ``notId``, ``a`` is
|
||||
*not* a parameter, and so we can't draw any conclusions about the way the
|
||||
function will behave because it is polymorphic, because the type tells us it
|
||||
might pattern match on ``a``.
|
||||
|
||||
On the other hand, it is merely a coincidence that, in non-dependently typed
|
||||
languages, types are *irrelevant* and get erased, and values are *relevant*
|
||||
and remain at run time. Idris 2, being based on QTT, allows us to make the
|
||||
distinction between relevant and irrelevant arguments precise. Types can be
|
||||
relevant, values (such as the ``n`` index to vectors) can be irrelevant.
|
||||
|
||||
For more details on multiplicities,
|
||||
see `Idris 2: Quantitative Type Theory in Action <https://www.type-driven.org.uk/edwinb/idris-2-quantitative-type-theory-in-action.html>`_.
|
@ -1,87 +0,0 @@
|
||||
.. _sect-packages:
|
||||
|
||||
********
|
||||
Packages
|
||||
********
|
||||
|
||||
Idris includes a simple build system for building packages and executables
|
||||
from a named package description file. These files can be used with the
|
||||
Idris compiler to manage the development process.
|
||||
|
||||
Package Descriptions
|
||||
====================
|
||||
|
||||
A package description includes the following:
|
||||
|
||||
+ A header, consisting of the keyword ``package`` followed by a package
|
||||
name. Package names can be any valid Idris identifier. The iPKG
|
||||
format also takes a quoted version that accepts any valid filename.
|
||||
|
||||
+ Fields describing package contents, ``<field> = <value>``.
|
||||
|
||||
At least one field must be the modules field, where the value is a
|
||||
comma separated list of modules. For example, given an idris package
|
||||
``maths`` that has modules ``Maths.idr``, ``Maths.NumOps.idr``,
|
||||
``Maths.BinOps.idr``, and ``Maths.HexOps.idr``, the corresponding
|
||||
package file would be:
|
||||
|
||||
::
|
||||
|
||||
package maths
|
||||
|
||||
modules = Maths
|
||||
, Maths.NumOps
|
||||
, Maths.BinOps
|
||||
, Maths.HexOps
|
||||
|
||||
|
||||
Other examples of package files can be found in the ``libs`` directory
|
||||
of the main Idris repository, and in `third-party libraries
|
||||
<https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
|
||||
|
||||
|
||||
Using Package files
|
||||
===================
|
||||
|
||||
Idris itself is aware about packages, and special commands are
|
||||
available to help with, for example, building packages, installing
|
||||
packages, and cleaning packages. For instance, given the ``maths``
|
||||
package from earlier we can use Idris as follows:
|
||||
|
||||
+ ``idris2 --build maths.ipkg`` will build all modules in the package
|
||||
|
||||
+ ``idris2 --install maths.ipkg`` will install the package, making it
|
||||
accessible by other Idris libraries and programs.
|
||||
|
||||
+ ``idris2 --clean maths.ipkg`` will delete all intermediate code and
|
||||
executable files generated when building.
|
||||
|
||||
Once the maths package has been installed, the command line option
|
||||
``--package maths`` makes it accessible (abbreviated to ``-p maths``).
|
||||
For example:
|
||||
|
||||
::
|
||||
|
||||
idris2 -p maths Main.idr
|
||||
|
||||
Package Dependencies Using Atom
|
||||
===============================
|
||||
|
||||
If you are using the Atom editor and have a dependency on another package,
|
||||
corresponding to for instance ``import Lightyear`` or ``import Pruviloj``,
|
||||
you need to let Atom know that it should be loaded. The easiest way to
|
||||
accomplish that is with a .ipkg file. The general contents of an ipkg file
|
||||
will be described in the next section of the tutorial, but for now here is
|
||||
a simple recipe for this trivial case:
|
||||
|
||||
- Create a folder myProject.
|
||||
|
||||
- Add a file myProject.ipkg containing just a couple of lines:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
package myProject
|
||||
|
||||
pkgs = pruviloj, lightyear
|
||||
|
||||
- In Atom, use the File menu to Open Folder myProject.
|
@ -1,104 +0,0 @@
|
||||
.. _sect-starting:
|
||||
|
||||
***************
|
||||
Getting Started
|
||||
***************
|
||||
|
||||
Prerequisites
|
||||
=============
|
||||
|
||||
You need a C compiler (default is clang), and optionally Idris 1.3.2 to build
|
||||
from source. You will also need:
|
||||
|
||||
- `Chez Scheme <https://cisco.github.io/ChezScheme/>`_
|
||||
- The `GNU Multiple Precision Arithmetic Library <https://gmplib.org/>`_ (GMP)
|
||||
|
||||
Both are available from MacPorts/Homebrew and all major Linux distributions.
|
||||
|
||||
**Note**: If you install ChezScheme from source files, building it locally, make sure
|
||||
you run ``./configure --threads`` to build multithreading support in.
|
||||
|
||||
Downloading and Installing
|
||||
==========================
|
||||
|
||||
You can download the Idris 2 source from the `Idris web site
|
||||
<https://www.idris-lang.org/pages/download.html>`_.
|
||||
This includes the Idris 2 source code (written in Idris 1) and the C
|
||||
code generated from that. Once you have unpacked the source, you can
|
||||
install it as follows:
|
||||
|
||||
* If you have Idris 1.3.2 installed::
|
||||
|
||||
make install
|
||||
|
||||
* If not, you can install directly from the generated C::
|
||||
|
||||
make install-fromc
|
||||
|
||||
This will, by default, install into ``${HOME}/.idris2``. You can change this
|
||||
by editing the options at the beginning of the ``Makefile``. For example,
|
||||
to install into ``/usr/local``, you can edit the ``PREFIX`` as follows::
|
||||
|
||||
PREFIX ?= /usr/local
|
||||
|
||||
To check that installation has succeeded, and to write your first
|
||||
Idris program, create a file called ``hello.idr`` containing the
|
||||
following text:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
module Main
|
||||
|
||||
main : IO ()
|
||||
main = putStrLn "Hello world"
|
||||
|
||||
If you are familiar with Haskell, it should be fairly clear what the
|
||||
program is doing and how it works, but if not, we will explain the
|
||||
details later. You can compile the program to an executable by
|
||||
entering ``idris2 hello.idr -o hello`` at the shell prompt. This will,
|
||||
by default, create an executable called ``hello``, which invokes a generated
|
||||
and compiled Chez Schem program, in the destination directory ``build/exec``
|
||||
which you can run:
|
||||
|
||||
::
|
||||
|
||||
$ idris2 hello.idr -o hello
|
||||
compiling hello.ss with output to hello.so
|
||||
$ ./build/exec/hello.so
|
||||
Hello world
|
||||
|
||||
Please note that the dollar sign ``$`` indicates the shell prompt!
|
||||
Some useful options to the Idris command are:
|
||||
|
||||
- ``-o prog`` to compile to an executable called ``prog``.
|
||||
|
||||
- ``--check`` type check the file and its dependencies without starting the interactive environment.
|
||||
|
||||
- ``--package pkg`` add package as dependency, e.g. ``--package contrib`` to make use of the contrib package.
|
||||
|
||||
- ``--help`` display usage summary and command line options.
|
||||
|
||||
You can find out more about compiling to executables in
|
||||
Section :ref:`sect-execs`.
|
||||
|
||||
The Interactive Environment
|
||||
===========================
|
||||
|
||||
Entering ``idris2`` at the shell prompt starts up the interactive
|
||||
environment. You should see something like the following:
|
||||
|
||||
.. literalinclude:: ../listing/idris-prompt-start.txt
|
||||
|
||||
This gives a ``ghci`` style interface which allows evaluation of, as
|
||||
well as type checking of, expressions; theorem proving, compilation;
|
||||
editing; and various other operations. The command ``:?`` gives a list
|
||||
of supported commands. Below, we see an example run in
|
||||
which ``hello.idr`` is loaded, the type of ``main`` is checked and
|
||||
then the program is compiled to the executable file ``hello``,
|
||||
available in the destination directory ``build/exec/``. Type
|
||||
checking a file, if successful, creates a bytecode version of the file (in this
|
||||
case ``build/ttc/hello.ttc``) to speed up loading in future. The bytecode is
|
||||
regenerated if the source file changes.
|
||||
|
||||
.. _run1:
|
||||
.. literalinclude:: ../listing/idris-prompt-helloworld.txt
|
@ -1,457 +0,0 @@
|
||||
.. _sect-theorems:
|
||||
|
||||
***************
|
||||
Theorem Proving
|
||||
***************
|
||||
|
||||
Equality
|
||||
========
|
||||
|
||||
Idris allows propositional equalities to be declared, allowing theorems about
|
||||
programs to be stated and proved. An equality type is defined as follows in the
|
||||
Prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Equal : a -> b -> Type where
|
||||
Refl : Equal x x
|
||||
|
||||
As a notational convenience, ``Equal x y`` can be written as ``x = y``.
|
||||
Equalities can be proposed between any values of any types, but the only
|
||||
way to construct a proof of equality is if values actually are equal.
|
||||
For example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
fiveIsFive : 5 = 5
|
||||
fiveIsFive = Refl
|
||||
|
||||
twoPlusTwo : 2 + 2 = 4
|
||||
twoPlusTwo = Refl
|
||||
|
||||
If we try...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
twoPlusTwoBad : 2 + 2 = 5
|
||||
twoPlusTwoBad = Refl
|
||||
|
||||
...then we'll get an error:
|
||||
|
||||
::
|
||||
|
||||
Proofs.idr:8:17--10:1:While processing right hand side of Main.twoPlusTwoBad at Proofs.idr:8:1--10:1:
|
||||
When unifying 4 = 4 and (fromInteger 2 + fromInteger 2) = (fromInteger 5)
|
||||
Mismatch between:
|
||||
4
|
||||
and
|
||||
5
|
||||
|
||||
.. _sect-empty:
|
||||
|
||||
The Empty Type
|
||||
==============
|
||||
|
||||
There is an empty type, ``Void``, which has no constructors. It is therefore
|
||||
impossible to construct a canonical element of the empty type. We can therefore
|
||||
use the empty type to prove that something is impossible, for example zero is
|
||||
never equal to a successor:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
disjoint : (n : Nat) -> Z = S n -> Void
|
||||
disjoint n prf = replace {p = disjointTy} prf ()
|
||||
where
|
||||
disjointTy : Nat -> Type
|
||||
disjointTy Z = ()
|
||||
disjointTy (S k) = Void
|
||||
|
||||
Don't worry if you don't get all the details of how this works just yet -
|
||||
essentially, it applies the library function ``replace``, which uses an
|
||||
equality proof to transform a predicate. Here we use it to transform a
|
||||
value of a type which can exist, the empty tuple, to a value of a type
|
||||
which can’t, by using a proof of something which can’t exist.
|
||||
|
||||
Once we have an element of the empty type, we can prove anything.
|
||||
``void`` is defined in the library, to assist with proofs by
|
||||
contradiction.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
void : Void -> a
|
||||
|
||||
Proving Theorems
|
||||
================
|
||||
|
||||
When type checking dependent types, the type itself gets *normalised*.
|
||||
So imagine we want to prove the following theorem about the reduction
|
||||
behaviour of ``plus``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReduces : (n:Nat) -> plus Z n = n
|
||||
|
||||
We’ve written down the statement of the theorem as a type, in just the
|
||||
same way as we would write the type of a program. In fact there is no
|
||||
real distinction between proofs and programs. A proof, as far as we are
|
||||
concerned here, is merely a program with a precise enough type to
|
||||
guarantee a particular property of interest.
|
||||
|
||||
We won’t go into details here, but the Curry-Howard correspondence [#Timothy]_
|
||||
explains this relationship. The proof itself is immediate, because
|
||||
``plus Z n`` normalises to ``n`` by the definition of ``plus``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReduces n = Refl
|
||||
|
||||
It is slightly harder if we try the arguments the other way, because
|
||||
plus is defined by recursion on its first argument. The proof also works
|
||||
by recursion on the first argument to ``plus``, namely ``n``.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesZ : (n:Nat) -> n = plus n Z
|
||||
plusReducesZ Z = Refl
|
||||
plusReducesZ (S k) = cong S (plusReducesZ k)
|
||||
|
||||
``cong`` is a function defined in the library which states that equality
|
||||
respects function application:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
cong : (f : t -> u) -> a = b -> f a = f b
|
||||
|
||||
To see more detail on what's going on, we can replace the recursive call to
|
||||
``plusReducesZ`` with a hole:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesZ (S k) = cong S ?help
|
||||
|
||||
Then inspecting the type of the hole at the REPL shows us:
|
||||
|
||||
::
|
||||
|
||||
Main> :t help
|
||||
k : Nat
|
||||
-------------------------------------
|
||||
help : k = (plus k Z)
|
||||
|
||||
We can do the same for the reduction behaviour of plus on successors:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
|
||||
plusReducesS Z m = Refl
|
||||
plusReducesS (S k) m = cong S (plusReducesS k m)
|
||||
|
||||
Even for small theorems like these, the proofs are a little tricky to
|
||||
construct in one go. When things get even slightly more complicated, it
|
||||
becomes too much to think about to construct proofs in this “batch
|
||||
mode”.
|
||||
|
||||
Idris provides interactive editing capabilities, which can help with
|
||||
building proofs. For more details on building proofs interactively in
|
||||
an editor, see :ref:`proofs-index`.
|
||||
|
||||
.. _sect-parity:
|
||||
|
||||
Theorems in Practice
|
||||
====================
|
||||
|
||||
The need to prove theorems can arise naturally in practice. For example,
|
||||
previously (:ref:`sec-views`) we implemented ``natToBin`` using a function
|
||||
``parity``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
|
||||
We provided a definition for ``parity``, but without explanation. We might
|
||||
have hoped that it would look something like the following:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
parity Z = Even {n=Z}
|
||||
parity (S Z) = Odd {n=Z}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | Even = Even {n=S j}
|
||||
parity (S (S (S (j + j)))) | Odd = Odd {n=S j}
|
||||
|
||||
Unfortunately, this fails with a type error:
|
||||
|
||||
::
|
||||
|
||||
With.idr:26:17--27:3:While processing right hand side of Main.with block in 2419 at With.idr:24:3--27:3:
|
||||
Can't solve constraint between:
|
||||
plus j (S j)
|
||||
and
|
||||
S (plus j j)
|
||||
|
||||
The problem is that normalising ``S j + S j``, in the type of ``Even``
|
||||
doesn't result in what we need for the type of the right hand side of
|
||||
``Parity``. We know that ``S (S (plus j j))`` is going to be equal to
|
||||
``S j + S j``, but we need to explain it to Idris with a proof. We can
|
||||
begin by adding some *holes* (see :ref:`sect-holes`) to the definition:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
parity Z = Even {n=Z}
|
||||
parity (S Z) = Odd {n=Z}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | Even = let result = Even {n=S j} in
|
||||
?helpEven
|
||||
parity (S (S (S (j + j)))) | Odd = let result = Odd {n=S j} in
|
||||
?helpOdd
|
||||
|
||||
Checking the type of ``helpEven`` shows us what we need to prove for the
|
||||
``Even`` case:
|
||||
|
||||
::
|
||||
|
||||
j : Nat
|
||||
result : Parity (S (plus j (S j)))
|
||||
--------------------------------------
|
||||
helpEven : Parity (S (S (plus j j)))
|
||||
|
||||
We can therefore write a helper function to *rewrite* the type to the form
|
||||
we need:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
|
||||
helpEven j p = rewrite plusSuccRightSucc j j in p
|
||||
|
||||
The ``rewrite ... in`` syntax allows you to change the required type of an
|
||||
expression by rewriting it according to an equality proof. Here, we have
|
||||
used ``plusSuccRightSucc``, which has the following type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
|
||||
|
||||
We can see the effect of ``rewrite`` by replacing the right hand side of
|
||||
``helpEven`` with a hole, and working step by step. Beginning with the following:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
|
||||
helpEven j p = ?helpEven_rhs
|
||||
|
||||
We can look at the type of ``helpEven_rhs``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
j : Nat
|
||||
p : Parity (S (plus j (S j)))
|
||||
--------------------------------------
|
||||
helpEven_rhs : Parity (S (S (plus j j)))
|
||||
|
||||
Then we can ``rewrite`` by applying ``plusSuccRightSucc j j``, which gives
|
||||
an equation ``S (j + j) = j + S j``, thus replacing ``S (j + j)`` (or,
|
||||
in this case, ``S (plus j j)`` since ``S (j + j)`` reduces to that) in the
|
||||
type with ``j + S j``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
|
||||
helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs
|
||||
|
||||
Checking the type of ``helpEven_rhs`` now shows what has happened, including
|
||||
the type of the equation we just used (as the type of ``_rewrite_rule``):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> :t helpEven_rhs
|
||||
j : Nat
|
||||
p : Parity (S (plus j (S j)))
|
||||
-------------------------------------
|
||||
helpEven_rhs : Parity (S (plus j (S j)))
|
||||
|
||||
Using ``rewrite`` and another helper for the ``Odd`` case, we can complete
|
||||
``parity`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
|
||||
helpEven j p = rewrite plusSuccRightSucc j j in p
|
||||
|
||||
helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
|
||||
helpOdd j p = rewrite plusSuccRightSucc j j in p
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
parity Z = Even {n=Z}
|
||||
parity (S Z) = Odd {n=Z}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})
|
||||
parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})
|
||||
|
||||
Full details of ``rewrite`` are beyond the scope of this introductory tutorial,
|
||||
but it is covered in the theorem proving tutorial (see :ref:`proofs-index`).
|
||||
|
||||
.. _sect-totality:
|
||||
|
||||
Totality Checking
|
||||
=================
|
||||
|
||||
If we really want to trust our proofs, it is important that they are
|
||||
defined by *total* functions — that is, a function which is defined for
|
||||
all possible inputs and is guaranteed to terminate. Otherwise we could
|
||||
construct an element of the empty type, from which we could prove
|
||||
anything:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
-- making use of 'hd' being partially defined
|
||||
empty1 : Void
|
||||
empty1 = hd [] where
|
||||
hd : List a -> a
|
||||
hd (x :: xs) = x
|
||||
|
||||
-- not terminating
|
||||
empty2 : Void
|
||||
empty2 = empty2
|
||||
|
||||
Internally, Idris checks every definition for totality, and we can check at
|
||||
the prompt with the ``:total`` command. We see that neither of the above
|
||||
definitions is total:
|
||||
|
||||
::
|
||||
|
||||
Void> :total empty1
|
||||
Void.empty1 is not covering due to call to function empty1:hd
|
||||
Void> :total empty2
|
||||
Void.empty2 is possibly not terminating due to recursive path Void.empty2
|
||||
|
||||
Note the use of the word “possibly” — a totality check can never be certain due
|
||||
to the undecidability of the halting problem. The check is, therefore,
|
||||
conservative. It is also possible (and indeed advisable, in the case of proofs)
|
||||
to mark functions as total so that it will be a compile time error for the
|
||||
totality check to fail:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
total empty2 : Void
|
||||
empty2 = empty2
|
||||
|
||||
Reassuringly, our proof in Section :ref:`sect-empty` that the zero and
|
||||
successor constructors are disjoint is total:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> :total disjoint
|
||||
Main.disjoint is Total
|
||||
|
||||
The totality check is, necessarily, conservative. To be recorded as
|
||||
total, a function ``f`` must:
|
||||
|
||||
- Cover all possible inputs
|
||||
|
||||
- Be *well-founded* — i.e. by the time a sequence of (possibly
|
||||
mutually) recursive calls reaches ``f`` again, it must be possible to
|
||||
show that one of its arguments has decreased.
|
||||
|
||||
- Not use any data types which are not *strictly positive*
|
||||
|
||||
- Not call any non-total functions
|
||||
|
||||
Directives and Compiler Flags for Totality
|
||||
------------------------------------------
|
||||
|
||||
[NOTE: Not all of this is implemented yet for Idris 2]
|
||||
|
||||
By default, Idris allows all well-typed definitions, whether total or not.
|
||||
However, it is desirable for functions to be total as far as possible, as this
|
||||
provides a guarantee that they provide a result for all possible inputs, in
|
||||
finite time. It is possible to make total functions a requirement, either:
|
||||
|
||||
- By using the ``--total`` compiler flag.
|
||||
|
||||
- By adding a ``%default total`` directive to a source file. All
|
||||
definitions after this will be required to be total, unless
|
||||
explicitly flagged as ``partial``.
|
||||
|
||||
All functions *after* a ``%default total`` declaration are required to
|
||||
be total. Correspondingly, after a ``%default partial`` declaration, the
|
||||
requirement is relaxed.
|
||||
|
||||
Finally, the compiler flag ``--warnpartial`` causes to print a warning
|
||||
for any undeclared partial function.
|
||||
|
||||
Totality checking issues
|
||||
------------------------
|
||||
|
||||
Please note that the totality checker is not perfect! Firstly, it is
|
||||
necessarily conservative due to the undecidability of the halting
|
||||
problem, so many programs which *are* total will not be detected as
|
||||
such. Secondly, the current implementation has had limited effort put
|
||||
into it so far, so there may still be cases where it believes a function
|
||||
is total which is not. Do not rely on it for your proofs yet!
|
||||
|
||||
Hints for totality
|
||||
------------------
|
||||
|
||||
In cases where you believe a program is total, but Idris does not agree, it is
|
||||
possible to give hints to the checker to give more detail for a termination
|
||||
argument. The checker works by ensuring that all chains of recursive calls
|
||||
eventually lead to one of the arguments decreasing towards a base case, but
|
||||
sometimes this is hard to spot. For example, the following definition cannot be
|
||||
checked as ``total`` because the checker cannot decide that ``filter (< x) xs``
|
||||
will always be smaller than ``(x :: xs)``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
qsort : Ord a => List a -> List a
|
||||
qsort [] = []
|
||||
qsort (x :: xs)
|
||||
= qsort (filter (< x) xs) ++
|
||||
(x :: qsort (filter (>= x) xs))
|
||||
|
||||
The function ``assert_smaller``, defined in the prelude, is intended to
|
||||
address this problem:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
assert_smaller : a -> a -> a
|
||||
assert_smaller x y = y
|
||||
|
||||
It simply evaluates to its second argument, but also asserts to the
|
||||
totality checker that ``y`` is structurally smaller than ``x``. This can
|
||||
be used to explain the reasoning for totality if the checker cannot work
|
||||
it out itself. The above example can now be written as:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
total
|
||||
qsort : Ord a => List a -> List a
|
||||
qsort [] = []
|
||||
qsort (x :: xs)
|
||||
= qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
|
||||
(x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
|
||||
|
||||
The expression ``assert_smaller (x :: xs) (filter (<= x) xs)`` asserts
|
||||
that the result of the filter will always be smaller than the pattern
|
||||
``(x :: xs)``.
|
||||
|
||||
In more extreme cases, the function ``assert_total`` marks a
|
||||
subexpression as always being total:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
assert_total : a -> a
|
||||
assert_total x = x
|
||||
|
||||
In general, this function should be avoided, but it can be very useful
|
||||
when reasoning about primitives or externally defined functions (for
|
||||
example from a C library) where totality can be shown by an external
|
||||
argument.
|
||||
|
||||
|
||||
.. [#Timothy] Timothy G. Griffin. 1989. A formulae-as-type notion of
|
||||
control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
|
||||
symposium on Principles of programming languages (POPL
|
||||
'90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
|
||||
http://doi.acm.org/10.1145/96709.96714
|
File diff suppressed because it is too large
Load Diff
@ -1,156 +0,0 @@
|
||||
.. _sec-views:
|
||||
|
||||
*****************************
|
||||
Views and the “``with``” rule
|
||||
*****************************
|
||||
|
||||
[NOT UPDATED FOR IDRIS 2 YET]
|
||||
|
||||
Dependent pattern matching
|
||||
==========================
|
||||
|
||||
Since types can depend on values, the form of some arguments can be
|
||||
determined by the value of others. For example, if we were to write
|
||||
down the implicit length arguments to ``(++)``, we’d see that the form
|
||||
of the length argument was determined by whether the vector was empty
|
||||
or not:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
(++) : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
(++) {n=Z} [] ys = ys
|
||||
(++) {n=S k} (x :: xs) ys = x :: xs ++ ys
|
||||
|
||||
If ``n`` was a successor in the ``[]`` case, or zero in the ``::``
|
||||
case, the definition would not be well typed.
|
||||
|
||||
.. _sect-nattobin:
|
||||
|
||||
The ``with`` rule — matching intermediate values
|
||||
================================================
|
||||
|
||||
Very often, we need to match on the result of an intermediate
|
||||
computation. Idris provides a construct for this, the ``with``
|
||||
rule, inspired by views in ``Epigram`` [#McBridgeMcKinna]_, which takes account of
|
||||
the fact that matching on a value in a dependently typed language can
|
||||
affect what we know about the forms of other values. In its simplest
|
||||
form, the ``with`` rule adds another argument to the function being
|
||||
defined.
|
||||
|
||||
We have already seen a vector filter function. This time, we define it
|
||||
using ``with`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
|
||||
filter p [] = ( _ ** [] )
|
||||
filter p (x :: xs) with (filter p xs)
|
||||
filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
|
||||
|
||||
Here, the ``with`` clause allows us to deconstruct the result of
|
||||
``filter p xs``. The view refined argument pattern ``filter p (x ::
|
||||
xs)`` goes beneath the ``with`` clause, followed by a vertical bar
|
||||
``|``, followed by the deconstructed intermediate result ``( _ ** xs'
|
||||
)``. If the view refined argument pattern is unchanged from the
|
||||
original function argument pattern, then the left side of ``|`` is
|
||||
extraneous and may be omitted:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
filter p (x :: xs) with (filter p xs)
|
||||
| ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
|
||||
|
||||
``with`` clauses can also be nested:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
foo : Int -> Int -> Bool
|
||||
foo n m with (n + 1)
|
||||
foo _ m | 2 with (m + 1)
|
||||
foo _ _ | 2 | 3 = True
|
||||
foo _ _ | 2 | _ = False
|
||||
foo _ _ | _ = False
|
||||
|
||||
If the intermediate computation itself has a dependent type, then the
|
||||
result can affect the forms of other arguments — we can learn the form
|
||||
of one value by testing another. In these cases, view refined argument
|
||||
patterns must be explicit. For example, a ``Nat`` is either even or
|
||||
odd. If it is even it will be the sum of two equal ``Nat``.
|
||||
Otherwise, it is the sum of two equal ``Nat`` plus one:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Parity : Nat -> Type where
|
||||
Even : {n : _} -> Parity (n + n)
|
||||
Odd : {n : _} -> Parity (S (n + n))
|
||||
|
||||
We say ``Parity`` is a *view* of ``Nat``. It has a *covering function*
|
||||
which tests whether it is even or odd and constructs the predicate
|
||||
accordingly. Note that we're going to need access to ``n`` at run time, so
|
||||
although it's an implicit argument, it has unrestricted multiplicity.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity : (n:Nat) -> Parity n
|
||||
|
||||
We’ll come back to the definition of ``parity`` shortly. We can use it
|
||||
to write a function which converts a natural number to a list of
|
||||
binary digits (least significant first) as follows, using the ``with``
|
||||
rule:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
natToBin : Nat -> List Bool
|
||||
natToBin Z = Nil
|
||||
natToBin k with (parity k)
|
||||
natToBin (j + j) | Even = False :: natToBin j
|
||||
natToBin (S (j + j)) | Odd = True :: natToBin j
|
||||
|
||||
The value of ``parity k`` affects the form of ``k``, because the
|
||||
result of ``parity k`` depends on ``k``. So, as well as the patterns
|
||||
for the result of the intermediate computation (``Even`` and ``Odd``)
|
||||
right of the ``|``, we also write how the results affect the other
|
||||
patterns left of the ``|``. That is:
|
||||
|
||||
- When ``parity k`` evaluates to ``Even``, we can refine the original
|
||||
argument ``k`` to a refined pattern ``(j + j)`` according to
|
||||
``Parity (n + n)`` from the ``Even`` constructor definition. So
|
||||
``(j + j)`` replaces ``k`` on the left side of ``|``, and the
|
||||
``Even`` constructor appears on the right side. The natural number
|
||||
``j`` in the refined pattern can be used on the right side of the
|
||||
``=`` sign.
|
||||
|
||||
- Otherwise, when ``parity k`` evaluates to ``Odd``, the original
|
||||
argument ``k`` is refined to ``S (j + j)`` according to ``Parity (S
|
||||
(n + n))`` from the ``Odd`` constructor definition, and ``Odd`` now
|
||||
appears on the right side of ``|``, again with the natural number
|
||||
``j`` used on the right side of the ``=`` sign.
|
||||
|
||||
Note that there is a function in the patterns (``+``) and repeated
|
||||
occurrences of ``j`` - this is allowed because another argument has
|
||||
determined the form of these patterns.
|
||||
|
||||
Defining ``parity``
|
||||
===================
|
||||
|
||||
The definition of ``parity`` is a little tricky, and requires some knowledge of
|
||||
theorem proving (see Section :ref:`sect-theorems`), but for completeness, here
|
||||
it is:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
parity : (n : Nat) -> Parity n
|
||||
parity Z = Even {n = Z}
|
||||
parity (S Z) = Odd {n = Z}
|
||||
parity (S (S k)) with (parity k)
|
||||
parity (S (S (j + j))) | Even
|
||||
= rewrite plusSuccRightSucc j j in Even {n = S j}
|
||||
parity (S (S (S (j + j)))) | Odd
|
||||
= rewrite plusSuccRightSucc j j in Odd {n = S j}
|
||||
|
||||
For full details on ``rewrite`` in particular, please refer to the theorem
|
||||
proving tutorial, in Section :ref:`proofs-index`.
|
||||
|
||||
.. [#McBridgeMcKinna] Conor McBride and James McKinna. 2004. The view from the
|
||||
left. J. Funct. Program. 14, 1 (January 2004),
|
||||
69-111. https://doi.org/10.1017/S0956796803004829
|
@ -1,456 +0,0 @@
|
||||
.. _typedd-index:
|
||||
|
||||
Type Driven Development with Idris: Updates Required
|
||||
====================================================
|
||||
|
||||
The code in the book `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>`_, will mostly work
|
||||
in Idris 2, with some small changes as detailed in this document. The updated
|
||||
code is also [going to be] part of the test suite (see `tests/typedd-book
|
||||
<https://github.com/edwinb/Idris2/tree/master/tests/typedd-book>`_ in the Idris
|
||||
2 source).
|
||||
|
||||
If you are new to Idris, and learning from the book, we recommend working
|
||||
through the first 3-4 chapters with Idris 1, to avoid the need to worry about
|
||||
the changes described here. After that, refer to this document for any
|
||||
necessary changes.
|
||||
|
||||
Chapter 1
|
||||
---------
|
||||
|
||||
No changes necessary
|
||||
|
||||
Chapter 2
|
||||
---------
|
||||
|
||||
The Prelude is smaller than Idris 1, and many functions have been moved to
|
||||
the base libraries instead. So:
|
||||
|
||||
In ``Average.idr``, add:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import Data.Strings -- for `words`
|
||||
import Data.List -- for `length` on lists
|
||||
|
||||
In ``AveMain.idr`` and ``Reverse.idr`` add:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import System.REPL -- for 'repl'
|
||||
|
||||
Chapter 3
|
||||
---------
|
||||
|
||||
Unbound implicits have multiplicity 0, so we can't match on them at run-time.
|
||||
Therefore, in ``Matrix.idr``, we need to change the type of ``createEmpties``
|
||||
and ``transposeMat`` so that the length of the inner vector is available to
|
||||
match on:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
createEmpties : {n : _} -> Vect n (Vect 0 elem)
|
||||
transposeMat : {n : _} -> Vect m (Vect n elem) -> Vect n (Vect m elem)
|
||||
|
||||
Chapter 4
|
||||
---------
|
||||
|
||||
For the reasons described above:
|
||||
|
||||
+ In ``DataStore.idr``, add ``import System.REPL`` and ``import Data.Strings``
|
||||
+ In ``SumInputs.idr``, add ``import System.REPL``
|
||||
+ In ``TryIndex.idr``, add an implicit argument:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
tryIndex : {n : _} -> Integer -> Vect n a -> Maybe a
|
||||
|
||||
Chapter 5
|
||||
---------
|
||||
|
||||
There is no longer a ``Cast`` instance from ``String`` to ``Nat``, because its
|
||||
behaviour of returing Z if the ``String`` wasn't numeric was thought to be
|
||||
confusing and potentially error prone. Instead, there is ``stringToNatOrZ`` in
|
||||
``Data.Strings`` which at least has a clearer name. So:
|
||||
|
||||
In ``Loops.idr`` and ``ReadNum.idr`` add ``import Data.Strings`` and change ``cast`` to
|
||||
``stringToNatOrZ``
|
||||
|
||||
Chapter 6
|
||||
---------
|
||||
|
||||
In ``DataStore.idr`` and ``DataStoreHoles.idr``, add ``import Data.Strings`` and
|
||||
``import System.REPL``. Also in ``DataStore.idr``, the ``schema`` argument to
|
||||
``display`` is required for matching, so change the type to:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
display : {schema : _} -> SchemaType schema -> String
|
||||
|
||||
In ``TypeFuns.idr`` add ``import Data.Strings``
|
||||
|
||||
Chapter 7
|
||||
---------
|
||||
|
||||
``Abs`` is now a separate interface from ``Neg``. So, change the type of ``eval``
|
||||
to include ``Abs`` specifically:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
eval : (Abs num, Neg num, Integral num) => Expr num -> num
|
||||
|
||||
Also, take ``abs`` out of the ``Neg`` implementation for ``Expr`` and add an
|
||||
implementation of ``Abs`` as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Abs ty => Abs (Expr ty) where
|
||||
abs = Abs
|
||||
|
||||
Chapter 8
|
||||
---------
|
||||
|
||||
In ``AppendVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs
|
||||
|
||||
``cong`` now takes an explicit argument for the function to apply. So, in
|
||||
``CheckEqMaybe.idr`` change the last case to:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
checkEqNat (S k) (S j) = case checkEqNat k j of
|
||||
Nothing => Nothing
|
||||
Just prf => Just (cong S prf)
|
||||
|
||||
A similar change is necessary in ``CheckEqDec.idr``.
|
||||
|
||||
In ``ExactLength.idr``, the ``m`` argument to ``exactLength`` is needed at run time,
|
||||
so change its type to:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
exactLength : {m : _} ->
|
||||
(len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
|
||||
|
||||
A similar change is necessary in ``ExactLengthDec.idr``. Also, ``DecEq`` is no
|
||||
longer part of the prelude, so add ``import Decidable.Equality``.
|
||||
|
||||
In ``ReverseVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs.
|
||||
|
||||
Chapter 9
|
||||
---------
|
||||
|
||||
+ In ``ElemType.idr``, add ``import Decidable.Equality``
|
||||
|
||||
In ``Hangman.idr``:
|
||||
|
||||
+ Add ``import Decidable.Equality`` and ``import Data.Strings``
|
||||
+ ``removeElem`` pattern matches on ``n``, so it needs to be written in its
|
||||
type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
removeElem : {n : _} ->
|
||||
(value : a) -> (xs : Vect (S n) a) ->
|
||||
{auto prf : Elem value xs} ->
|
||||
Vect n a
|
||||
|
||||
+ ``letters`` is used by ``processGuess``, because it's passed to ``removeElem``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
processGuess : {letters : _} ->
|
||||
(letter : Char) -> WordState (S guesses) (S letters) ->
|
||||
Either (WordState guesses (S letters))
|
||||
(WordState (S guesses) letters)
|
||||
|
||||
+ ``guesses`` and ``letters`` are implicit arguments to ``game``, but are used by the
|
||||
definition, so add them to its type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
game : {guesses : _} -> {letters : _} ->
|
||||
WordState (S guesses) (S letters) -> IO Finished
|
||||
|
||||
In ``RemoveElem.idr``
|
||||
|
||||
+ ``removeElem`` needs to be updated as above.
|
||||
|
||||
Chapter 10
|
||||
----------
|
||||
|
||||
Lots of changes necessary here, at least when constructing views, due to Idris
|
||||
2 having a better (that is, more precise and correct!) implementation of
|
||||
unification, and the rules for recursive ``with`` application being tightened up.
|
||||
|
||||
In ``MergeSort.idr``, add ``import Data.List``
|
||||
|
||||
In ``MergeSortView.idr``, add ``import Data.List``, and make the arguments to the
|
||||
views explicit:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
mergeSort : Ord a => List a -> List a
|
||||
mergeSort input with (splitRec input)
|
||||
mergeSort [] | SplitRecNil = []
|
||||
mergeSort [x] | SplitRecOne x = [x]
|
||||
mergeSort (lefts ++ rights) | (SplitRecPair lefts rights lrec rrec)
|
||||
= merge (mergeSort lefts | lrec)
|
||||
(mergeSort rights | rrec)
|
||||
|
||||
In ``SnocList.idr``, in ``my_reverse``, the link between ``Snoc rec`` and ``xs ++ [x]``
|
||||
needs to be made explicit. Idris 1 would happily decide that ``xs`` and ``x`` were
|
||||
the relevant implicit arguments to ``Snoc`` but this was little more than a guess
|
||||
based on what would make it type check, whereas Idris 2 is more precise in
|
||||
what it allows to unify. So, ``x`` and ``xs`` need to be explicit arguments to
|
||||
``Snoc``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data SnocList : List a -> Type where
|
||||
Empty : SnocList []
|
||||
Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x])
|
||||
|
||||
Correspondingly, they need to be explicit when matching. For example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
my_reverse : List a -> List a
|
||||
my_reverse input with (snocList input)
|
||||
my_reverse [] | Empty = []
|
||||
my_reverse (xs ++ [x]) | (Snoc x xs rec) = x :: my_reverse xs | rec
|
||||
|
||||
Similar changes are necessary in ``snocListHelp`` and ``my_reverse_help``. See
|
||||
tests/typedd-book/chapter10/SnocList.idr for the full details.
|
||||
|
||||
Also, in ``snocListHelp``, ``input`` is used at run time so needs to be bound
|
||||
in the type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
snocListHelp : {input : _} ->
|
||||
(snoc : SnocList input) -> (rest : List a) -> SnocList (input +
|
||||
|
||||
It's no longer necessary to give ``{input}`` explicitly in the patterns for
|
||||
``snocListHelp``, although it's harmless to do so.
|
||||
|
||||
In ``IsSuffix.idr``, the matching has to be written slightly differently. The
|
||||
recursive with application in Idris 1 probably shouldn't have allowed this!
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
isSuffix : Eq a => List a -> List a -> Bool
|
||||
isSuffix input1 input2 with (snocList input1, snocList input2)
|
||||
isSuffix [] input2 | (Empty, s) = True
|
||||
isSuffix input1 [] | (s, Empty) = False
|
||||
isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec, Snoc ysrec)
|
||||
= if x == y
|
||||
then isSuffix xs ys | (xsrec, ysrec)
|
||||
else False
|
||||
|
||||
This doesn't yet get past the totality checker, however, because it doesn't
|
||||
know about looking inside pairs.
|
||||
|
||||
In ``DataStore.idr``: Well this is embarrassing - I've no idea how Idris 1 lets
|
||||
this through! I think perhaps it's too "helpful" when solving unification
|
||||
problems. To fix it, add an extra parameter ``schema`` to ``StoreView``, and change
|
||||
the type of ``SNil`` to be explicit that the ``empty`` is the function defined in
|
||||
``DataStore``. Also add ``entry`` and ``store`` as explicit arguments to ``SAdd``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data StoreView : (schema : _) -> DataStore schema -> Type where
|
||||
SNil : StoreView schema DataStore.empty
|
||||
SAdd : (entry, store : _) -> (rec : StoreView schema store) ->
|
||||
StoreView schema (addToStore entry store)
|
||||
|
||||
Since ``size`` is as explicit argument in the ``DataStore`` record, it also needs
|
||||
to be relevant in the type of ``storeViewHelp``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
storeViewHelp : {size : _} ->
|
||||
(items : Vect size (SchemaType schema)) ->
|
||||
StoreView schema (MkData size items)
|
||||
|
||||
In ``TestStore.idr``:
|
||||
|
||||
+ In ``listItems``, ``empty`` needs to be ``DataStore.empty`` to be explicit that you
|
||||
mean the function
|
||||
+ In ``filterKeys``, there is an error in the ``SNil`` case, which wasn't caught
|
||||
because of the type of ``SNil`` above. It should be:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
filterKeys test DataStore.empty | SNil = []
|
||||
|
||||
Chapter 11
|
||||
----------
|
||||
|
||||
In ``Streams.idr`` add ``import Data.Stream`` for ``iterate``.
|
||||
|
||||
In ``Arith.idr`` and ``ArithTotal.idr``, the ``Divides`` view now has explicit
|
||||
arguments for the dividend and remainder, so they need to be explicit in
|
||||
``bound``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
bound : Int -> Int
|
||||
bound x with (divides x 12)
|
||||
bound ((12 * div) + rem) | (DivBy div rem prf) = rem + 1
|
||||
|
||||
In ``ArithCmd.idr``, update ``DivBy`` as above. Also add ``import Data.Strings`` for
|
||||
``Strings.toLower``.
|
||||
|
||||
In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also,
|
||||
since export rules are per-namespace now, rather than per-file, you need to
|
||||
export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
|
||||
|
||||
Chapter 12
|
||||
----------
|
||||
|
||||
For reasons described above: In ``ArithState.idr``, add ``import Data.Strings``.
|
||||
Also the ``(>>=)`` operators need to be set as ``export`` since they are in their
|
||||
own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional
|
||||
arguments ``div`` and ``rem``.
|
||||
|
||||
Chapter 13
|
||||
----------
|
||||
|
||||
In ``StackIO.idr``:
|
||||
|
||||
+ ``tryAdd`` pattern matches on ``height``, so it needs to be written in its
|
||||
type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
tryAdd : {height : _} -> StackIO height
|
||||
|
||||
+ ``height`` is also an implicit argument to ``stackCalc``, but is used by the
|
||||
definition, so add it to its type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
stackCalc : {height : _} -> StackIO height
|
||||
|
||||
+ In ``StackDo`` namespace, export ``(>>=)``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
namespace StackDo
|
||||
export
|
||||
(>>=) : StackCmd a height1 height2 ->
|
||||
(a -> Inf (StackIO height2)) -> StackIO height1
|
||||
(>>=) = Do
|
||||
|
||||
In ``Vending.idr``:
|
||||
|
||||
+ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``strToInput``
|
||||
+ In ``MachineCmd`` type, add an implicit argument to ``(>>=)`` data constructor:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
(>>=) : {state2 : _} ->
|
||||
MachineCmd a state1 state2 ->
|
||||
(a -> MachineCmd b state2 state3) ->
|
||||
MachineCmd b state1 state3
|
||||
|
||||
+ In ``MachineIO`` type, add an implicit argument to ``Do`` data constructor:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data MachineIO : VendState -> Type where
|
||||
Do : {state1 : _} ->
|
||||
MachineCmd a state1 state2 ->
|
||||
(a -> Inf (MachineIO state2)) -> MachineIO state1
|
||||
|
||||
+ ``runMachine`` pattern matches on ``inState``, so it needs to be written in its
|
||||
type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty
|
||||
|
||||
+ In ``MachineDo`` namespace, add an implicit argument to ``(>>=)`` and export it:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
namespace MachineDo
|
||||
export
|
||||
(>>=) : {state1 : _} ->
|
||||
MachineCmd a state1 state2 ->
|
||||
(a -> Inf (MachineIO state2)) -> MachineIO state1
|
||||
(>>=) = Do
|
||||
|
||||
+ ``vend`` and ``refill`` pattern match on ``pounds`` and ``chocs``, so they need to be written in
|
||||
their type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
|
||||
refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs)
|
||||
|
||||
+ ``pounds`` and ``chocs`` are implicit arguments to ``machineLoop``, but are used by the
|
||||
definition, so add them to its type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
|
||||
|
||||
Chapter 14
|
||||
----------
|
||||
|
||||
In ``ATM.idr``:
|
||||
|
||||
+ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``runATM``
|
||||
|
||||
In ``ATM.idr``, add:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import Data.Strings -- for `toUpper`
|
||||
import Data.List -- for `nub`
|
||||
|
||||
+ In ``Loop`` namespace, export ``GameLoop`` type and its data constructors:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
namespace Loop
|
||||
public export
|
||||
data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
|
||||
(>>=) : GameCmd a state1 state2_fn ->
|
||||
((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) ->
|
||||
GameLoop b state1 state3_fn
|
||||
Exit : GameLoop () NotRunning (const NotRunning)
|
||||
|
||||
+ ``letters`` and ``guesses`` are used by ``gameLoop``, so they need to be written in its type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
gameLoop : {letters : _} -> {guesses : _} ->
|
||||
GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
|
||||
|
||||
+ In ``Game`` type, add an implicit argument ``letters`` to ``InProgress`` data constructor:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Game : GameState -> Type where
|
||||
GameStart : Game NotRunning
|
||||
GameWon : (word : String) -> Game NotRunning
|
||||
GameLost : (word : String) -> Game NotRunning
|
||||
InProgress : {letters : _} -> (word : String) -> (guesses : Nat) ->
|
||||
(missing : Vect letters Char) -> Game (Running guesses letters)
|
||||
|
||||
+ ``removeElem`` pattern matches on ``n``, so it needs to be written in its type:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
removeElem : {n : _} ->
|
||||
(value : a) -> (xs : Vect (S n) a) ->
|
||||
{auto prf : Elem value xs} ->
|
||||
Vect n a
|
||||
|
||||
Chapter 15
|
||||
----------
|
||||
|
||||
TODO
|
@ -1,659 +0,0 @@
|
||||
.. _updates-index:
|
||||
|
||||
#####################
|
||||
Changes since Idris 1
|
||||
#####################
|
||||
|
||||
Idris 2 is mostly backwards compatible with Idris 1, with some minor
|
||||
exceptions. This document describes the changes, approximately in order of
|
||||
likelihood of encountering them in practice. New features are described at
|
||||
the end, in Section :ref:`sect-new-features`.
|
||||
|
||||
The Section :ref:`typedd-index` describes how these changes affect the code
|
||||
in the book `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>`_.
|
||||
|
||||
.. note::
|
||||
The documentation for Idris has been published under the Creative
|
||||
Commons CC0 License. As such to the extent possible under law, *The
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
New Core Language: Quantities in Types
|
||||
======================================
|
||||
|
||||
Idris 2 is based on `Quantitative Type Theory (QTT)
|
||||
<https://bentnib.org/quantitative-type-theory.html>`_, a core language
|
||||
developed by Bob Atkey and Conor McBride. In practice, this means that every
|
||||
variable in Idris 2 has a *quantity* associated with it. A quantity is one of:
|
||||
|
||||
* ``0``, meaning that the variable is *erased* at run time
|
||||
* ``1``, meaning that the variable is used *exactly once* at run time
|
||||
* *Unrestricted*, which is the same behaviour as Idris 1
|
||||
|
||||
For more details on this, see Section :ref:`sect-multiplicities`. In practice,
|
||||
this might cause some Idris 1 programs not to type check in Idris 2 due to
|
||||
attempting to use an argument which is erased at run time.
|
||||
|
||||
Erasure
|
||||
-------
|
||||
|
||||
In Idris, names which begin with a lower case later are automatically bound
|
||||
as implicit arguments in types, for example in the following skeleton
|
||||
definition, ``n``, ``a`` and ``m`` are implicitly bound:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
append xs ys = ?append_rhs
|
||||
|
||||
One of the difficulties in compiling a dependently typed programming language
|
||||
is deciding which arguments are used at run time and which can safely be
|
||||
erased. More importantly, it's one of the difficulties when programming: how
|
||||
can a programmer *know* when an argument will be erased?
|
||||
|
||||
In Idris 2, a variable's quantity tells us whether it will be available at
|
||||
run time or not. We can see the quantities of the variables in scope in
|
||||
``append_rhs`` by inspecting the hole at the REPL:
|
||||
|
||||
::
|
||||
|
||||
Main> :t append_rhs
|
||||
0 m : Nat
|
||||
0 a : Type
|
||||
0 n : Nat
|
||||
ys : Vect m a
|
||||
xs : Vect n a
|
||||
-------------------------------------
|
||||
append_rhs : Vect (plus n m) a
|
||||
|
||||
The ``0`` next to ``m``, ``a`` and ``n`` mean that they are in scope, but there
|
||||
will be ``0`` occurrences at run-time. That is, it is *guaranteed* that they
|
||||
will be erased at run-time.
|
||||
|
||||
This does lead to some potential difficulties when converting Idris 1 programs,
|
||||
if you are using implicit arguments at run time. For example, in Idris 1 you
|
||||
can get the length of a vector as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vlen : Vect n a -> Nat
|
||||
vlen {n} xs = n
|
||||
|
||||
This might seem like a good idea, since it runs in constant time and takes
|
||||
advantage of the type level information, but the trade off is that ``n`` has to
|
||||
be available at run time, so at run time we always need the length of the
|
||||
vector to be available if we ever call ``vlen``. Idris 1 can infer whether the
|
||||
length is needed, but there's no easy way for a programmer to be sure.
|
||||
|
||||
In Idris 2, we need to state explicitly that ``n`` is needed at run time
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vlen : {n : Nat} -> Vect n a -> Nat
|
||||
vlen xs = n
|
||||
|
||||
(Incidentally, also note that in Idris 2, names bound in types are also available
|
||||
in the definition without explicitly rebinding them.)
|
||||
|
||||
This also means that when you call ``vlen``, you need the length available. For
|
||||
example, this will give an error
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sumLengths : Vect m a -> Vect n a —> Nat
|
||||
sumLengths xs ys = vlen xs + vlen ys
|
||||
|
||||
Idris 2 reports::
|
||||
|
||||
vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
|
||||
m is not accessible in this context
|
||||
|
||||
This means that it needs to use ``m`` as an argument to pass to ``vlen xs``,
|
||||
where it needs to be available at run time, but ``m`` is not available in
|
||||
``sumLengths`` because it has multiplicity ``0``.
|
||||
|
||||
We can see this more clearly by replacing the right hand side of
|
||||
``sumLengths`` with a hole...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sumLengths : Vect m a -> Vect n a -> Nat
|
||||
sumLengths xs ys = ?sumLengths_rhs
|
||||
|
||||
...then checking the hole's type at the REPL::
|
||||
|
||||
Main> :t sumLengths_rhs
|
||||
0 n : Nat
|
||||
0 a : Type
|
||||
0 m : Nat
|
||||
ys : Vect n a
|
||||
xs : Vect m a
|
||||
-------------------------------------
|
||||
sumLengths_rhs : Nat
|
||||
|
||||
Instead, we need to give bindings for ``m`` and ``n`` with
|
||||
unrestricted multiplicity
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
|
||||
sumLengths xs ys = vLen xs + vLen xs
|
||||
|
||||
Remember that giving no multiplicity on a binder, as with ``m`` and ``n`` here,
|
||||
means that the variable has unrestricted usage.
|
||||
|
||||
If you're converting Idris 1 programs to work with Idris 2, this is probably the
|
||||
biggest thing you need to think about. It is important to note,
|
||||
though, that if you have bound implicits, such as...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
excitingFn : {t : _} -> Coffee t -> Moonbase t
|
||||
|
||||
...then it's a good idea to make sure ``t`` really is needed, or performance
|
||||
might suffer due to the run time building the instance of ``t`` unnecessarily!
|
||||
|
||||
One final note on erasure: it is an error to try to pattern match on an
|
||||
argument with multiplicity ``0``, unless its value is inferrable from
|
||||
elsewhere. So, the following definition is rejected
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
badNot : (0 x : Bool) -> Bool
|
||||
badNot False = True
|
||||
badNot True = False
|
||||
|
||||
This is rejected with the error::
|
||||
|
||||
badnot.idr:2:1--3:1:Attempt to match on erased argument False in
|
||||
Main.badNot
|
||||
|
||||
The following, however, is fine, because in ``sNot``, even though we appear
|
||||
to match on the erased argument ``x``, its value is uniquely inferrable from
|
||||
the type of the second argument
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data SBool : Bool -> Type where
|
||||
SFalse : SBool False
|
||||
STrue : SBool True
|
||||
|
||||
sNot : (0 x : Bool) -> SBool x -> Bool
|
||||
sNot False SFalse = True
|
||||
sNot True STrue = False
|
||||
|
||||
Experience with Idris 2 so far suggests that, most of the time, as long as
|
||||
you're using unbound implicits in your Idris 1 programs, they will work without
|
||||
much modification in Idris 2. The Idris 2 type checker will point out where you
|
||||
require an unbound implicit argument at run time - sometimes this is both
|
||||
surprising and enlightening!
|
||||
|
||||
|
||||
Linearity
|
||||
---------
|
||||
|
||||
Full details on linear arguments with multiplicity ``1`` are given in Section
|
||||
:ref:`sect-multiplicities`. In brief, the intuition behind multiplicity ``1`` is
|
||||
that if we have a function with a type of the following form...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
f : (1 x : a) -> b
|
||||
|
||||
...then the guarantee given by the type system is that *if* ``f x`` *is used
|
||||
exactly once, then* ``x`` *is used exactly once* in the process.
|
||||
|
||||
Prelude and ``base`` libraries
|
||||
==============================
|
||||
|
||||
The Prelude in Idris 1 contained a lot of definitions, many of them rarely
|
||||
necessary. The philosophy in Idris 2 is different. The (rather vaguely
|
||||
specified) rule of thumb is that it should contain the basic functions
|
||||
required by almost any non-trivial program.
|
||||
|
||||
This is a vague specification since different programmers will consider
|
||||
different things absolutely necessary, but the result is that it contains:
|
||||
|
||||
- Anything the elaborator can desugar to (e.g. tuples, ``()``, ``=``)
|
||||
- Basic types ``Bool``, ``Nat``, ``List``, ``Stream``, ``Dec``, ``Maybe``,
|
||||
``Either``
|
||||
- The most important utility functions: ``id``, ``the``, composition, etc
|
||||
- Interfaces for arithmetic and implementations for the primitives and
|
||||
basic types
|
||||
- Basic ``Char`` and ``String`` manipulation
|
||||
- ``Show``, ``Eq``, ``Ord``, and implementations for all types in the prelude
|
||||
- Interfaces and functions for basic proof (``cong``, ``Uninhabited``, etc)
|
||||
- ``Semigroup``, ``Monoid``
|
||||
- ``Functor``, ``Applicative``, ``Monad`` and related functions
|
||||
- ``Foldable``, ``Alternative`` and ``Traversable``
|
||||
- ``Enum``, for list range syntax
|
||||
- Console ``IO``
|
||||
|
||||
Anything which doesn't fit in here has been moved to the ``base`` libraries.
|
||||
Among other places, you can find some of the functions which used to be
|
||||
in the prelude in:
|
||||
|
||||
- ``Data.List`` and ``Data.Nat``
|
||||
- ``Data.Maybe`` and ``Data.Either``
|
||||
- ``System.File`` and ``System.Directory``, (file management was previously
|
||||
part of the prelude)
|
||||
- ``Decidable.Equality``
|
||||
|
||||
Smaller Changes
|
||||
===============
|
||||
|
||||
Ambiguous Name Resolution
|
||||
-------------------------
|
||||
|
||||
Idris 1 worked very hard to resolve ambiguous names, by type, even if this
|
||||
involved some complicated interaction with interface resolution. This could
|
||||
sometimes be the cause of long type checking times. Idris 2 simplifies this, at
|
||||
the cost of sometimes requiring more programmer annotations on ambiguous
|
||||
names.
|
||||
|
||||
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.
|
||||
It will postpone resolution if a name can't be resolved immediately, but unlike
|
||||
Idris 1, it won't attempt significant backtracking. If you have deeply nested
|
||||
ambiguous names (beyond a small threshold, default 3) Idris 2 will report an
|
||||
error. You can change this threshold with a directive, for example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
%ambiguity_depth 10
|
||||
|
||||
However, in such circumstances it is almost certainly a better idea to
|
||||
disambiguate explicitly.
|
||||
|
||||
Indeed in general, if you get an ambiguous name error, the best approach is to
|
||||
give the namespace explicitly. You can also rebind names locally:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> let (::) = Prelude.(::) in [1,2,3]
|
||||
[1, 2, 3]
|
||||
|
||||
One difficulty which remains is resolving ambiguous names where one possibility
|
||||
is an interface method, and another is a concrete top level function.
|
||||
For example, we may have:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b
|
||||
LinearIO.(>>=) : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
|
||||
|
||||
As a pragmatic choice, if type checking in a context where the more concrete
|
||||
name is valid (``LinearIO.(>>=)`` here, so if type checking an expression known
|
||||
to have type ``IO t`` for some ``t``), the more concrete name will be chosen.
|
||||
|
||||
This is somehow unsatisfying, so we may revisit this in future!
|
||||
|
||||
Modules, namespaces and export
|
||||
------------------------------
|
||||
|
||||
The visibility rules, as controlled by the ``private``, ``export`` and
|
||||
``public export`` modifiers, now refer to the visibility of names from
|
||||
other *namespaces*, rather than other *files*.
|
||||
|
||||
So if you have the following, all in the same file...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
namespace A
|
||||
private
|
||||
aHidden : Int -> Int
|
||||
aHidden x = x * 2
|
||||
|
||||
export
|
||||
aVisible : Int -> Int
|
||||
aVisibile x = aHidden x
|
||||
|
||||
mamespace B
|
||||
export
|
||||
bVisible : Int -> Int
|
||||
bVisible x = aVisible (x * 2)
|
||||
|
||||
...then ``bVisible`` can access ``aVisible``, but not ``aHidden``.
|
||||
|
||||
Records are, as before, defined in their own namespace, but fields are always
|
||||
visible from the parent namespace.
|
||||
|
||||
Also, module names must now match the filename in which they're defined, with
|
||||
the exception of the module ``Main``, which can be defined in a file with
|
||||
any name.
|
||||
|
||||
``%language`` pragmas
|
||||
---------------------
|
||||
|
||||
There are several ``%language`` pragmas in Idris 1, which define various
|
||||
experimental extensions. None of these are available in Idris 2, although
|
||||
extensions may be defined in the future.
|
||||
|
||||
``let`` bindings
|
||||
----------------
|
||||
|
||||
``let`` bindings, i.e. expressions of the form ``let x = val in e`` have
|
||||
slightly different behaviour. Previously, you could rely on the computational
|
||||
behaviour of ``x`` in the scope of ``e``, so type checking could take into
|
||||
account that ``x`` reduces to ``val``. Unfortunately, this leads to complications
|
||||
with ``case`` and ``with`` clauses: if we want to preserve the computational
|
||||
behaviour, we would need to make significant changes to the way ``case`` and
|
||||
``with`` are elaborated.
|
||||
|
||||
So, for simplicity and consistency (and, realistically, because I don't have
|
||||
enough time to resolve the problem for ``case`` and ``with``) the above
|
||||
expression ``let x = val in e`` is equivalent to ``(\x => e) val``.
|
||||
|
||||
So, ``let`` now effectively generalises a complex subexpression.
|
||||
If you do need the computational behaviour of a definition, it is now possible
|
||||
using local function definitions instead - see Section :ref:`sect-local-defs`
|
||||
below.
|
||||
|
||||
``auto``-implicits and Interfaces
|
||||
---------------------------------
|
||||
|
||||
Interfaces and ``auto``-implicit arguments are similar, in that they invoke an
|
||||
expression search mechanism to find the value of an argument. In Idris 1,
|
||||
they were implemented separately, but in Idris 2, they use the same mechanism.
|
||||
Consider the following *total* definition of ``fromMaybe``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data IsJust : Maybe a -> Type where
|
||||
ItIsJust : IsJust (Just val)
|
||||
|
||||
fromMaybe : (x : Maybe a) -> {auto p : IsJust x} -> a
|
||||
fromMaybe (Just x) {p = ItIsJust} = x
|
||||
|
||||
Since interface resolution and ``auto``-implicits are now the same thing,
|
||||
the type of ``fromMaybe`` can be written as:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
fromMaybe : (x : Maybe a) -> IsJust x => a
|
||||
|
||||
So now, the constraint arrow ``=>`` means that the argument will be found
|
||||
by ``auto``-implicit search.
|
||||
|
||||
When defining a ``data`` type, there are ways to control how ``auto``-implicit
|
||||
search will proceed, by giving options to the data type. For example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Elem : (x : a) -> (xs : List a) -> Type where
|
||||
[search x]
|
||||
Here : Elem x (x :: xs)
|
||||
There : Elem x xs -> Elem x (y :: xs)
|
||||
|
||||
The ``search x`` option means that ``auto``-implicit search for a value of
|
||||
type ``Elem t ts`` will start as soon as the type checker has resolved the
|
||||
value ``t``, even if ``ts`` is still unknown.
|
||||
|
||||
By default, ``auto``-implicit search uses the constructors of a data type
|
||||
as search hints. The ``noHints`` option on a data type turns this behaviour
|
||||
off.
|
||||
|
||||
You can add your own search hints with the ``%hint`` option on a function.
|
||||
For example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data MyShow : Type -> Type where
|
||||
[noHints]
|
||||
MkMyShow : (myshow : a -> String) -> MyShow a
|
||||
|
||||
%hint
|
||||
showBool : MyShow Bool
|
||||
showBool = MkMyShow (\x => if x then "True" else "False")
|
||||
|
||||
myShow : MyShow a => a -> String
|
||||
myShow @{MkMyShow myshow} = myshow
|
||||
|
||||
In this case, searching for ``MyShow Bool`` will find ``showBool``, as we
|
||||
can see if we try evaluating ``myShow True`` at the REPL:
|
||||
|
||||
::
|
||||
|
||||
Main> myShow True
|
||||
"True"
|
||||
|
||||
In fact, this is how interfaces are elaborated. However, ``%hint`` should be
|
||||
used with care. Too many hints can lead to a large search space!
|
||||
|
||||
Totality and Coverage
|
||||
---------------------
|
||||
|
||||
``%default covering`` is now the default status [Actually still TODO, but
|
||||
planned soon!]
|
||||
|
||||
Build artefacts
|
||||
---------------
|
||||
|
||||
This is not really a language change, but a change in the way Idris saves
|
||||
checked files, and still useful to know. All checked modules are now saved in a
|
||||
directory ``build/ttc``, in the root of the source tree, with the directory
|
||||
structure following the directory structure of the source. Executables are
|
||||
placed in ``build/exec``.
|
||||
|
||||
.. _sect-new-features:
|
||||
|
||||
New features
|
||||
============
|
||||
|
||||
As well as the change to the core language to use quantitative type theory,
|
||||
described above, there are several other new features.
|
||||
|
||||
.. _sect-local-defs:
|
||||
|
||||
Local function definitions
|
||||
--------------------------
|
||||
|
||||
Functions can now be defined locally, using a ``let`` block. For example,
|
||||
``greet`` in the following example, which is defined in the scope of a local
|
||||
variable ``x``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
chat : IO ()
|
||||
chat
|
||||
= do putStr "Name: "
|
||||
x <- getLine
|
||||
let greet : String -> String
|
||||
greet msg = msg ++ " " ++ x
|
||||
putStrLn (greet "Hello")
|
||||
putStrLn (greet "Bye")
|
||||
|
||||
These ``let`` blocks can be used anywhere (in the middle of ``do`` blocks
|
||||
as above, but also in any function, or in type declarations).
|
||||
``where`` blocks are now elaborated by translation into a local ``let``.
|
||||
|
||||
However, Idris no longer attempts to infer types for functions defined in
|
||||
``where`` blocks, because this was fragile. This may be reinstated, if we can
|
||||
come up with a good, predictable approach.
|
||||
|
||||
Scope of implicit arguments
|
||||
---------------------------
|
||||
|
||||
Implicit arguments in a type are now in scope in the body of a definition.
|
||||
We've already seen this above, where ``n`` is in scope automatically in the
|
||||
body of ``vlen``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
vlen : {n : Nat} -> Vect n a -> Nat
|
||||
vlen xs = n
|
||||
|
||||
This is important to remember when using ``where`` blocks, or local definitions,
|
||||
since the names in scope will also be in scope when declaring the *type* of
|
||||
the local definition. For example, the following definition, where we attempt
|
||||
to define our own version of ``Show`` for ``Vect``, will fail to type check:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
showVect : Show a => Vect n a -> String
|
||||
showVect xs = "[" ++ showBody xs ++ "]"
|
||||
where
|
||||
showBody : Vect n a -> String
|
||||
showBody [] = ""
|
||||
showBody [x] = show x
|
||||
showBody (x :: xs) = show x ++ ", " ++ showBody xs
|
||||
|
||||
This fails because ``n`` is in scope already, from the type of ``showVect``,
|
||||
in the type declaration for ``showBody``, and so the first clause ``showBody
|
||||
[]`` will fail to type check because ``[]`` has length ``Z``, not ``n``. We can
|
||||
fix this by locally binding ``n``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
showVect : Show a => Vect n a -> String
|
||||
showVect xs = "[" ++ showBody xs ++ "]"
|
||||
where
|
||||
showBody : forall n . Vect n a -> String
|
||||
...
|
||||
|
||||
Or, alternatively, using a new name:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
showVect : Show a => Vect n a -> String
|
||||
showVect xs = "[" ++ showBody xs ++ "]"
|
||||
where
|
||||
showBody : Vect n' a -> String
|
||||
...
|
||||
|
||||
Idris 1 took a different approach here: names which were parameters to data
|
||||
types were in scope, other names were not. The Idris 2 approach is, we hope,
|
||||
more consistent and easier to understand.
|
||||
|
||||
Better inference
|
||||
----------------
|
||||
|
||||
In Idris 1, holes (that is, unification variables arising from implicit
|
||||
arguments) were local to an expression, and if they were not resolved while
|
||||
checking the expression, they would not be resolved at all. In Idris 2,
|
||||
they are global, so inference works better. For example, we can now say:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
test : Vect ? Int
|
||||
test = [1,2,3,4]
|
||||
|
||||
Main> :t test
|
||||
Main.test : Vect (S (S (S (S Z)))) Int
|
||||
|
||||
The ``?``, incidentally, differs from ``_`` in that ``_`` will be bound as
|
||||
an implicit argument if unresolved after checking the type of ``test``, but
|
||||
``?`` will be left as a hole to be resolved later. Otherwise, they can be
|
||||
used interchangeably.
|
||||
|
||||
Dependent case
|
||||
--------------
|
||||
|
||||
``case`` blocks were available in Idris 1, but with some restrictions. Having
|
||||
better inference means that ``case`` blocks work more effectively in Idris 2,
|
||||
and dependent case analysis is supported.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
append xs ys
|
||||
= case xs of
|
||||
[] => ys
|
||||
(x :: xs) => x :: append xs ys
|
||||
|
||||
The implicit arguments and original values are still available in the body of
|
||||
the ``case``. Somewhat contrived, but the following is valid:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
info : {n : _} -> Vect n a -> (Vect n a, Nat)
|
||||
info xs
|
||||
= case xs of
|
||||
[] => (xs, n)
|
||||
(y :: ys) => (xs, n)
|
||||
|
||||
|
||||
Record updates
|
||||
--------------
|
||||
|
||||
Dependent record updates work, provided that all relevant fields are updated
|
||||
at the same time. Dependent record update is implemented via dependent ``case``
|
||||
blocks rather than by generating a specific update function for each field as
|
||||
in Idris 1, so you will no longer get mystifying errors when trying to update
|
||||
dependent records!
|
||||
|
||||
For example, we can wrap a vector in a record, with an explicit length
|
||||
field:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
record WrapVect a where
|
||||
constructor MkVect
|
||||
purpose : String
|
||||
length : Nat
|
||||
content : Vect length a
|
||||
|
||||
Then, we can safely update the ``content``, provided we update the ``length``
|
||||
correspondingly:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
addEntry : String -> WrapVect String -> WrapVect String
|
||||
addEntry val = record { length $= S,
|
||||
content $= (val :: ) }
|
||||
|
||||
Generate definition
|
||||
-------------------
|
||||
|
||||
A new feature of the IDE protocol supports generating complete definitions from
|
||||
a type signature. You can try this at the REPL, for example, given our
|
||||
favourite introductory example...
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
|
||||
...assuming this is defined on line 3, you can use the ``:gd`` command as
|
||||
follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Main> :gd 3 append
|
||||
append [] ys = ys
|
||||
append (x :: xs) ys = x :: append xs ys
|
||||
|
||||
This works by a fairly simple brute force search, which tries searching for a
|
||||
valid right hand side, and case splitting on the left if that fails, but is
|
||||
remarkably effective in a lot of situations. Some other examples which work:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y
|
||||
my_curry : ((a, b) -> c) -> a -> b -> c
|
||||
my_uncurry : (a -> b -> c) -> (a, b) -> c
|
||||
append : Vect n a -> Vect m a -> Vect (n + m) a
|
||||
lappend : (1 xs : List a) -> (1 ys : List a) -> List a
|
||||
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
|
||||
|
||||
This is available in the IDE protocol via the ``generate-def`` command.
|
||||
|
||||
Chez Scheme target
|
||||
------------------
|
||||
|
||||
The default code generator is, for the moment, `Chez Scheme
|
||||
<https://www.scheme.com/>`_. A Racket code generator is also available. There
|
||||
is not yet a way to plug in code generators as in Idris 1, but this is coming.
|
||||
To change the code generator, you can use the ``:set cg`` command:
|
||||
|
||||
::
|
||||
|
||||
Main> :set cg racket
|
||||
|
||||
Early experience shows that both are much faster than the Idris 1 C code
|
||||
generator, in both compile time and execution time (but we haven't done any
|
||||
formal study on this yet, so it's just anecdotal evidence).
|
Loading…
Reference in New Issue
Block a user