Type Safe Redis Queries: A Case Study of Type-Level Programming in Haskell

TL;DR

This paper presents a Haskell-based domain-specific language that leverages type-level programming to ensure compile-time type safety for Redis database operations, preventing runtime errors related to type mismatches.

Contribution

It introduces a novel type-safe Redis query language using advanced Haskell type-level features, enhancing reliability and safety of database interactions.

Findings

Successfully prevents runtime type errors in Redis operations

Demonstrates practical use of Haskell's type-level programming techniques

Improves safety and correctness in database programming

Abstract

Redis is an in-memory data structure store, often used as a database, with a Haskell interface Hedis. Redis is dynamically typed --- a key can be discarded and re-associated to a value of a different type, and a command, when fetching a value of a type it does not expect, signals a runtime error. We develop a domain-specific language that, by exploiting Haskell type-level programming techniques including indexed monad, type-level literals and closed type families, keeps track of types of values in the database and statically guarantees that type errors cannot happen for a class of Redis programs.