Search

Since LISP, dynamic languages have supported dynamically-checked type annotations. Even in dynamic languages, these annotations are typically static: tests are restricted to checking low-level features of objects and values, such as primitive types or membership of an explicit programmer-defined class. We propose much more dynamic types for dynamic languages — first-class objects that programmers can customise, that can be composed with other types and depend on computed values — and to use these first-class type-like values as types. In this way programs can define their own conceptual models of types, extending both the kinds of tests programs can make via types, and the guarantees those tests can provide. Building on a comprehensive pattern-matching system and leveraging standard language syntax lets these types be created, composed, applied, and reused straightforwardly, so programmers can use these truly dynamic first-class types to make their programs easier to read, understand, and debug.

Structural type systems provide an interesting alternative to the more common nominal typing scheme. Several existing languages employ structural types in some form, including Modula-3, Scala and various extensions proposed for Java. However, formalising a recursive structural type system is challenging. In particular, the need to use structural coinduction remains a hindrance for many. We formalise in Agda a simple recursive and structural type system with products and unions. Agda proves useful here because it has explicit support for coinduction and will raise an error if this is misused. The implementation distinguishes between inductively and coinductively defined types: the former corresponds to a finite representation, such as found in source code or the internals of a compiler, while the latter corresponds to a mathematical ideal with which we can coinductively define relations and proofs that are easily applied back to the inductive interpretation. As an application of this, we provide a mechanised proof of subtyping soundness against a semantic embedding of the types into Agda.

Method names with multiple separate parts are a feature of many dynamic languages derived from Smalltalk. Generalising the syntax of method names to allow parts to be repeated, optional, or alternatives, means a single definition can respond to a whole family of method requests. We show how generalising method names can support flexible APIs for domain-specific languages, complex initialisation tasks, and control structures defined in libraries. We describe how we have extended Grace to support generalised method names, and prove that such an extension can be integrated into a gradually-typed language while preserving type soundness.

Many IR effectiveness measures are motivated from intuition, theory, or user studies. In general, most effectiveness measures are well correlated with each other. But, what about where they don't correlate? Which rankings cause measures to disagree? Are these rankings predictable for particular pairs of measures? In this work, we examine how and where metrics disagree, and identify differences that should be considered when selecting metrics for use in evaluating retrieval systems.

littleBits (littleBits.cc) is an open-source hardware library of pre assembled analogue components that can be easily assembled into circuits, disassembled, reassembled, and re-used. In this demo, we consider littleBits --- and the littleBits synth kit in particular ---as a physically-embodied domain specific functional programming language, and how littleBits circuits can be considered as monadic programs.

Grace is a new gradually, structurally typed object-oriented programming language. Formal models of existing languages provide a rigorous base for claiming type soundness, so we have set about creating a model of a subset of Grace. While much of the formal literature of objects has used structural typing, models of popular modern languages such as Featherweight Java have had to use nominal typing to match the language they are modelling. In contrast to this, we present Tinygrace: a subset of Grace with a structural type system, feature-parity with FJ, and an accompanying proof of soundness.