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.