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?

ghc@7.10.3, singletons@2.1

You can remove the warning in `from'` by adding functions `storeHead :: Store e (s ': ss) -> e s` and `storeTail :: Store e (s ': ss) -> Store e ss` and use them on the store after you've matched `AtHead` or `InTail`. — cchalmers, Jul 10 '16 at 11:51
Your two `HasElemC` instances overlap. GHC will find it impossible to discharge a `HasElemC` constraint because it doesn't check preconditions when doing proof search. Fortunately there's [a well-known trick using type families and `UndecidableInstances`](https://wiki.haskell.org/GHC/AdvancedOverlap). (In fact this is one of the few good uses of Boolean type families.) — Benjamin Hodgson, Jul 10 '16 at 19:23
Thank you cchalmers, that worked. Thanks, Benjamin. Overlaps are fine in my case: I don't need functions polymorphic in ss. Although I might need them in the future. — NioBium, Jul 10 '16 at 19:43
@NioBium I think you're misunderstanding me: `HasElemC` is _useless_ because of the way you've defined your instances. Try writing `x = HasElem "a" '["a"]; x = hasElem`. It won't type-check. — Benjamin Hodgson, Jul 10 '16 at 21:18
No, I understand you. My code using `from` does type-check and runs correctly. You just need to mark AtHead instance OVERLAPPING/InTail instance OVERLAPPABLE. Are you saying it shouldn't? — NioBium, Jul 10 '16 at 21:38
NioBium, I think maybe @BenjaminHodgson may just dislike overlapping instances sufficiently that he's not tried too hard to learn how to use them; it's very often better to learn how *not* to. The type family trick will be pickier, unfortunately. For example, the type family thing will refuse to select an instance using a polymorphic inequality like `a /~ (q ': a)` because type families can represent infinite types. Overlapping instances will happily do so because it doesn't affect type safety. — dfeuer, Jul 11 '16 at 03:43

score 8 · Answer 1 · edited May 23 '17 at 12:01

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.

Thank you. I was just trying not to invent the wheel. Still hoping someone would provide a solution in Haskell singletons, if one exists. What's the point in lifting all of those functions to type-level, if you can't use them in proofs? — NioBium, Jul 10 '16 at 19:47
Well, singletons are (and `singletons` is) one particular mode of use of GADTs and data-kinds. Proof-terms like `Elem` are another. They don't naturally fit into the singleton framework because they're not singletons! — Benjamin Hodgson, Jul 10 '16 at 21:11

Idiomatic boolean equality usage (singletons)

1 Answers1

Linked