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
- Haskell (EDSL) → YuCat → Solidity/Yul → foundry → EVM bytecode
- Representing programs using categories (CT through diagrams)
- YulCat - a category-theory-based internal representation
- Symmetric Monoidal, Cartesian Closed Category
- Represented as GADT in Haskell:
- Storage operations: SGet, SPut
- Message calls
- Control flow: built-in functions, switch, tight-loop/foldable
- Spiwack, Bernardy: Evaluating Linear Functions to Symmetric Monoidal Categories
- Also related: Conal Elliott, Compiling to Categories
Safety through data versioning
- Data versioning – tracking EVM state (data versions) at compilation time, preventing the use of outdated data
- Implemented using the LinearTypes extension of Haskell
- LTL as Models
- Linear types for encoding labelled state transition systems
- Prior work: linear streams from Tweag
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:
- Towards Type-Directed API Search for Mainstream Languages
- Related earlier work: Bruce, Cosmo, Longo: Provable isomorphisms of types
- Related talk at ICFP: https://www.youtube.com/watch?v=yI-X5oH0LOE
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:
- lambdanas-language-server
- lsp + lsp-types libraries
- lsp-test
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 capabilitiescap
- 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
- Caprese: Capabilities and Resources for Effects
- ongoing research project
- Gears: An experimental asynchronous programming library for Scala 3
- Scala 3.7 includes capability support
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:
- John Sturdy, A Lisp through the looking glass, PhD thesis, 1991
- Reflective Towers of Interpreters
- Early work by Brian Cantwell Smith:
- Related presentation at London Clojurians: Autology: Writing a self-rewriting Lisp
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