git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/docs/reference/language-extensions.rst
36 lines 1.7 kB history raw
1*******************
2Language Extensions
3*******************
7Type Providers
8===============
10Idris type providers are a way to get the type system to reflect
11observations about the world outside of Idris. Similarly to `F# type
12providers <http://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
13they cause effectful computations to run during type checking, returning
14information that the type checker can use when checking the rest of the
15program. While F# type providers are based on code generation, Idris
16type providers use only the ordinary execution semantics of Idris to
17generate the information.
19A type provider is simply a term of type ``IO (Provider t)``, where
20``Provider`` is a data type with constructors for a successful result
21and an error. The type ``t`` can be either ``Type`` (the type of types)
22or a concrete type. Then, a type provider ``p`` is invoked using the
23syntax ``%provide (x : t) with p``. When the type checker encounters
24this line, the IO action ``p`` is executed. Then, the resulting term is
25extracted from the IO monad. If it is ``Provide y`` for some ``y : t``,
26then ``x`` is bound to ``y`` for the remainder of typechecking and in
27the compiled code. If execution fails, a generic error is reported and
28type checking terminates. If the resulting term is ``Error e`` for some
29string ``e``, then type checking fails and the error ``e`` is reported
30to the user.
32Example Idris type providers can be seen at `this
33repository <https://github.com/david-christiansen/idris-type-providers>`__.
34More detailed descriptions are available in David Christiansen's `WGP
35'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
36thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.