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
%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,
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
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.
Another way to extend the language is elaborator reflection which is described in the Elaborator Reflection section.