Survey of Static Reasoning in Haskell

This post surveys a few techniques for achieving high confidence in Haskell code at type-checking time. (It will not cover any aspects of testing.) To compare the approaches, I'll implement a single interface with each of them.

The surveyed techniques are fairly complicated. I'll try to explain a bit about each, but please refer to their documentation for additional background. This post will also assume familiarity with a lot of Haskell: existential quantification (-XExistentialQuantification, -XGADTs, or -XRank2Types), existential quantification with higher-rank polymorphism (-XRankNTypes), safe coercions (Data.Coerce), phantom types, constraint kinds (-XConstraintKinds), GADTs, and data kinds (-XDataKinds and -XPolyKinds).

This post probably should have included hs-to-coq, but I'm unfamiliar with it and perfection is the enemy of completion.

The Specification

The interface in question is for lists of key/value pairs, also known as association lists. For the sake of brevity, we'll only require four operations:

The point is to do a broad-strokes comparison, so we'll adopt a very minimal specification, only requiring that

forall k v assoc. lookup k (insert k v assoc) == v

along with the usual functor laws. The asymptotics should be:

Vanilla Haskell

First, let's see what an implementation in "plain Haskell" might look like:

{-# LANGUAGE DeriveFunctor #-}

module Vanilla
  ( Assoc
  , empty
  , insert
  , lookup
  , lookupMaybe
  ) where

import Prelude hiding (lookup)

newtype Assoc k v = Assoc [(k, v)]
  deriving Functor

empty :: Assoc k v
empty = Assoc []

insert :: k -> v -> Assoc k v -> Assoc k v
insert k v (Assoc assoc) = Assoc ((k, v):assoc)

lookup :: Eq k => k -> Assoc k v -> v
lookup k (Assoc assoc) =
  case assoc of
    [] -> error "Failure!"
    ((k', v):rest) ->
      if k == k'
      then v
      else lookup k (Assoc rest)

Short and sweet! Using the API is pretty simple, too:

test :: String
test = lookup 2 (insert 2 "" empty)

But there's one problem: lookup calls error, which can cause the program to fail at run-time. How can we gain more assurance that a program written using this interface won't unexpectedly fail? A common answer would be to reify the partiality in the return type, e.g., with Maybe or Either:

lookupMaybe :: Eq k => k -> Assoc k v -> Maybe v
lookupMaybe k (Assoc assoc) =
  case assoc of
    [] -> Nothing
    ((k', v):rest) ->
      if k == k'
      then Just v
      else lookupMaybe k (Assoc rest)

This amounts to passing the buck. Every caller of lookupMaybe has to decide how to handle the Nothing case; they can choose to "infect" their own return type with partiality, or to risk a run-time error by using a partial function like fromJust :: Maybe a -> a.

In general, API authors choose between four options to deal with partiality:1

  1. Run-time failure, as in lookup
  2. Returning a "default" value, as in a division function that returns zero when given a zero divisor
  3. Reifying the partiality in the return type, as in lookupMaybe
  4. Restricting the function's domain, e.g., head :: NonEmpty a -> a

What if we want to the avoid runtime failure in (1), the ambiguity of (2), and give callers more flexibility than (3)? (In the lookup example, it's not even clear that (4) is at all applicable.) Well hold on to your hats, because there are at least four different ways to do it and they all involve quite a bit of type-system tomfoolery.

Smart Constructors and the Existential Trick

Types are the main tool that Haskell programmers use to get static guarantees about their programs. But type signatures like Int -> Bool encode statements about sets of values (in this case, this is a function that will take any Int as an input), whereas the precondition of lookup is a relationship between the particular values of the key and association list. lookup requires that this key is present in this specific association list. We need some way to attach unique type-level names to each association list, and to tie keys to particular names.

First, we'll add a type variable name to both parameters that acts as a unique identifier for the association list. Assoc name k v is an association list with name name, and Key name k is a key into the association list with name name.

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ExistentialQuantification #-}

module Smart
  ( Assoc
  , Key
  , SomeAssoc(..)
  , empty
  , insert
  , isKey
  , lookup
  ) where

import Prelude hiding (lookup)

newtype Assoc name k v = Assoc [(k, v)]
  deriving Functor

newtype Key name k = Key k

The question is now: How do we make sure each new Assoc has a fresh name and can't be confused with any other Assoc? The trick that makes this work is existential quantification. Consider the type Something:

data Something = forall a. Something a

Say that I give you two Something values, and you pattern match on them:

you :: Something -> Something -> Int
you (Something x) (Something y) = _

me :: Int
me = you (Something ()) (Something "foo")

What can you do with the data I've given you? In short, pretty much nothing. You can't use x and y in any meaningful way, they have completely unknown and unrelated types (GHC will name their types something like a and a1). In other words, we've given x and y unique type-level labels. The same trick will work for Assoc!

data SomeAssoc k v = forall name. SomeAssoc (Assoc name k v)

empty :: SomeAssoc k v
empty = SomeAssoc (Assoc [])

Since we didn't export the constructor of Assoc but we did export that of SomeAssoc, the only way to make a new association list is to pattern match on the existentially-quantified empty value, which invents a new type-level name for each Assoc.

insert and lookup much the same, modulo slightly changed types:

insert :: k -> v -> Assoc name k v -> Assoc name k v
insert k v (Assoc assoc) = Assoc ((k, v):assoc)

lookup :: Eq k => Key name k -> Assoc name k v -> v
lookup (Key k) (Assoc assoc) =
  case assoc of
    [] -> error "Impossible"
    ((k', v):rest) ->
      if k == k'
      then v
      else lookup (Key k) (Assoc rest)

It looks like lookup is still partial, but by carefully controlling how clients get a Key, we can ensure that it's total. And the only way we'll let them do so is with isKey (note that the constructor of Key, like that of Assoc, is not exported):

isKey :: Eq k => k -> Assoc name k v -> Maybe (Key name k)
isKey k (Assoc assoc) =
  case assoc of
    [] -> Nothing
    ((k', _):rest) ->
      if k == k'
      then Just (Key k)
      else isKey k (Assoc rest)

It's basically identical to lookup: it searches through the list and only yields a Key if k really is a key in the list. Since this is the only way to get a Key, every lookup is guaranteed to succeed.

Here's an example usage:

test :: String
test =
  case empty of
    SomeAssoc emp ->
      let assoc = insert 2 "" emp
      in case isKey 2 assoc of
           Just k -> lookup k assoc
           Nothing -> error "not a key"

Note that while isKey introduces a Maybe, the actual lookup operation doesn't. You can, e.g., store keys in a list and look them up later, without introducing partiality at the lookup. This still isn't ideal; one way to work around it in some cases would be to have insert return a Key.

GADTs, or Dependent Types

Dependent types are (roughly speaking) types that can mention values. Haskell doesn't have "full" dependent types, but GADTs make the type system quite expressive. Let's see what we can do with them!

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}

module GADT
  ( Assoc
  , NatRepr(..)
  , Key
  , empty
  , insert
  , isKey
  , lookup
  ) where

import Prelude hiding (lookup)
import Data.Kind (Type)
import Data.Type.Equality (TestEquality(testEquality), (:~:)(Refl))
import GHC.TypeLits (Nat, type (+))

For the sake of concreteness, we'll fix the keys to be natural numbers:

data NatRepr (n :: Nat) where
  Zero :: NatRepr 0
  Succ :: NatRepr n -> NatRepr (n + 1)

NatRepr is a singleton type meaning each value has a unique type. For example, Zero :: NatRepr 0 and Succ Zero :: NatRepr 1.

Just as lookup had an Eq constraint above, NatRepr needs a TestEquality instance, which is similar but for singletons:

instance TestEquality NatRepr where
  testEquality n m =
    case (n, m) of
      (Succ _, Zero) -> Nothing
      (Zero, Succ _) -> Nothing
      (Zero, Zero) -> Just Refl
      (Succ n', Succ m') ->
        case testEquality n' m' of
          Just Refl -> Just Refl
          Nothing -> Nothing

The Assoc type carries a type-level list of its keys:

data Assoc (keys :: [Nat]) (a :: Type) where
  Nil :: Assoc '[] a
  Cons :: NatRepr n -> a -> Assoc keys a -> Assoc (n ': keys) a

Because this is a GADT, we can no longer derive Functor, we have to write it ourselves:

instance Functor (Assoc keys) where
  fmap f =
    \case
      Nil -> Nil
      Cons n a rest -> Cons n (f a) (fmap f rest)

empty has an empty type-level list of keys:

empty :: Assoc '[] a
empty = Nil

insert adds one key to the front of the type-level list. In fact, insert is just Cons:

insert :: NatRepr n -> a -> Assoc keys a -> Assoc (n ': keys) a
insert = Cons

As in the smart constructor approach, we use a new type Key to track the relationship between a key and an association list. Unlike the smart constructor approach, we don't have to trust the implementation of isKey; the types force it to be correct.

data Key (n :: Nat) (keys :: [Nat]) where
  KeyHere :: Key n (n ': l)
  KeyThere :: Key n keys -> Key n (m ': keys)

isKey :: NatRepr n -> Assoc keys a -> Maybe (Key n keys)
isKey n assoc =
  case assoc of
    Nil -> Nothing
    Cons m _ rest ->
      case testEquality n m of
        Just Refl -> Just KeyHere
        Nothing ->
          case isKey n rest of
            Nothing -> Nothing
            Just key -> Just (KeyThere key)

In lookup, GHC's pattern match checker can tell that if there's a Key n keys, then the type-level list keys can't be empty, so there's no need to handle the Nil case:

lookup :: Key n keys -> Assoc keys a -> a
lookup key assoc =
  case (key, assoc) of
    (KeyHere, Cons _ a _) -> a
    (KeyThere key', Cons _ _ rest) -> lookup key' rest

Here's an example usage:

test :: String
test =
  case isKey two assoc of
    Just k -> lookup k assoc
    Nothing -> error "not a key"
  where
    two = Succ (Succ Zero)
    assoc = insert two "" empty

Ghosts of Departed Proofs

The Ghosts of Departed Proofs (GDP) paper (PDF) outlined several insights that supercharge the smart constructor/existential trick above.

It's worth noting that I'm not an expert in GDP.

GDP Infrastructure

The following introduction to the core GDP infrastructure is fairly cursory, please check out the paper for more information. I'm defining all this here to make this post self-contained, but the combinators in this module are available in the gdp package on Hackage.

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module GDP.Named
  ( Named
  , name
  , the
  , SuchThat
  , suchThat
  , Defn
  , Proof
  , axiom
  , type (-->)
  , implElim
  ) where

import Prelude hiding (lookup)
import Data.Coerce (Coercible, coerce)

First, the Named type and name function generalize the existential introduction of type-level names for values, using an equivalence between rank-2 types (the forall in the second parameter to name) and existential types:

-- | Called @~~@ in GDP.
newtype Named name a = Named a
  deriving Functor

name :: a -> (forall name. Named name a -> t) -> t
name x k = coerce k x
{-# INLINE name #-}

To extract a Named value, clients use the:

class The x a | x -> a where
  the :: x -> a
  default the :: Coercible x a => x -> a
  the = coerce

instance The (Named name a) a where

Modules can give type-level names to functions using Defn (demonstrated later):

data Defn = Defn

type Defining name = (Coercible Defn name, Coercible name Defn)

Type-level propositions are called Proof, and can be manipulated with axioms like implElim:

data Proof a = Proof  -- called QED in GDP

axiom :: Proof a
axiom = Proof

data p --> q

implElim :: Proof (p --> q) -> Proof p -> Proof q
implElim _ _ = axiom

Type-level propositions can be attached to values with SuchThat (which can also be cast away with the):

-- | Called @:::@ in GDP.
newtype SuchThat p a = SuchThat a
  deriving Functor

instance The (SuchThat p a) a where

suchThat :: a -> Proof p -> SuchThat p a
suchThat x _ = coerce x

GDP Implementation of Association Lists

Now let's take a look at using those tools to provide more assurance for the Assoc API. Happily, we can directly reuse Assoc and empty from the vanilla Haskell implementation!

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeOperators #-}

module GDP
  ( Assoc
  , Vanilla.empty
  , IsKey
  , Insert
  , insert
  , lookup
  ) where

import           Prelude hiding (lookup)

import qualified GDP.Named as GDP
import           GDP.Named (type (-->))
import           GDP.Maybe (IsJust)
import qualified GDP.Maybe as GDP
import qualified Vanilla as Vanilla
import           Vanilla (Assoc)

Instead of a separate Key type, we create a type-level proposition IsKey. A GPD.Proof (IsKey kn assocn) means that the key of type GDP.Named kn k is present in the association list of type GDP.Named assocn (Assoc k v).

-- | @kn@ is a key of association list @assocn@
data IsKey kn assocn
type role IsKey nominal nominal

lookup takes a key with an additional IsKey proof as a parameter and then just shells out to the underlying vanilla Haskell lookup implementation. The return type and the Lookup newtype will be explained in just a moment.

-- | Type-level name of 'lookup' for use in lemmas.
newtype Lookup kn assocn = Lookup GDP.Defn
type role Lookup nominal nominal

lookup ::
  Eq k =>
  GDP.SuchThat (IsKey kn assocn) (GDP.Named kn k) ->
  GDP.Named assocn (Assoc k v) ->
  GDP.Named (Lookup kn assocn) v
lookup k assoc =
  GDP.defn (Vanilla.lookup (GDP.the (GDP.the k)) (GDP.the assoc))

insert works much the same way, but it doesn't have any preconditions and so doesn't use SuchThat:

-- | Type-level name of 'insert' for use in lemmas.
newtype Insert kn vn assocn = Insert GDP.Defn
type role Insert nominal nominal nominal

insert ::
  GDP.Named kn k ->
  GDP.Named vn v ->
  GDP.Named assocn (Assoc k v) ->
  GDP.Named (Insert kn vn assocn) (Assoc k v)
insert k v assoc =
  GDP.defn (Vanilla.insert (GDP.the k) (GDP.the v) (GDP.the assoc))

So how do clients construct a GDP.SuchThat (IsKey kn assocn) (GDP.Named kn k) to pass to lookup? One of the nice parts of GDP is that library authors can determine how clients reason about propositions they define, like IsKey. In particular, library authors can introduce type-level names for their API functions like Lookup and Insert, and export axioms that describe how the API relates to the propositions.

One way to know that a key is in a map is if we just inserted that key. We can express this fact by exporting an axiom:

insertIsKey :: GDP.Proof (IsKey kn (Insert kn vn assocn))
insertIsKey = GDP.axiom

With that lemma, here's an example use of this safe API:

test :: String
test =
  GDP.name Vanilla.empty $ \emp ->
    GDP.name (2 :: Int) $ \k ->
      GDP.name "" $ \v ->
        GDP.the $
          lookup
            (k `GDP.suchThat` insertIsKey)
            (insert k v emp)

We can also conclude IsKey when lookupMaybe returns a Just value, kind of like what isKey did in previous examples:

-- | Type-level name of 'lookupMaybe' for use in lemmas.
newtype LookupMaybe kn assocn = LookupMaybe GDP.Defn

lookupMaybe ::
  Eq k =>
  GDP.Named kn k ->
  GDP.Named assocn (Assoc k v) ->
  GDP.Named (LookupMaybe kn assocn) (Maybe v)
lookupMaybe k assoc =
  GDP.defn (Vanilla.lookupMaybe (GDP.the k) (GDP.the assoc))

lookupMaybeKey ::
  GDP.Proof (IsJust (LookupMaybe kn assocn) --> IsKey kn assocn)
lookupMaybeKey = GDP.axiom

test2 :: String
test2 =
  GDP.name Vanilla.empty $ \emp ->
    GDP.name (2 :: Int) $ \k ->
      GDP.name "" $ \v ->
        GDP.the $
          let assoc = insert k v emp
          in case GDP.maybeCase (lookupMaybe k assoc) of
               GDP.IsNothing _ -> error "impossible"
               GDP.IsJust isJustPf _ ->
                 lookup
                   (k `GDP.suchThat` GDP.implElim lookupMaybeKey isJustPf)
                   assoc

where IsJust and maybeCase are defined in GDP.Maybe:

{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE TypeOperators #-}

module GDP.Maybe
  ( IsNothing
  , IsJust
  , MaybeCase(IsNothing, IsJust)
  , maybeCase
  ) where

import qualified GDP.Named as GDP

data IsJust name
data IsNothing name
data MaybeCase name a
  = IsNothing (GDP.Proof (IsNothing name))
  | IsJust (GDP.Proof (IsJust name)) a

-- | Called @classify@ in GDP.
maybeCase :: GDP.Named name (Maybe a) -> MaybeCase name a
maybeCase x =
  case GDP.the x of
    Nothing -> IsNothing GDP.axiom
    Just a -> IsJust GDP.axiom a

Such code could clearly be defined once and for all in a library somewhere, and probably even generated by Template Haskell.

Liquid Haskell

Liquid Haskell adds refinement types to Haskell, which are kind of like dependent types. It operates as a GHC type-checking plugin, and doesn't affect the runtime semantics of Haskell. I'm no Liquid Haskell expert, but luckily one of the case studies in the documentation is on association lists. What follows is a slight adaptation.

{-# LANGUAGE LambdaCase #-}

module Liquid
  ( Assoc
  , empty
  , insert
  , lookup
  ) where

import Prelude hiding (lookup)

import           Data.Set (Set)
import qualified Data.Set as Set

The Assoc type is isomorphic to the vanilla implementation:

data Assoc k v
  = Nil
  | Cons k v (Assoc k v)

keys retrieves the set of keys in the association list. It's only used at the type level. Using keys, we can refine the type of empty to state that empty has no keys. Types like { v : T | C v } should be read like "values of type T that additionally satisfy constraint C". The base type T can almost always be omitted, as it can be inferred from the vanilla-Haskell type signature.

{-@ measure keys @-}
keys :: Ord k => Assoc k v -> Set k
keys =
  \case
    Nil -> Set.empty
    Cons k _ rest -> Set.union (Set.singleton k) (keys rest)

{-@ empty :: { v : _ | keys v == Set.empty } @-}
empty :: Assoc k v
empty = Nil

Similarly, the function addKey is used to refine the type of insert:

{-@ inline addKey @-}
addKey :: Ord k => k -> Assoc k v -> Set k
addKey k kvs = Set.union (Set.singleton k) (keys kvs)

{-@ insert :: k : _ -> _ -> assoc : _ -> { v : _ | keys v = addKey k assoc } @-}
insert :: k -> v -> Assoc k v -> Assoc k v
insert = Cons

Finally, has is used to express the precondition on lookup:

{-@ inline has @-}
has :: Ord k => k -> Assoc k v -> Bool
has k assoc = Set.member k (keys assoc)

{-@ lookup :: assoc : _ -> k : { key : _ | has key assoc } -> v @-}
lookup :: Eq k => Assoc k v -> k -> v
lookup assoc k =
  case assoc of
    Nil -> error "Impossible"
    Cons k' v rest ->
      if k == k'
      then v
      else lookup rest k

Note that the order of parameters to lookup has to be flipped so that assoc is in scope in the refinement type for k.

Using this API looks almost exactly like it does for the vanilla implementation:

test :: String
test = lookup (insert 2 "" empty) 2

The type-checker will catch invalid calls to lookup:

src/Liquid.hs:58:36-45: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == 3}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | Set_mem VV (Liquid.keys ?d)}
    .
    in the context
      ?b : {?b : (Liquid.Assoc GHC.Types.Int [GHC.Types.Char]) | Liquid.keys ?b == Set_empty 0}

      ?d : {?d : (Liquid.Assoc GHC.Types.Int [GHC.Types.Char]) | Liquid.keys ?d == Set_cup (Set_sng 2) (Liquid.keys ?b)}
   |
58 | test2 = lookup (insert 2 "" empty) (3 :: Int)
   |                                    ^^^^^^^^^^

Conclusions

Smart Constructors and the Existential Trick

Smart constructors and the existential trick are likely the most accessible of all of the above techniques. They require only a single fairly conservative extension to Haskell 2010 (-XExistentialQuantification or -XRank2Types). However, the safety argument relies on the correct implementation of the newtype abstraction by the library author; in this case it would be easy enough to accidentally export the Key constructor or provide some other way of constructing a Key that violates the intended invariant. Also, a new newtype and smart constructor generally have to be custom-built for each desired safety property.

GADTs, or Dependent Types

Dependent types significantly reduce the possibility of programmer error. Once appropriate definitions for Assoc and Key are found, it is impossible for the library author to mis-implement isKey. Like smart constructors and the vanilla Haskell code, they require no external tooling nor libraries. However, programming with dependently-typed techniques has its downsides:

I'm very familiar with dependent types, which likely partially accounts for why this list is so extensive.

GDP

The GDP approach is remarkably flexible. The ability to define arbitrary lemmas about an API gives the API consumers a huge amount of power. For example, it was possible to provide two ways to produce an IsKey proof without changing the actual implementation. Furthermore, the GDP approach was able to directly reuse the vanilla Haskell implementation by simply providing wrappers with more interesting type signatures.

On the other hand, understanding the GDP approach requires a good deal of study. GDP also requires trusting the library author to provide sound reasoning principles. The GDP paper outlines a few possible approaches (including use of Liquid Haskell) to improve confidence in the exported lemmas.

Liquid Haskell

Liquid Haskell was a bit difficult to install, some of the project's packages had too-restrictive bounds (resulting in Cabal being unable to find a build plan) whereas others had too-permissive bounds (resulting in compilation failures when Cabal did find a plan). Generally, Liquid Haskell is the unfortunate combination of an impressive amount of infrastructure and code that's maintained mostly by academics. They've done a great job of making it fairly easy to get started, but I wouldn't rely on it for a commercial project for mundane reasons like not being able to upgrade to the latest GHC until the Liquid Haskell team releases a corresponding version of liquid-base.

Liquid Haskell sometimes requires you to write code in a particular way, rejecting semantically equivalent (and arguably, clearer) rewrites. For instance, I originally tried to write keys like so:

{-@ measure keys @-}
keys :: Ord k => Assoc k v -> Set k
keys =
  \case
    Nil -> Set.empty
    Cons k _ rest -> Set.insert k (keys rest)

That didn't work, Liquid Haskell said Unbound symbol Data.Set.Internal.insert. So I tried to factor the insert-via-union into a where binding for the sake of clarity like so:

{-@ measure keys @-}
keys :: Ord k => Assoc k v -> Set k
keys =
  \case
    Nil -> Set.empty
    Cons k _ rest -> setInsert k (keys rest)
  where setInsert x = Set.union (Set.singleton x)

This resulted in Uh oh. Cannot create measure 'Liquid.keys': Does not have a case-of at the top-level. If I understand correctly, this is probably because Liquid Haskell analyzes code at the GHC Core level, so it's sensitive to changes that look similar at the source level but compile to different Core. Such errors are annoying, but I was able to find workarounds whenever they came up. Just like "dependent Haskell", Liquid Haskell error messages leave a lot to be desired.

Like dependently typed Haskell and GDP, actually understanding Liquid Haskell would take at least several hours if not days of study. That being said, I was able to get started with this example in maybe an hour or so using their documentation.

Aside from the type signatures, the Liquid Haskell implementation looks pretty much exactly like the "vanilla" implementation. Remarkably, the API is also almost identical, and users could choose whether or not to use (and understand!) Liquid Haskell when consuming the API, unlike in the other techniques.

As in the dependently-typed approach, less trust in the library author is required.

Like GDP, I believe that Liquid Haskell provides the ability to export lemmas for consumers to use in constructing proofs. Unlike GDP, I believe all such lemmas can be machine-checked.

Comparison and Takeaways

The following table summarizes the above remarks. A table can't have much nuance and I'm not an expert in GDP nor Liquid Haskell, so the ratings should be taken with a hefty grain of salt.

Key:

TODO: Table got nerfed when changing blog software...

My overall take is that all of these techniques are under-utilized and under-explored. GADTs/dependent types, GDP, and Liquid Haskell would all be much easier to write if there were more widely-available libraries for programming with them. Given the attention that dependent types have received in the Haskell community, I think GDP and Liquid Haskell are especially neglected.

As the table shows at a glance, these techniques offer a wide range of benefits and drawbacks, which indicates that they're likely appropriate for different use-cases. Broad adoption of several would enable Haskell programmers to use techniques because they're appropriate to their goals, rather than because they have a paucity of options.

Footnotes

1

These are taken from the Ghosts of Departed Proofs paper.