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.