Data.Typeable.cast to an existential type

Question

So this is a continuation of my object system saga (part 1, part 2).

This part essentially boils to the following.

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}

import Data.Typeable
import GHC.Exts (Constraint)

data Obj (cls :: * -> Constraint) = forall o. (cls o, Typeable o) => Obj o

downcast :: Obj a -> Maybe (Obj b)
downcast (Obj x) = do
                     cx <- cast x
                     return $ Obj cx

The definition of downcast fails with this error:

• Could not deduce: b o0 arising from a use of ‘Obj’
  from the context: (a o, Typeable o)
    bound by a pattern with constructor:
               Obj :: forall (cls :: * -> Constraint) o.
                      (cls o, Typeable o) =>
                      o -> Obj cls,
             in an equation for ‘downcast’
    at downcast.hs:12:11-15
• In the second argument of ‘($)’, namely ‘Obj cx’
  In a stmt of a 'do' block: return $ Obj cx
  In the expression:
    do cx <- cast x
       return $ Obj cx
• Relevant bindings include
    cx :: o0 (bound at moo.hs:13:22)
    downcast :: Obj a -> Maybe (Obj b) (bound at downcast.hs:12:1)

I don't quite understand why this error happens :( Can it be fixed?

Answer 1

By the time your Haskell is translated into GHC Core, the classes (and the attendant logic programming constructs such as impliciation) are nowhere to be seen. They are transformed by the compiler into dictionary passing code — each instance becomes a record (a regular value) and each method becomes a member of that record. (For more specifics, see a previous answer of mine.)

So a constructor which packages up a constraint,

data Obj c where  -- I'm using GADT syntax
    Obj :: c a => a -> Obj c

is really represented at runtime by a regular product type,

data Obj c where
    Obj :: c a -> a -> Obj c

where the c a field is the runtime method dictionary representing the c a instance.

To downcast an Obj c to an Obj c' at runtime, even if you had a way to test that the concrete a was an instance of both c and c', you'd still have to somehow synthesise a dictionary for c'. Since c' will generally contain more methods than c, this amounts to asking the computer to write a program for you.

---

As David mentioned in the comments, I think your best bet would be to build knowledge about your specific class hierarchy into your runtime system under a closed-world assumption. If you have an oracle which can look up an instance's actual runtime dictionary,

oracle :: MonadRuntime m => TypeRep a -> TypeRep c -> m (Maybe (Dict (c a)))

then you can write cast (with some uncomfortable type wrangling):

data Obj c where
    Obj :: c a => TypeRep a -> a -> Obj c

cast :: forall c c' m. (MonadRuntime m, Typeable c') => Obj c -> m (Maybe (Obj c'))
cast (Obj tr x) = do
    mdict <- oracle tr (typeRep @c')
    case mdict of
        Just Dict -> return (Just (Obj tr x))
        Nothing -> return Nothing

Note that this cast actually lets you (attempt to) change your object's interface to any other interface, not just those which are derived from the object's static type. (In C# you can do this by upcasting to object and then downcasting.) You can prevent this by requiring an entailment in cast's context:

cast :: forall c c' m. (MonadRuntime m, Typeable c', Class c c') => Obj c -> m (Maybe (Obj c'))

(Of course, that entailment would not actually be used at runtime.)

---

The challenge is to implement oracle! I think it’s going to be one of those challenges which is not fun so I'll just give you a pointer or two.

Your Runtime monad will probably be some sort of Reader with a lookup table mapping (the TypeReps of) as and cs to dictionaries. The as and cs will need to be existentially quantified in order to store them in a heterogeneous list.

data TableEntry where
    TableEntry :: c a => TypeRep c -> TypeRep a -> TableEntry

type MonadRuntime = MonadReader [TableEntry]

Then oracle will need to look up the TableEntry matching the class/type pair, then open the existential, establish the type equality by taking apart the typeReps, and return Just Dict. (This part in particular sounds like a nightmare to code up.)

Before you run your MonadRuntime program you'll need to construct the Table containing all of the instances your program cares about.

table = [
    TableEntry (typeRep @Ord) (typeRep @Int),
    TableEntry (typeRep @Eq) (typeRep @Bool)
    ]

---

All in all I don’t see how it could possibly be worth the headache. Type classes are fundamentally unlike OO classes (and they're not even that much like OO interfaces), so it's really not surprising that it's hard to use them to model OO classes.