PI: Ohad Kammar, University of Edinburgh. Co-I: Robert Wright, University of Edinburgh.

  • Data-science pipelines drive modern artificial intelligence technology and innovation and it is crucial that they are robust and stable.
  • Unfortunately, data analysis pipelines involve intricate dependencies and relationships, much too subtle for most common programming language type-systems to express.
  • Idris 2 is a new dependently-typed programming language that supports type-driven development and also multiple backends, including C, JavaScript, Haskell, OCaml, and Scheme.

Data-science pipelines drive modern artificial intelligence technology and innovation. They take as input raw, unprocessed data, and pump it through layer after layer of intricate processing stages, to be emitted as data visualisations, analytics reports, or into decision-making processes.As we utilise data pipelines for more and more aspects of our life, it becomes more important to ensure that they are robust and stable.Static typing is one of the most successful methods for developing robust software, since the compiler reports errors even before the program runs.

Unfortunately, data analysis pipelines involve intricate dependencies and relationships, much too subtle for most common programming language type-systems to express. The goal of this project was to develop infrastructure needed to explore how degree type-driven development can help with the construction of expressive and robust data analysis pipelines in Idris 2.

Idris 2 is a new dependently-typed programming language that supports type-driven development and also multiple backends, including C, JavaScript, Haskell, OCaml, and Scheme.

PUBLICATIONS. [1] Robert Wright, Michel Steuwer, and Ohad Kammar. Idris2-Table: evaluating dependently-typed tables with the Brown Benchmark for Table Types (Extended Abstract).  (TyDe’22) [2] Ohad Kammar, Katarzyna Marek, Minh Nguyen, Michel Steuwer, Jacob Walters, and Robert Wright. Towards type-driven data-science in Idris. (LAFI’23)

RELATED GRANT. Royal Society University Research Fellowship Renewal, “Foundations for Type-Driven Data Science” (2024 – 2026).