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).
Shocking Finale
30 October 2023 (programming retrochallenge retrochallenge2023 retro homelab)Sunday, 15th October. Day of the HomeLab-2 game jam deadline. My port of The Revenge, or at least its first half, is fully playable. It even has quicksaving/loading implemented, with an in-memory buffer. Unfortunately, I didn't have time to find out what it would entail to implement persistent saving on cassette, but at least with quicksaving you can play cautiously enough to avoid frustrating deaths.
But can you actually win the game? To make sure you can, I wanted to play through from start to finish, using the hacked-up game scripts I ended up with that has a lot of the locations and scripts stripped. I could have just played the whole thing on a HomeLab-2 emulator, but I wanted something a bit more streamlined for two reasons:
- Because of the horrible foil keyboard of the real HomeLab-2, the firmware's keyboard sensing is a bit flakey when emulated on modern hardware with precise keypress detection, and so it's common to end up with unwanted key repetitions.
- If it turns out there's some flaw in the game scripts somewhere in the middle, I didn't want to replay the whole game from scratch after fixing the bug, reassembling and then reloading it into the emulator.
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