Haskell Data.Unique

Viewed 165

I need to rename variables for an application where I am unifying terms, and the way I have done it in the past has been to use (gensym)-like features, and replace the name of the var with the gensym-ed name, usually mangled to a string. I also need to compare the names of variables.

so (rename (logvar1 "foo")) would return (logvar1 "#:23322) - or whatever, and I can get hold of the "#:23322" and check it against any other logical vars in the terms.

In haskell, I am not sure how to do that. I have found Data.Unique, which returns a IO Unique. Unique is part of Eq, but of course IO Unique isn't.

What is the best way to write this function

m = newUnique
n = newUnique

test :: (Monad m, Eq a) => m a -> m a -> m Bool
test u1 u2 = do
  v1 <- u1
  v2 <- u2
  if v1 == v2 then return True else return False

I would like True of False back, not IO True or IO False.

Of course, you can't always get what you want.....

I'm grateful for any help. I understand why the IO is there, I'm just not sure how best do deal with it in the rest of my program where I just want to compare

2 Answers

The idea of this library is that in the part of your program where you need to generate unique labels, you use IO. Later, when you only need to compare unique labels, no IO is needed

main :: IO ()
main = do
  x <- newUnique
  y <- newUnique
  print $ same x y

same :: Eq a => a -> a -> Bool
same = (==)

I've defined an alias for (==) just to make it clear that there is no IO involved in comparisons, only in label creation.

You could do the same thing using State instead of IO, and implementing your own gensym with that. The advantage of that approach would be that you could get more transparent gensyms, e.g. giving them a name and a unique number instead of just an opaque unique identifier.

I don't think your test signature makes sense. You shouldn't compare monadic values – that would be comparing generators of unique values, not unique values themselves.

You do need a monad for generating the unique keys, because a non-monadic generator could not know about other ones that have already been generated; however doing this in IO is a bit overkill, a dedicated special monad would be better. prim-uniq offers such generators: they can be used either in IO like Data.Unique.newUnique, but also locally in the ST monad.

type VarId s = Uniq s

data Expr s = LogVar (VarIs s)
            | ...
  deriving (Eq)

rename :: (PrimMonad m, s ~ PrimState m)
              => Expr s -> m (Expr s)
rename (LogVar _) = LogVar <$> getUniq
rename ... = ...
Related