Alternative to Typeable in PureScript

Help
#1

Hi all,

I’ve a question about the status of Typeable in PureScript.

What I like to do is check at runtime that the type of a container I have and the type of input from the user are equal. A simplified version in Haskell using GADTs where the type a in Input is existential:

data Container :: Type -> Type where
  Elem :: Typeable a => a -> Container a
  -- more omitted --

data Input :: Type where
  Change :: Typeable a => a -> Input
  -- more omitted --

During runtime using eqT and :~::

handle :: formal a. Container a -> Input -> Container a
handle (Elem old_val) (Change new_val)
  -- this is allowed because the compiler now knows
  -- `old_val` and `new_val` have the same type due to matching on `Refl`
  | Just Refl <- sameT old_val new_val = Edit new_val
  | otherwise = Edit old_val
  where
    sameT :: ( Typeable a, Typeable b ) => a -> b -> Maybe (a :~: b)
    sameT _ _ = eqT

I’ve found this old library, which doesn’t work any more. Also, I’ve found this GitHub issue talking about automatically generating Typeable instances by the compiler. It mentions that “it’s almost always a nice idea to explore alternatives to Typeable.” However, it doesn’t mention any.

Is there some alternative I could use? Should I revive Typeable?

1 Like
Purescript-Typeable
#2

I think the alternative that’s gotten the most usage is polymorphic variants (something equivalent to https://github.com/natefaubion/purescript-variant). You still have to lift things into a wrapper, but it can be done in a modular way with good inference due to row types.

As an example, most Haskell extensible effects libraries use Typeable, but the same thing can be done in PureScript with polymorphic variants over Free https://github.com/natefaubion/purescript-run

1 Like
#3

I looked around in the libraries you mention, and I see there are some row tricks used there. However, I fail to see how I could use that in my use case. Could you give me a short example how to match types at runtime using poly variants to make this more clear for me?

1 Like
#4

First thing is you have to accept that you aren’t going to get the same thing as Typeable :smiley:. If you are looking to recover the same functionality as Typeable, you are going to be disappointed.

Typeable is “just” a unique hash of some type coupled with a coercion. This lets us defer our knowledge of some type to runtime, and otherwise completely forget about it, which can be really useful in frameworky stuff. Combined with GADTs, you can existentially pack up these hashes. There is no “safe” way to do exactly this in PureScript.

import Data.Leibniz (type (~))

newtype TypeRep = TypeRep String

derive instance eqTypeRep :: Eq TypeRep

class NaiveTypeable a where
  typeRep :: a -> TypeRep

eqT :: forall a b. NaiveTypeable a => NaiveTypeable b => a -> b -> Maybe (a ~ b)
eqT a b
  | typeRep a == typeRep b = Just (unsafeCoerce identity)
  | otherwise = Nothing

data Foo

instance typeableMyFoo :: NaiveTypeable Foo where
  typeRep _ = TypeRep "Data.Foo#Foo"

The whole reason Typeable is only compiler derived is because it relies on the user constructing their own hash, which is inherently unsafe.

So how does Variant solve some of the same problems? It doesn’t. Or at least not, directly. Any alternative to Typeable is to “just” not forget about the types. If you write everything over a unified closed sum, then you always know what everything can be. However this means the user has to write some larger data type to encompass all the cases they want in their program, which isn’t very modular. Variant lets one use polymorphic sums, which means you can define different branches in a fairly modular way, and have them unify when you use them together. So Variant does not solve the Typeable problem, but it makes the case of not having Typeable much easier to deal with, by not have to maintain a monolithic closed sum.

In the case of something like extensible effects, Typeable is used to implement an open union, where types can exist together, discriminated by their TypeRep. Variant and row-types solve a subset of that problem in a way that is mostly ergonomic and fully inferrable.

I can’t speak directly to your problem because it isn’t complete (you’ve brought up an XY problem). You’ve proposed a situation that is only solved by Typeable, and then asked how things that are not Typeable solve it. The question to ask at that point is, “How would I solve this with only ADTs and no Typeable?”, which is likely to be unergonomic, but can likely be made a lot nicer with the alternatives.

2 Likes
Passing on different types of Records
#5

LOL, you’re totally right I posted an XY question :laughing: I’ll take a look at the alternatives again and think about if I can solve my problem in another way, although I think that it will indeed be unergonomic.

Indeed the best (actually the only) way to implement Typeable is by letting the compiler derive instances. Just following my train of thought: the compiler can already generate representations for Data.Generic.Rep. As type reflection is more or less lowering the rep to the value level, would it be possible to reuse this machinery for Typeable? Although I think Generic is more restricted and applicable to less data types than Typeable is… Maybe when I’ll have some more time in a couple of months I could take a look into this.

1 Like