We want to be able to take a type definition and get an Idris data type out of it. http://docs.idris-lang.org/en/latest/guides/type-providers-ffi.html example https://github.com/david-christiansen/idris-type-providers/blob/master/Providers/CSV.idr