Thomas Ekström Hansen
Thomas Ekström Hansen
Home
Projects
Experience
Accomplishments
Blog
Coursework
Light
Dark
Automatic
idris2
Type You an Idris – Part 1: Warmup
The best way to learn & understand a thing is to implement it. So let’s implement (a subset) of Idris2! This part is an introduction and covers some function exercises that will help later.
Thomas Ekström Hansen
Fri, 2 Sep 2022
An attempt at explaining Decidable Equality
One of the more difficult concepts in Idris, I’ve found, is proving things through dependent types. The ‘simplest’ introduction to this is probably the
DecEq
interface, which this post aims to introduce, explain, and implement.
Thomas Ekström Hansen
Tue, 15 Mar 2022
Implementing Condition Variables in Racket
Explaining and implementing Birell’s 2003 paper on Condition Variables for Modula-2+, in Racket.
Thomas Ekström Hansen
Tue, 27 Jul 2021
Debugging Idris2 Racket Threads
A dive into functional concurrency, FFIs, and thread weirdness.
Thomas Ekström Hansen
Wed, 24 Feb 2021
Cite
×