Idiomatic boolean equality usage (singletons)

Question

I want to create a data structure to store items tagged on type level using Symbol. This:

data Store e (ss :: [Symbol]) where
  Nil :: Store e '[]
  Cons :: e s -> Store e ss -> Store e (s ': ss)

data HasElem (a :: k) (as :: [k]) where
  AtHead :: HasElem a (a ': as)
  InTail :: HasElem a as -> HasElem a (b ': as)

class HasElemC (a :: k) (as :: [k]) where hasElem :: HasElem a as
instance HasElemC {OVERLAPPING} a (a ': as) where hasElem = AtHead
instance HasElemC a as => HasElemC a (b ': as) where hasElem = InTail hasElem

from :: HasElemC s ss => Store e ss -> e s
from = from' hasElem

from' :: HasElem s ss -> Store e ss -> e s
-- from' _ Nil = undefined
from' h (Cons element store) = case h of
  AtHead -> element
  InTail h' -> from' h' store

kinda works, if you neglect the fact that compiler warns me for not supplying from' _ Nil definition (why does it, by the way? is there a way to make it stop?) But what I really wanted to do in the beginning was to use singletons library in idiomatic fashion, instead of writing my own type-level code. Something like this:

import Data.Singletons.Prelude.List

data Store e (ss :: [Symbol]) where
  Nil :: Store e '[]
  Cons :: Sing s -> e s -> Store e ss -> Store e (s ': ss)

from :: Elem s ss ~ True => Store e ss -> e s
from (Cons evidence element nested) = ???

Sadly I could not figure out how to convert the context to a propositional equality. How can you use building blocks from singletons library to do what I'm trying to do?

[email protected], [email protected]

Answer 1

Don't use Booleans! I seem to keep repeating myself on this point: Booleans are of extremely limited usefulness in dependently-typed programming and the sooner you un-learn the habit the better.

An Elem s ss ~ True context promises to you that s is in ss somewhere, but it doesn't say where. This leaves you in the lurch when you need to produce an s-value from your list of ss. One bit is not enough information for your purposes.

Compare this with the computational usefulness of your original HasElem type, which is structured like a natural number giving the index of the element in the list. (Compare the shape of a value like There (There Here) with that of S (S Z).) To produce an s from a list of ss you just need to dereference the index.

That said, you should still be able to recover the information you threw away and extract a HasElem x xs value from a context of Elem x xs ~ True. It's tedious, though - you have to search the list for the item (which you already did in order to evaluate Elem x xs!) and eliminate the impossible cases. Working in Agda (definitions omitted):

recover : {A : Set}
          (_=?_ : (x : A) -> (y : A) -> Dec (x == y))
          (x : A) (xs : List A) ->
          (elem {{_=?_}} x xs == true) ->
          Elem x xs
recover _=?_ x [] ()
recover _=?_ x (y :: ys) prf with x =? y
recover _=?_ x (.x :: ys) prf | yes refl = here
recover _=?_ x (y :: ys) prf | no p = there (recover _=?_ x ys prf)

All this work is unnecessary, though. Just use the information-rich proof-term to start with.

---

By the way, you should be able to stop GHC warning you about incomplete patterns by doing your Elem matching on the left hand side, rather than in a case-expression:

from' :: HasElem s ss -> Store e ss -> e s
from' AtHead (Cons element store) = element
from' (InTail i) (Cons element store) = from' i store

By the time you're on the right-hand side of a definition, it's too late for pattern-matching to refine the possible constructors for other terms on the left.