******************* 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 `__.