I’m interested in dependent types and metaprogramming.
I’m a PhD student with Ohad Kammar, at the University of Edinburgh. I’m working on metaprogramming by reusing fragments of the host language.
Supported by the National Cyber Security Centre (NCSC), as part of the UK Research Institute in Verified Trustworthy Software Systems, led by Ohad Kammar, at the University of Edinburgh.
As part of this project, I have:
We present a library for the ergonomic creation, manipulation, and use of first-order algebras. We do not rely on hard-coded syntactic support for our embedded language. Instead, we use metaprogramming to provide syntactic sugar for creating and using user-definable deeply-embedded first-order algebras.
We manipulate Idris 2 syntax with elaborator reflection at compile-time. We reinterpret the syntax with non-standard semantics, to provide utilities for creating, and writing terms in, user-defined algebras. We show how to use this to evaluate in an algebra internally to a category.
Traditionally, most data science is done in dynamically typed languages. If you’re manipulating a table of data, and make a typo in a column name, or ask for the wrong column, then you don’t find out until runtime - after which significant computation may have taken place. So a small mistake could lose a large amount of time.
With dependant types, we can express the schemas of tables at compile-time. This allows us to check, at compile-time, that our columns exist, and are of the correct types.
We will go through a simple machine learning example, and show the whole workflow, to demonstrate how dependant types can help the process.
An introduction to a number of tools supporting data science work in Idris. We will talk about tools for extracting data from businesses, presenting results to stakeholders, and other tools that were developed in the course of developing these tools.
This is the surrounding work, we wont directly do any data science.
Writing backends is time-consuming, and most languages have C FFIs, so wouldn’t it be nice if we could just use the C backend instead? In this talk I show how to extend RefC to create Idris 2 backends for more languages, by a high-level overview of the Python backend.
No Python knowledge will be required, we will be staying mostly in Idris code. This talk should be useful both if you want to get involved in the Python backend, or if you want to create another RefC-based backend.