Decidable Propositional Equality in Haskell

Types and Kinds

A recent discussion on the cvs-ghc mailing list touched on propositional decidable equality in Haskell. This post will explain propositional equality and consider different encodings of this idea in Haskell.


This blog post is a literate Haskell file, compatible with GHC 7.6.1. As usual, we need some initial declarations to get off the ground.

> {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies,
>              LambdaCase #-}
> {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
> data Nat = Zero | Succ Nat

Throughout the post, I will be talking about equality on Nats, but the ideas here extend to any types that would admit a good instance of Eq.

We will need length-indexed vectors to make interesting use of the ideas here:

> data Vec :: * -> Nat -> * where
>   VNil  :: Vec a Zero
>   VCons :: a -> Vec a n -> Vec a (Succ…

View original post 2,180 more words

This entry was posted in Philosophie. Bookmark the permalink.