About myself

I'm Dr. Gergő Érdi (Érdi Gergő in the original Hungarian order of surname first), born in Budapest and living in Singapore since 2011.
I graduated from Semmelweis University of Medicine with an MD in 2005. Meanwhile, in 2003 I also started studying at the Computer Science faculty of Eötvös Loránd University, and got my CS master's degree in 2011.
Between 2005 and 2011, I've worked at Intentional Software. Since 2011, I'm currently at Standard Chartered Bank.
Retrocomputing with Clash: Haskell for FPGA Hardware Design
My new book on everything Clash, Haskell, and old computers, is out now! Check out the sample chapters and buy it from Leanpub (e-book) or Lulu (hardcopy).
A small benchmark for functional languages targeting web browsers
2 July 2022 (programming haskell idris javascript)I had an idea for a retro-gaming project that will require a MOS 6502 emulator that runs smoothly in the browser and can be customized easily. Because I only need the most basic of functionality from the emulation (I don't need to support interrupts, timing accuracy, or even the notion of cycles), I thought I'd just quickly write one. This post is not about the actual retro-gaming project that prompted this, but instead, my experience with the performance of the generated code using various functional-for-web languages.
As I usually do in situations like this, I started with a Haskell implementation to serve as a kind of executable specification, to make sure my understanding of the details of various 6502 instructions is correct. This Haskell implementation is nothing fancy: the outside world is modelled as a class MonadIO m => MonadMachine m, and the CPU itself runs in MonadMachine m => ReaderT CPU m, using IORefs in the CPU record for registers.
The languages
Ironing out all the wrinkles took a whole day, but once it worked well enough, it was time for the next step: rewriting it in a language that can then target the browser. PureScript seemed like an obvious choice: it's used a lot in the real world so it should be mature enough, and with how simple my Haskell code is, PureScript's idiosyncracies compared to Haskell shouldn't really come into play beyond the syntax level. The one thing that annoyed me to no end was that numeric literals are not overloaded, so all Word8s in my code had to be manually fromIntegral'd; and, in an emulator of an eight-bit CPU, there's a ton of Word8 literals...
The second contender was Idris 2. I've had good experience with Idris 1 for the web when I wrote the ICFP Bingo web app, but that project was all about the DOM manipulation and no computation. I was curious what performance I can get from Idris 2's JavaScript backend.
And then I had to include Asterius, a GHC-based compiler emitting WebAssembly. Its GitHub page states it is "actively maintained by Tweag I/O", but it's actually in quite a rough shape: the documentation on how to build it is out of date, so the only way to try it is via a 20G Docker container...
Notably missing from this list is GHCJS. Unfortunately, I couldn't find an up-to-date version of it; it seems the project, or at least work on integrating with standard Haskell tools like Stack, has died off.
To compare performances, I load the same memory image into the various emulators, set the program counter to the same starting point, and run it for 4142 instructions until a certain target instruction is reached. To paper over the browser's JavaScript JIT engine etc., each test runs for 100 times first as a warm-up, then 100 times measured.
Beside the PureScript, Idris 2, and GHC/Asterius implementations, I have also added a fourth version to serve as the baseline: vanilla JavaScript. Of course, I tried to make it as close to the functional versions as possible; I hope what I wrote is close to what could reasonably be expected as the output of a compiler.
Performance results
The following numbers come from the collected implementations in this GitHub repo. The PureScript and Idris 2 versions have been improved based on ideas from the respective Discord channels. For PureScript, using the CPS-transformed version of Reader helped; and in the case of Idris 2, Stefan Höck's changes of arguments instead of ReaderT, and using PrimIO when looping over instructions, improved performance dramatically.
Implementation | Generated code size (bytes) | Average time of 4142 instructions (ms) |
JavaScript | 12,877 | 0.98 |
ReasonML/ReScript | 27,252 | 1.77 |
Idris 2 | 60,379 | 6.38 |
Clean | 225,283 | 39.41 |
PureScript | 151,536 | 137.03 |
GHC/Asterius | 1,448,826 | 346.73 |
So Idris 2 comes out way ahead of the pack here: unless you're willing to program in JavaScript, it's by far your best bet both for tiny deployment size and superb performance. All that remains to improve is to compile monad transformer stacks better so that the original ReaderT code works as well as the version using implicit parameters
To run the benchmark yourself, checkout the GitHub repo, run make in the top-level directory, and then use a web browser to open _build/index.html and use the JavaScript console to run await measureAll().
Update on 2022-07-08
I've added ReScript (ReasonML for the browser), which comes in as the new functional champion! I still wouldn't want to write this program in ReScript, though, because of the extra pain caused it lacks not only overloaded literals, but even type-driven operator resolution...
Also today, I have received a pull request from Camil Staps that adds a Clean implementation.
Older entries
My software
These days, I'm mostly just writing small programs for fun, or throw-away code relevant to some theoretical subjects I happen to get interested in in the field of functional programming, and then push them to my GitHub repos or write about them in my blog. Ones you might find interesting include:
- Space Invaders arcade machine implemented on an FPGA, running the original firmware on its Intel 8080-compatible CPU. The CPU and the whole machine are all written in CLaSH.
- A MOS 6502-compatible CPU implemented in Kansas Lava. I've turned this into a full Commodore PET and I plan to eventually build a complete Commodore 64 from it.
- Scope- and typechecker for the simply typed λ-calculus, in Agda and in Haskell. The latter utilizes many of the same techniques as the former.
- Alef: A lazy functional programming language (interpreter and compiler). I later reworked that into a simpler version for this blogpost.
- MetaFun: Compile a Haskell-like functional language into C++ template metaprograms
- Tandoori: Compositional type checker for Haskell 98 (my M.Sc. thesis)
- Brainfuck compiler & transpiler for the Commodore 64
Full list (including older stuff)
Talks
These are slides and recordings from some talks I've done over the years at various meetup groups and conferences.
- Executable, Synthesizable, Human Readable: Pick Three (intro video): A short walkthrough of a Clash implementation of Pong, as an illustration of the hardware design approach I explore in detail in my upcoming book. (Haskell Love 2021, September 2021)
- ScottCheck: An Adventure in Symbolic Execution (video recording): A whirlwind tour through classic text adventure games, interpreters, SMT solvers, and monad transformer stacks, to answer the eternal question of mankind: "Can you get the coin into the throne room, if it is behind a locked door, and the key is guarded by a vampire?". (Berlin Functional Programming Meetup Group, October 2020)
- Free monoids take a price HIT: a short étude in representing free algebraic structures as syntax modulo theory, using higher inductive types (well, just quotient types, really, but when all you have is a hammer...). Source code of Literate Agda slides contains the Cubical Agda proof that all free monoids are isomorphic. (Haskell.SG meetup, January 2020)
- Cooking a Haskell Curry with Applicative Functors: I was asked to give a talk at the Singapore Institute of Technology for CS students learning FP. I haven't googled these terms, but I'm pretty sure "CS" means "cooking school" and "FP" means "food preparation". This is all based on this old blog post of course, but is updated to use a representation more direct than the (not really correct) free applicative over a co-Yoneda functor. (Singapore Institute of Technology FP Day, March 2019)
- Cubical Type Theory: From i0 to i1, or as I put it on Twitter: Breaking News! Industry programmer writes integer addition in cubical type theory in one week! (Haskell.SG meetup, December 2018)
- Generic Description of Well-Scoped, Well-Typed Syntaxes (Midlands Graduate School, April 2018)
- Resurrecting an 8-bit text adventure game with 5 programming languages and a bit of puzzle solving (Hack && Tell Singapore, July 2017)
- Matt Brown, Jens Palsberg: Typed Self-Evaluation via Intensional Type Functions (Papers We Love.SG ⨯ Haskell.SG, February 2017)
- Pattern Synonyms (Haskell Symposium 2016)
- Compositional Type Checking (video recording) (Haskell.SG meetup, July 2016)
- Matt Brown, Jens Palsberg: Breaking Through the Normalization Barrier: A Self-Interpreter for Fω (Papers We Love.SG, November 2015)
- Conor McBride: "The Derivative of a Regular Type is its Type of One-Hole Contexts" (Paper We Love.SG, June 2015)
- Hobbist FPGA development with Kansas Lava (Haskell.SG meetup, May 2015)
- Practical introduction to Agda (Singapore Functional Meetup, June/July 2012)
- Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism (Masters thesis defense, January 2011)
Papers
Pattern synonyms
- M. Pickering, G. Érdi, S. Peyton Jones, R. Eisenberg: Pattern Synonyms: our paper from Haskell Symposium 2016
- Slides from my Haskell Symposium 2016 talk
Symbolic execution
- G. Érdi: An Adventure in Symbolic Execution (extended abstract): a brief experience report on checking text adventure games for soluability using SMT solvers. My talk from IFL 2020 is on YouTube. I also did a much more extended version of this talk at the Berlin Functional Programming meetup; here are the slides from that version and here is the recording.
Syntax-generic programming
- G. Érdi: Generic Description of Well-Scoped, Well-Typed Syntaxes: never write a substitution proof for your particular extended lambda calculus manually ever again!
- Agda library implementation of the above paper
Compositional type checking
- G. Érdi: Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism: My 2011 MSc thesis
- The case for compositional type checking: an introductory blog post explaining the basic difference between linear and compositional type systems
- Defence presentation
- Slides and video recording from my talk at Haskell.SG in 2016, based on a new implementation that aims for simplicity and understandability