Каков вариант использования eqT вместо приведения?

#haskell

Вопрос:

В Data.Typeable нем есть приведение функции

 cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b

и функция eqT

 eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)

Они кажутся почти идентичными по эффекту и реализации, мне было интересно, есть ли какой-либо практический смысл в описании eqT: извлеките свидетельство равенства двух типов.

1. Вы можете легко реализовать cast из eqT . Хотя вы также можете реализовать eqT from cast , это не так очевидно, IMO (сначала я думал, что это невозможно! Я рекомендую попробовать это в качестве упражнения.). Это потому eqT , что позволяет case eqT @a @b of Just Refl -> ... , который сообщает компилятору предположить a~b в ... , и это предположение автоматически обрабатывается компилятором по мере необходимости, что является очень мощным. Для сравнения, cast только позволяет конвертировать a в (возможно) b , и это само по себе не дает указания проверке типов что-либо предполагать.

Ответ №1:

Это неудобно:

 checkEq :: forall a b. (Typeable a, Typeable b, Eq b) => a -> a -> Maybe Bool
checkEq a a' = do
    b  <- cast @_ @b a
    b' <- cast a'
    pure (b == b')

Внутренне это дважды проверяет приведение и выполняет два Maybe сопоставления с шаблоном. Но как только мы выполним одно приведение, мы знаем, что другое будет успешным!

Это лучше:

checkEq a a' = (Refl -> a == a') <

gt; eqT @a @b
Только одна проверка, только одно Maybe совпадение с шаблоном.

Такого рода вещи часто возникают, когда у вас есть Typeable вещи, определяемые количественно в структурах данных, и вы хотите выполнять над ними операции, которые принимают несколько аргументов. Приведение равенства типов в область видимости один раз (с Refl помощью шаблона), а затем возможность использовать это равенство несколько раз, является как более удобным, так и более эффективным, чем повторный cast ввод.

Редактировать

чи указывает, что в данном случае на самом деле можно сделать только одно cast :

 checkEq a a' = (eq -> eq a a') <

gt; cast ((==) @b)

checkEq a a' = uncurry ((==) @b) <

gt; cast (a, a')

 

В общем случае вы можете создать кортеж из всех операций, которые вам нужно выполнить, или всех значений, которые вам нужно выполнить. Я думаю, что на самом деле это не оставляет мне веских технических аргументов ни в пользу того, ни в пользу другого!

1. Я на 100% согласен. Кажется, есть способ использовать только один cast , но это еще более неудобно: определить foo :: b -> b -> Maybe Bool , а затем case cast foo :: Maybe (a->b->Bool) of ... , который работает, потому что, когда a~b у нас есть (b->b->Bool)~(a->b->Bool) . eqT намного проще в использовании и гораздо удобнее для чтения.

2. @chi О, здорово! Я включу некоторые комментарии по этому поводу.