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 AnyNameEq 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.
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.
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
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)
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.
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 It is an foreign imported thingy.
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:
It is an foreign imported thingy.