Data.Typeable.cast в экзистенциальный тип

К тому времени, как ваш Haskell будет переведен в GHC Core, классы (и сопутствующие конструкции логического программирования, такие как имплициация) исчезнут. Они преобразуются компилятором в код передачи словаря — каждый instance становится записью (обычным значением), а каждый метод становится членом этой записи. (Для более подробной информации см. мой предыдущий ответ.)

Таким образом, конструктор, который упаковывает ограничение,

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

действительно представлен во время выполнения обычным типом продукта,

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

где поле c a — это словарь методов времени выполнения, представляющий экземпляр c a.

Чтобы преобразовать Obj c в Obj c' во время выполнения, даже если бы у вас был способ проверить, что конкретное a является экземпляром как c, так и c', вам все равно нужно каким-то образом синтезировать словарь для c'. Поскольку c' обычно содержит больше методов, чем c, это равносильно тому, чтобы попросить компьютер написать для вас программу.

Как упоминал Дэвид в комментариях, я думаю, что ваш лучше всего было бы встроить знания о вашей конкретной иерархии классов в вашу систему времени выполнения в рамках предположения о закрытом мире. Если у вас есть оракул, который может искать фактическую среду выполнения экземпляра, словарь,

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

тогда вы можете написать cast (с некоторыми неудобными спорами типа):

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

Обратите внимание, что этот cast фактически позволяет вам (попытаться) изменить интерфейс вашего объекта на любой другой интерфейс, а не только те, которые являются производными от статического типа объекта. (В C# вы можете сделать это путем повышения до object, а затем понижения.) Вы можете предотвратить это, потребовав entailment в контексте cast:

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

(Конечно, это следствие не будет использоваться во время выполнения.)

Задача состоит в том, чтобы реализовать oracle! Я думаю, что это будет одна из тех задач, которые неинтересны, поэтому я просто дам вам пару советов.

Ваша монада Runtime, вероятно, будет чем-то вроде Reader с таблицей поиска, отображающей (TypeReps) as и cs в словари. as и cs должны быть экзистенциально количественно определены, чтобы хранить их в неоднородном списке.

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

type MonadRuntime = MonadReader [TableEntry]

Затем oracle нужно будет найти TableEntry, соответствующий паре класс/тип, затем открыть экзистенциал, установить равенство типов, разобрав typeRep, и вернуть Just Dict. (В частности, эта часть звучит как кошмар для написания кода.)

Прежде чем запускать программу MonadRuntime, вам нужно создать Table, содержащую все экземпляры, о которых заботится ваша программа.

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

В общем, я не понимаю, как это может стоить головной боли. Классы типов фундаментально отличаются от ОО-классов (и они даже не очень похожи на ОО-интерфейсы), поэтому неудивительно, что их сложно использовать для моделирования ОО-классов.