Custom Eq instance for Singletons

Learn
1

I need some guidance regarding singletons.

So, I’m trying to generate a custom Eq instance for my singletons:

type Name = [Char] 
$(singletons [d|
  newtype TVar' = TV [Char] deriving (Eq)
  data Types 
    = TCon Name [Types]
    | TVar TVar' 

  instance Eq Types where 
    (==) (TCon a xs) (TCon b ys) = 
      ((a == ['T','O','P']) && ... )
    :
    :
    :
  |])

But i can already see that this is going to be very painful to work with.

  • I have to write strings as their list representation instead of their sugated version "TOP". Otherwise I get a could not deduce SIsString [Char] error.
  • I cannot pattern match on literals, so (==) (TCon ['T','O','P'] xs) (TCon ['T','O','P'] ys) yields an error

I could of course, work with Nat instead of names, and have a structure that remembers the mappings. But I would like to avoid that. Is there a better methodology to follow?

2

The challenge is that "TOP" has a different representation at the term level versus the type level. At the term level, "TOP" is a String (or, more generally, any instance of IsString). At the type level, "TOP" is a Symbol, and you can’t easily create Symbol values at the term level. Somehow, we have to convince singletons to use a String-like thing at the term level and a Symbol at the type level.

This requires some advanced singletons usage, but one way to accomplish this would be to follow the advice listed in this section of the singletons README. That is, create two different versions of your data type at the term and type level:

-- Term level
data Types = TCon Text [Types] | ...

-- Type level
data PTypes = PTCon Symbol [Types] | ...

And then override singletons-th’s Template Haskell options to ensure that it promotes Types to PTypes, TCon to PTCon, etc.

3 Likes
3

omg thats brilliant, thank you so much! i totally forgot that main package had this documented