LambdaDays2025 Report

Programming Language Theory
1

Last week, I’ve attended the LambdaDays conference. Below, I briefly summarize some of the talks that I found interesting and I think could be of broader interest in the organization. The summaries themselves are very brief and probably not detailed enough to learn much about the subject beyond a general overview, but each includes some external references. The videos of the talks will be available publicly on youtube in several months (as a participant I may get access earlier).

Yolc

Yolc is advertised as “a safe, expressive, fun language for Ethereum”. It is a DSL in Haskell for Ethereum smart contracts.

Motivation

  • expressive type system of Haskell in Ethereum smart contracts
  • safety: using linear types for data versioning – tracking EVM state

Pipeline

Safety through data versioning

Hoogle for the hungry masses

Hoogle is a widely-used API search engine for Haskell, allowing to search by (approximate) types. The talk presents TypeSearch.dev – a type-directed API search engine for mainstream (typed OO) languages.

Key points:

  • Target - mainstream (typed OO) languages
  • Inspiration - Curry-Howard correspondence
  • Type search is proof search / code synthesis
  • Surface language syntax (e.g. Java) translated to an internal representation (functional IR with subtyping and polymorphism).

References:

Create your first Language Server

The conclusion I got from the talk is that if I want to implement a language server in Haskell, I should check out the following projects:

Rethinking our adoption strategy

Evan Czaplicki (creator of Elm) gave an interesting talk about different strategies to support adoption and long-term economic viability of new programming languages. Slides are available here: Rethinking our Adoption Strategy by Evan Czaplicki on Prezi.

Making capabilities safe and convenient

Martin Odersky (designer of Scala) talked about capabilities in Scala 3.7 and beyond. Capabilities are an alternative to an effect system, and can also be seen as a mechanism for access control. For example, a file handle can be seen as a capability to perfom IO operations on a given file. In the basic object capability model, capabilities are regular program values passed around in functions. Scala 3.7 introduces language-level capability support, including relevant static checks.

Staged architecture for effects

  • 1st stage - pure FP
  • 2nd stage - effects in monads
  • not convenient - composition problem

Capability-based architecture

  • one stage - program can access all of machine
  • access controlled by fine-grained capabilities
  • depends on the runtime (effects not arbitrary)
  • capabilities make effects trackable but don’t perform them (access mechanism only) - direct style
  • Object capabilities:
    • Dennis, van Horn: Programming semantics for multiprogrammed computations
    • capabilities are regular program values
    • pros:
      • no new features (remove non-local mutable variables)
      • proven track-record in security
    • cons:
      • tedious (lots of parameters to pass around)
      • problem of revocation - an object can’t be forced to give up a capability (lifetimes / sharing hard to enforce statically)
  • Typed capabilities:
    • passing capabilities implicitly (convenience)
    • tracking capabilities in types (safety)
  • Scala 3 features used for implementing capabilities:
    • using clauses
    • path-dependent types

Capabilities for effects

  • monads don’t commute
  • effects don’t always commute
  • capabilities to describe effects
def f : CanThrow[E] ?=> T
  • Simplicity: foundations and applications of implicit function types, POPL 2018
  • Effect polymorphism problem
    • effects are transitive
    • capabilites support effect polymorphism
  • capability capture checking: Scala docs
  • capabilities captured by closures: A => B can capture free vars
  • T^{c_1,...,c_n} - capturing type, c_1,..,c_n are capabilities
  • cap - root capability
  • T^ is T^{cap}
  • A ->{c} B is (A → B)^{c}
  • A => B is A ->{cap} B
  • capabilities index types (dependent typing)
  • subtyping for capabilities (sets of capabilities)
  • subcapturing: dervided capabilities more spacific than original
  • Fengyun Liu, A study of capability-based effect systems, PhD thesis, EPFL, 2016

Current status

Self-rewriting Lisp

Jeremy (@mariari) is going to like this.

Autology is a pure functional Lisp with the ability to modify its own interpreter (dynamic rewriting of the language at runtime), implemented by Dave Kimber on top of Clojure. Among other conseqences, this approach allows to blend different programming languages together, e.g., write snippets of Python and C in the same Autology program (after appropriate self-modification at runtime).

Autology expressions:

  • atoms
  • lists
  • binding with lexical scoping (bind)
  • quoting expressions (qu)

Notes:

  • Functions (as a language feature) implemented in Autology by self-modification (implementation fits on a single slide)
  • Blending languages together
    • e.g. Scheme, Python, C, can be used together by rebinding the interpreter
    • the syntax is handled by a custom read function
    • but you can also have e.g. a python-style for loop with unicode variable names in C

Why not macros?

  • different characteristics
  • macros: static (read time), limited to parseable expressions, hygenic with gensyms
  • meta-interpretation: dynamic (run-time), any syntax, unhygenic

References:

Effectful programming in Flix

Flix is an effect-oriented programming language, supporting functional, imperative and logic programming styles.

Notes:

  • effect system separate from type system
def f(x) = x / getCurrentMinute()
  • In Flix:
def count(f : a -> Bool \ { }, l : List[a]) : int32 \ { } = ...
def sayHello(name : String): Unit \ {IO} = ...
def map(f : a -> b \ ef, l: List[a]): List[b] \ ef = ...
def >>(f: a -> b \ ef1, g : b -> c \ ef2): a -> c \ ef1 + ef2 = ...
def onException(f: Exception -> Unit \ ef - {Throw}): Unit = ...
def onMouseDown(f: MouseEvent -> Unit \ ef - {Block}): Unit = ...
  • effect sets
  • kinds of effects: primitive, heap, library-defined, user-defined
  • effect polymorphism and effect exclusion
  • Local mutable memory:
    • imperative programming encapsulated in a single function
  • Associated effects:
trait Div[t] {
  type DEff : Eff
  def div(x, y : t) : t \ DEff
}
  • Declarative logic programming: “embedded” Datalog
  • Modern compiler architecture:
    • parallel
    • incremental
    • still phased
2 Likes