Simulate a path-dependent type in Haskell

Question

Here is a simplified example of what I want to do. Let's say you have a HList of pairs:

let hlist = HCons (1, "1") (HCons ("0", 2) (HCons ("0", 1.5) HNil))

Now I want to write a function replaceAll which will replace all the "keys" of a given type with the first "value" of the same type. For example, with the HList above I would like to replace all the String keys with "1" which is the first value of type String found in the HList

 replaceAll @String hlist =
    HCons (1, "1") (HCons ("1", 2) (HCons ("1", 1.5) HNil))

This seems to require path-dependent types in order to "extract" the type of the first pair and being able to use it to direct the replacement of keys in a second step but I don't know how to encode this in Haskell.

Answer 1

This is a proof search problem ("find occurrences of String in this list"), so you can expect that the solution will involve type class Prolog. I'll answer a simpler version of your question (namely "find the first occurrence of String") and let you figure out how to adjust it for your exact use case.

Since we're doing a proof search, let's start by writing down the proof object we'll be searching for.

data Contains a as where
    Here :: Contains a (a ': as)
    There :: Contains a as -> Contains a (b ': as)

A value of type Contains a as is a constructive proof that you can find a in the type-level list as. Structurally, Contains is like a natural number (compare There (There Here) with S (S Z)) identifying the location of a in the list as. To prove that a is in as you give its index.

For example, you can replace an element at a given location in an HList with a new element of the same type.

replace :: a -> Contains a as -> HList as -> HList as
replace x Here (HCons y ys) = HCons x ys
replace x (There i) (HCons y ys) = HCons y (replace x i ys)

---

We want to search for an a within a given list using type class Prolog. There are two cases - either you find the a at the head of the list, or it's somewhere in the tail. (If a is not in as, using contains will fail with a "no instance" error.) Ideally we'd write something like this:

class CONTAINS a as where
    contains :: Contains a as

instance CONTAINS a (a ': as) where
    contains = Here

instance CONTAINS a as => CONTAINS a (b ': as) where
    contains = There contains  -- recursively call `contains` on the sublist

but this fails the overlapping instance rule. Instance contexts and type equalities are not inspected during instance search - the elaborator doesn't backtrack - so neither of these instances is more specific than the other.

Fortunately there's a well-known solution to this problem. It involves using a closed type family to tell a and b apart. You define an auxiliary class CONTAINS' with an extra parameter, in this case a Bool telling you whether a can be found at the head of as.

class CONTAINS' (eq :: Bool) a (as :: [*]) where
    contains' :: Contains a as

Then you define instances for the cases when eq is True or False. The elaborator can tell these instances apart, because True and False are visibly different. Note that the step case recursively calls CONTAINS.

instance CONTAINS' True a (a ': as) where
    contains' = Here

instance CONTAINS a as => CONTAINS' False a (b ': as) where
    contains' = There contains

Finally you define your CONTAINS instance in terms of CONTAINS', and use the result of ==, a closed type family which tests whether its arguments are equal, to pick an instance.

instance CONTAINS' (a == b) a (b ': as) => CONTAINS a (b ': as) where
    contains = contains' @(a == b)

(This is one of the very few acceptable uses of Boolean type families.)

Now you can use CONTAINS as you would any other class. When you try and instantiate a and as GHC will attempt to search for an a inside as, and the contains method will return its index.

example :: Contains Int '[Bool, Int, Char]
example = contains

-- "no instance for CONTAINS"
failingExample :: Contains String '[Bool, Int, Char]
failingExample = contains

This is a fairly simple example and the code is already quite messy. You can definitely approach the example in your question in the same manner, but all told I'm not convinced that static checking is worth the complexity in this instance. Have you considered an implementation based on Typeable?