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.
Composable CPU descriptions in CλaSH, and wrap-up of RetroChallenge 2018/09
30 September 2018 (programming haskell fpga electronics retrochallenge clash)My last post ended with some sample CλaSH code illustrating the spaghetti-ness you can get yourself into if you try to describe a CPU directly as a function (CPUState, CPUIn) -> (CPUState, CPUOut). I promised some ideas for improving that code.
To start off gently, first of all we can give names to some common internal operations to help readability. Here's the code from the previous post rewritten with a small kit of functions:
intensionalCPU (s0, CPUIn{..}) = case phase s of WaitKeyPress reg -> let s' = case cpuInKeyEvent of Just (True, key) -> goto Fetch1 . setReg reg key $ s _ -> s out = def{ cpuOutMemAddr = pc s' } in (s', out) Fetch1 -> let s' = goto Exec s{ opHi = cpuInMem, pc = succ $ pc s } out = def{ cpuOutMemAddr = pc s' } in (s', out) where s | cpuInVBlank = s0{ timer = fromMaybe 0 . predIdx $ timer s0 } | otherwise = s0
Using a State monad
To avoid the possibility of screwing up the threading of the internal state, we can use the State CPUState monad:
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)
Papers
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 from my talk at Haskell.SG in 2016 based on a new implementation that aims for simplicity and understandability
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
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
Talks
These are slides from some talks I've done over the years at various meetup groups.
- 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.
- 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.
- 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 (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)