This blog post presents a safe API for destination-passing style programming using Linear Haskell against arbitrary functional data types.

How GHC's design informs linear types

How linear constraints get rid of scope functions and why it matters.

How a linear constraint arrow relates to freezing arrays in Haskell.

On design choices to build a resource-safe interface for Sparkle using linear types

What should the type of linear traverse be exactly?

Announcing linear-base, a standard library for linearly typed Haskell programs.

Destinations give you control over your memory allocations, and linear types make them pure.

Announcement of the upcoming QualifiedDo language extension.

Looking back at the journey which brought us there, and forward to what still lies ahead.

A primer on the interaction between linear types and exceptions in Haskell.

In this post about inline-java I aim to walk you through the upcoming safe interface of the library, which allows detecting memory management mistakes at compile time using linear types.

Haskell's Data and Control module hierarchies have always bugged me. Now, I understand that the intuition behind the Data/Control separation is rooted in a deep technical justification.

In an earlier blog post, we discussed how streaming libraries help writing composable programs without lazy I/O. We showed, for a simple program, how using a streaming library helps reducing the amount of unaided bookkeeping that the programmer needs to do in order to make it…

In the “all about reflection” post, we introduced the data type. Any sorting function should have the type . However, this doesn’t actually guarantee that is indeed a sorting function: it only says that is a sorted list, but not that it is actually a sort of . For example is…

Foreign function interfaces (FFI) allow fast interop between languages. Unlike other approaches, like performing RPC calls between different components written in different languages, using the FFI allows for all manner of data to be shared between each language runtime, in the…

We saw last time that with linear types, we could precisely capture the state of sockets in their types. In this post, I want to use the same idea of tracking states in types, but applied to a more unusual example from our paper: sending rich structured data types across the…

At the time of our first post on linear types, we were fresh out of the design phase to extend GHC with linear types. We had a prototype implementation, but it was just a proof of concept: there was precious little you could do with it. A few months down the line, we are now in a…

We’re extending GHC with linear types. Ever since Jean-Yves Girard discovered linear logic in 1986, researchers around the world have been going “wow! resource tracking, this must be useful for programming languages”. After all, any real computation on a real machine takes…