Phantom type and Data.Exists

#1

I was trying to port the following Haskell code:

data Name a = Fn String !Integer
            | Bn !Integer !Integer
            deriving (Eq, Ord)

data AnyName where
  AnyName :: Typeable a => Name a -> AnyName

instance Eq AnyName where
  (AnyName n1) == (AnyName n2) = case gcast n2 of
    Just n2' -> n1 == n2'
    Nothing -> False

With the help of Data.Exists module, I managed to get this far:

import Data.Exists

data Name a
  = Fn String Int
  | Bn Int Int

derive instance eqName :: Eq (Name a)
derive instance ordName :: Ord (Name a)

data AnyName = AnyName (Exists Name)

instance eqAnyName :: Eq AnyName where
  eq (AnyName x) (AnyName y) = undefined

and got stuck.

What the original Haskell AnyName Eq does is comparing the type of existentially hidden phantom types first and only comparing the actual values if types are the same.

Because the phantom type is existentially hidden, in Purescript I have to mimic that with Data.Exists. But then again, how can I compare the types when implementing Eq instance? Even if I get pass that, how to compare the actual values? unsafeCoerce lhs == rhs simply throws EscapedSkolem error.

How would you write the Eq instance for AnyName? Is it possible at all?

The same goes for the Ord instance. I want to store AnyName in a Map or Set.

#2

You’ll need something like Typeable, which in Haskell is a bit like this:

class Typeable a where
  typeRep :: Proxy a -> TypeRep

and then you can define something along the lines of

cast :: (Typeable a, Typeable b) => a -> Maybe b
cast x | typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b) = Just (unsafeCoerce x)
cast _ = Nothing

ie. check whether the TypeRep values for a and b are the same, and if they are, it’s okay to use unsafeCoerce to convert an a to a b.

Without Typeable, you have no way of knowing that the two AnyName values you are trying to compare for equality actually have the same type packaged up inside them. Unlike Haskell, PureScript has no built-in Typeable class. You could define your own Typeable class, but allowing users to write their own instances is a little bit dangerous, because you’re completely reliant on people writing correct instances.

1 Like
#3

That worked! I have to salvage a seemingly abandoned purescript-typeable project and resort to Oleg’s version of Exists since the Data.Exists seems to be too liberal and have no Typeable constraints on any of its type variables.

The cast function would trigger EscapedSkolem error. So I have to fall back to String. Performance wise, it is probably terrible :upside_down_face:

Anyway, here is the code:

import Data.Tuple (Tuple(..))
import Data.Typeable (class Typeable, class Typeable1, TypeRep, mkTyRep, typeOf)
import Type.Proxy (Proxy(..))

data Name a
  = Fn String Int
  | Bn Int Int

derive instance eqName :: Eq (Name a)
derive instance ordName :: Ord (Name a)

instance typeable1Name :: Typeable1 Name where
  typeOf1 _ = mkTyRep "Unbound" "Name"

-- | Existential quantification using the universal one.
-- |
-- | By Oleg Grenrus "More GADTs in PureScript"
newtype Exists f = Exists { runExists :: forall r. (forall a. Typeable a => f a -> r) -> r }

mkExists :: forall f a. Typeable1 f => Typeable a => f a -> Exists f
mkExists x = Exists { runExists: \f -> f x }

data AnyName = AnyName (Exists Name)

instance eqAnyName :: Eq AnyName where
  eq (AnyName (Exists a)) (AnyName (Exists b)) = a' == b'
    where
    a' = a.runExists repr
    b' = b.runExists repr

instance ordAnyName :: Ord AnyName where
  compare (AnyName (Exists a)) (AnyName (Exists b)) = compare a' b'
    where
    a' = a.runExists repr
    b' = b.runExists repr

repr :: forall a. Typeable a => Name a -> Tuple TypeRep String
repr x = Tuple (typeOf (Proxy :: Proxy (Name a))) (show x)
#4

Data.Exists seems to be too liberal

Can you clarify what you mean? The only reason a Typeable constraint would be necessary is if you need to try and recover what the original type was. Data.Exists specifically does not let you do that, requiring the consumer to be polymorphic over that domain and it’s constraints. I would consider the Typeable version to be more liberal.

#5

I should’ve been more specific. It is only too liberal for this specific use case. If I swap Data.Exists in, the code won’t compile. And in fact, I have to add several Typeable constraints to Oleg’s version too.

I have no idea how to do that to Data.Exists :sweat_smile: It is an foreign imported thingy.

#6

And that terrible String can be dropped after all. Using a dummy type works:

repr :: forall a. Typeable a => Name a -> Tuple TypeRep (Name Int)
repr x = Tuple (typeOf (Proxy :: Proxy (Name a))) (unsafeCoerce x)
#7

This has worked until it meets Monad. I couldn’t figure out how to lift runExists into a Monad. But this whole exercise helps me realize that AnyName is no more than a fancy type-tagged value, so why not make it explicit:

newtype AnyName = AnyName (Tuple TypeRep (Name Int))

Simplicity prevails, again.