kirancodes.me
To Proof Maintenance & Beyond!

Chesskell: a two-player game at the type level

Toby Bailey, Michael B. Gale

Abstract

Extensions to Haskell's type system, as implemented in GHC, have given developers more tools to express the domain-specific rules and invariants of their programs in types. For these extensions to see mainstream adoption, their use in complex applications has to be practical. We present Chesskell, an EDSL for describing Chess games where a type-level model of the full FIDE ruleset prevents us from expressing games with invalid moves. Our work highlights current limitations when using GHC to express such complex rules due to the resulting memory usage and compile times, which we report on. We further present some approaches for working around those limitations.

Related papers