294 papers · page 1 of 15
Ravi Chugh
Block-based code editors have been adopted widely in classrooms with young learners, yet they are often perceived as inferior compared to the ultimate flexibility of text editors. Beyond blocks, alternatives to manipulating programs as text have been pursued through various struc…
Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, Aaron Stump
Programming with typeclass-defined combinators like fmap allows programs a great deal of generality and concision, but programmers have to explicitly invoke combinators in the right places in order to get their programs to type check. In this paper, we propose inferring these ope…
Matthías Páll Gissurarson, Elisabet Lobo Vesga, Alejandro Russo
Many of the domain-specific languages we use every day are not written to files but typed at an interactive prompt, e.g., database shells, cloud CLIs, and in-house analytics consoles. For these REPL-driven command languages, autocomplete is, we argue, not a polish feature but a c…
Matthias Hetzenberger, Georg Moser, Florian Zuleger
Probabilistic algorithms and data structures are widely used to obtain favourable expected performance guarantees. While their mathematical analysis is often well understood, mechanising expected-cost analyses remains challenging, requiring reasoning about probability distributio…
Alex Hobbs, Alex Dixon
Functional programming is a core part of many undergraduate-level courses in Computer Science. Pedagogical interest in Haskell continues to grow as functional idioms become commonplace in popular multi-paradigm languages. The Glasgow Haskell Compiler (GHC) is by far Haskell’s mos…
Alperen Keles, George Miao, Leonidas Lampropoulos
Property-based testing frameworks rely on shrinking to turn noisy random failures into counterexamples that developers can debug. Although bug-finding performance is routinely measured, shrinking itself is rarely evaluated quantitatively. We present an experience report on evalua…
Robert Krook, Lennart Augustsson
Cloud Haskell brings Erlang-style distributed programming to Haskell, but its treatment of mobile code exposes a difficult boundary in the source-level API. Remote processes must be expressed as static closures, messages must satisfy serialisation constraints, and participating n…
Stephanie Weirich
Dependent type theory is having a moment as the foundation for interactive provers, such as Lean, Rocq, and Agda. But what does dependent type theory offer to programmers, who just want to get work done? While Haskell is not a full spectrum dependently-typed language, its type sy…
Travis Cardwell, Sam Derbyshire, Edsko de Vries, Dominik Schrempf
Interfacing Haskell with C libraries is a common necessity, but the manual creation of bindings is both error-prone and laborious. We present hs-bindgen, a new tool that provides fully automatic generation of Haskell FFI bindings directly from C header files.
We introduce a nove…
Richard A. Eisenberg
After spending a decade focusing mostly on Haskell, I have spent the last three years looking deeply at OCaml. This talk will capture some lessons learned about my work in the two languages and their communities -- how they are similar, how they differ, and how each might usefull…
Gergo Érdi
Clash is a compiler from Haskell to hardware description. We explore a "Haskell-first" approach to hardware design by building an FPGA Sudoku solver based on a well-known software implementation, showing the step-by-step process of adapting it to hardware. The final code still ex…
Zac Garby, Patrick Bahr, Graham Hutton
We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. We focus on languages whose semantics can be expressed as a fold, and show how the calculations can be simplified using …
Simon Peyton Jones
Eight years ago "Compiling without continuations" introduced the idea of so-called join points as a powerful optimisation tool in a functional language compiler. Since then join points have become more and more deeply entwined in GHC's optimisation passes; for example they are tr…
Samuel Klumpers, Tom Schrijvers
Automatic differentiation (AD) is a family of algorithms with many applications in scientific computing and machine learning. They compute numerical derivatives by interpreting or transforming the source code of numeric expressions. The correctness and efficiency of such AD algor…
Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, Manuel M. T. Chakravarty
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages c…
Anton Lorenzen
Persistent data structures are ubiquitous in functional programming languages and their designers frequently have to reason about amortized time complexity. But proving amortized bounds is difficult in a persistent setting, and pen-and-paper proofs give little assurance of correc…
Noé De Santo, Stephanie Weirich
We introduce the Rebound library that supports well-scoped term representations in Haskell and automates the definition of substitution, alpha-equivalence, and other operations that work with binding structures. The key idea of our design is the use of first-class environments th…
Grant VanDomelen, Gan Shen, Lindsey Kuper, Yao Li
Freer monads are a useful structure commonly used in various domains due to their expressiveness. However, a known issue with freer monads is that they are not amenable to static analysis. This paper explores freer arrows, a relatively expressive structure that is amenable to sta…
Robert Weingart, Nicolas Wu
In Haskell, type classes can act like functions from types to terms. However, unlike for functions, there is no way for the programmer to ask the compiler to verify that classes pattern-match exhaustively on their arguments, and their usage must always be marked by a constraint e…
Lennart Augustsson
MicroHs is a compiler for Haskell2010. It translates Haskell to SKI style combinators via λ-calculus. The runtime system is quite small with few dependencies.