Haskell FFI and Dependent Types in Agda

Haskell FFI Basics - Fraser Tweedale

Wanting to make use of libraries written in other langauges (often C) is a common situation in high-level languages, and Haskell is no exception. This talk will introduce and demonstrate real-world use of Haskell's C foreign function interface (FFI), including how to deal with some common C idioms. We will examine the c2hs tool which simplifies bindings and review some other Haskell FFI tools.

Attendees who are comfortable with Haskell syntax and have a passing familiarity with C (especially pointers) will get the most out of this presentation.

A dependently-typed Agda taster - Matt Brecknell

Let's tuck into some term-indexed types!

Part one

We'll see what it means to reify definitional equality of terms as a type, and how to use equality to rewrite types. We'll reinvent Sigma and Pi types, starting from the simple sums and products we all know and love.

Part two (next month)

We'll show how to build evidence that a certain thing can be found in a list, and how to use this evidence to safely retrieve a different thing from some other suitably-indexed heterogeneous list.

Finally, if we have time, we'll use what we just built to embed the simply-typed lambda calculus.