TyDe 2018- Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development

Full Citation in the ACM Digital Library

Authenticated modular maps in Haskell

We present hamm, a Haskell library that enables programmers to easily configure authenticated map (key-value store) implementations. We use type level programming techniques to establish an extensible foundation, and provide an example base map and several example “add on” transformers supporting features such as caches, Bloom filters and paging structures. Another add-on enables a prover to provide—and a verifier to verify—a “summary” containing only a small subset of the map’s data, and a verifier to receive and verify additional data only if needed. Preliminary performance results demonstrate significant potential for authenticated maps configured using hamm to support our goal of enabling participants to join blockchain networks faster.

Typing, representing, and abstracting control: functional pearl

A well known technique to implement programming languages with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to obtain the CPS hierarchy and to implement a family of control operators shifti and reseti. This functional pearl retells the story of a family of delimited control operators and their translation to lambda calculus via the CPS hierarchy. Prior work on the CPS hierarchy fixes a level of n control operators for the entire program upfront, but we allow different parts of the program to live at different levels. It turns out that taking shift0 rather than shift as the basis for the family of control operators is essential for this. Our source language is a typed embedding in the dependently typed language Idris. Our target language is a HOAS embedding in Idris. The translation avoids administrative beta- and eta-redexes at all levels of the CPS hierarchy, by iterating well-known techniques for the non-iterated CPS translation.

Implementing resource-aware safe assembly for kernel probes as a dependently-typed DSL

We present construction of resource-aware safe typed assembly language as an EDSL in dependently-typed Idris language. We use this assembly language to compile Linux kernel probes — small pieces of instrumentation code injected directly into the kernel and thus having to satisfy strict safety properties. We believe that the techniques presented can be generally applied to embedding a typed assembly language into a functional language with dependent types.

Extensible type-directed editing

Dependently typed programming languages, such as Idris and Agda, feature rich interactive environments that use informative types to assist users with the construction of programs. However, these environments have been provided by the authors of the language, and users have not had an easy way to extend and customize them. We address this problem by extending Idris's metaprogramming facilities with primitives for describing new type-directed editing features, making Idris's editors as extensible as its elaborator.

First class dynamic effect handlers: or, polymorphic heaps with dynamic effect handlers

Algebraic effect handlers are a powerful abstraction mechanism that can express many complex control-flow mechanisms. This article extends basic algebraic effect handlers with first class dynamic effects. Dynamic effects add a lot more expressiveness but surprisingly only need minimal changes to the original semantics. As such, dynamic effects are a powerful abstraction but can still be understood and reasoned about as regular effect handlers. We illustrate the expressiveness of dynamic effects with first class event streams in CorrL and also model full polymorphic heap references without requiring any further primitives.

Sums of products for mutually recursive datatypes: the appropriationist’s view on generic programming

Generic programming for mutually recursive families of datatypes is hard. On the other hand, most interesting abstract syntax trees are described by a mutually recursive family of datatypes. We could give up on using that mutually recursive structure, but then we lose the ability to use those generic operations which take advantage of that same structure. We present a new approach to generic programming that uses modern Haskell features to handle mutually recursive families with explicit sum-of-products structure. This additional structure allows us to remove much of the complexity previously associated with generic programming over these types.

From algebra to abstract machine: a verified generic construction

Many functions over algebraic datatypes can be expressed in terms of a fold. Doing so, however, has one notable drawback: folds are not tail-recursive. As a result, a function defined in terms of a fold may raise a stack overflow when executed. This paper defines a datatype generic, tail-recursive higher-order function that is guaranteed to produce the same result as the fold. Doing so combines the compositional nature of folds and the performance benefits of a hand-written tail-recursive function in a single setting.