Language Extensions¶
Type Providers¶
Idris type providers are a way to get the type system to reflect observations about the world outside of Idris. Similarly to F# type providers, they cause effectful computations to run during type checking, returning information that the type checker can use when checking the rest of the program. While F# type providers are based on code generation, Idris type providers use only the ordinary execution semantics of Idris to generate the information.
A type provider is simply a term of type IO (Provider t)
, where
Provider
is a data type with constructors for a successful result
and an error. The type t
can be either Type
(the type of types)
or a concrete type. Then, a type provider p
is invoked using the
syntax %provide (x : t) with p
. When the type checker encounters
this line, the IO action p
is executed. Then, the resulting term is
extracted from the IO monad. If it is Provide y
for some y : t
,
then x
is bound to y
for the remainder of typechecking and in
the compiled code. If execution fails, a generic error is reported and
type checking terminates. If the resulting term is Error e
for some
string e
, then type checking fails and the error e
is reported
to the user.
Example Idris type providers can be seen at this repository. More detailed descriptions are available in David Christiansen’s WGP ‘13 paper and M.Sc. thesis.
Elaborator Reflection¶
Another way to extend the language is elaborator reflection which is described in the Elaborator Reflection section.