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).
Formatting serial streams in hardware
12 August 2024 (programming haskell clash fpga)I've been playing around with building a Sudoku solver circuit on an FPGA: you connect to it via a serial port, send it a Sudoku grid with some unknown cells, and after solving it, you get back the solved (fully filled-in) grid. I wanted the output to be nicely human-readable, for example for a 3,3-Sudoku (i.e. the usual Sudoku size where the grid is made up of a 3 ⨯ 3 matrix of 3 ⨯ 3 boxes):
4 2 1 9 5 8 6 3 7 8 7 3 6 2 1 9 5 4 5 9 6 4 7 3 2 1 8 3 1 2 8 4 6 7 9 5 7 6 8 5 1 9 3 4 2 9 4 5 7 3 2 8 6 1 2 8 9 1 6 4 5 7 3 1 3 7 2 9 5 4 8 6 6 5 4 3 8 7 1 2 9
This post is about how I structured the stream transformer that produces all the right spaces and newlines, yielding a clash-protocols based circuit.
Continue reading »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