`coerce` и создание переменных типа

Question

Рассмотрим следующую сессию GHCi:

>:set -XTypeApplications
>import Data.Map.Strict
>import GHC.Exts
>newtype MySet a = MySet (Map a ())
>let member' :: Ord a => a -> MySet a -> Bool; member' = coerce member

<interactive>:21:57: error:
    * Couldn't match representation of type `a0' with that of `()'
        arising from a use of `coerce'
    * In the expression: coerce member
      In an equation for member': member' = coerce member
>let member' :: Ord a => a -> MySet a -> Bool; member' = coerce (member @_ @())

У меня есть догадка о том, что здесь происходит: проверка типа должна удовлетворить Coercible (Ord a => a -> Map a b -> Bool) (Ord a => a -> MySet a -> Bool) и не в состоянии создать экземпляр b в этом ограничении (),

Есть ли более элегантный способ, чем сделать это с -XTypeApplications?

Редактировать: я особенно ищу решения, которые имеют дело со многими случаями MySet a в типе, например union :: Ord a => MySet a -> MySet a -> MySet a,

Answer 1

member :: Ord a => a -> Map a b -> Bool
member' :: Ord a => a -> MySet a -> Bool

GHC должен принять

Coercible (Map a b) (MySet a)

Он видит что

Coercible (MySet a) (Map a ())

что оставляет это нуждающимся

Coercible (Map a ()) (Map a b)

что приводит к

Coercible () b

Но что это b? Это неоднозначно. В этом случае не имеет значения, что b есть, потому что по параметричности, member не может заботиться Так что было бы совершенно разумно выбрать b ~ () и разрешить принуждение тривиально. Но GHC, как правило, не выполняет такой параметрический анализ при выводе типов. Я подозреваю, что это может быть сложно изменить это. В особенности, всякий раз, когда вывод типа "угадывает", существует риск, что он может ошибиться и заблокировать вывод где-то еще. Это большая банка червей.

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

Answer 2

Решение с TypeApplications довольно просто:

{-# LANGUAGE TypeApplications #-}

import Data.Coerce
import qualified Data.Map as M

newtype Set a = Set (M.Map a ())

member :: Ord a => a -> Set a -> Bool
member = coerce (M.member @_ @())

union :: Ord a => Set a -> Set a -> Set a
union = coerce (M.union @_ @())

Обратите внимание, что некоторые функции требуют более или менее подстановочных знаков, например,

smap :: (Ord b) => (a -> b) -> Set a -> Set b
smap = coerce (M.mapKeys @_ @_ @())

Чтобы определить, как именно вы должны указать тип приложения (кроме проб и ошибок), используйте

>:set -fprint-explicit-foralls
>:i M.mapKeys
M.mapKeys ::
  forall k2 k1 a. Ord k2 => (k1 -> k2) -> M.Map k1 a -> M.Map k2 a

Порядок переменных, из которого вы получаете :i тот же самый, используемый TypeApplications,

Обратите внимание, что вы не можете использовать coerce за fromList - это не ограничение, это просто не имеет смысла:

fromList :: Ord a => [a] -> Set a
fromList = coerce (M.fromList @_ @())

Это дает ошибку

* Couldn't match representation of type `a' with that of `(a, ())'

Лучшее, что вы можете сделать здесь, это, вероятно,

fromList :: Ord a => [a] -> Set a
fromList = coerce (M.fromList @_ @()) . map (flip (,) ())