Почему я должен приводить этот тип данных по полям, а не по всем сразу? - PullRequest
Новая
       19

Почему я должен приводить этот тип данных по полям, а не по всем сразу?

8 голосов
/ 27 июня 2019

У меня есть два типа (<->) и (<-->), представляющие изоморфизмы между типами: 

data Iso (m :: k -> k -> *) a b = Iso { to :: m a b, from :: m b a }
type (<->) = Iso (->)
infix 0 <->

data (<-->) a b = Iso' { to' :: a -> b, from' :: b -> a }
infix 0 <-->

Единственное различие между ними состоит в том, что (<->) - это специализация более общего типа.

Я могу coerce (<-->) изоморфизмы легко: 

coerceIso' :: (Coercible a a', Coercible b b') => (a <--> b) -> (a' <--> b')
coerceIso' = coerce

Но я получаю ошибку, когда пытаюсь сделать то же самое с (<->) изоморфизмами: 

coerceIso :: (Coercible a a', Coercible b b') => (a <-> b) -> (a' <-> b')
coerceIso = coerce
{-
src/Data/Iso.hs:27:13: error:
    • Couldn't match type ‘a’ with ‘a'’ arising from a use of ‘coerce’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          coerceIso :: forall a a' b b'.
                       (Coercible a a', Coercible b b') =>
                       (a <-> b) -> a' <-> b'
        at src/Data/Iso.hs:25:1-73
      ‘a'’ is a rigid type variable bound by
        the type signature for:
          coerceIso :: forall a a' b b'.
                       (Coercible a a', Coercible b b') =>
                       (a <-> b) -> a' <-> b'
        at src/Data/Iso.hs:25:1-73

-}

Мой текущий способ обхода заключается в том, чтобы принудительно выполнять функции перемотки вперед и назад: 

coerceIso :: (Coercible a a', Coercible b b') => (a <-> b) -> (a' <-> b')
coerceIso (Iso f f') = Iso (coerce f) (coerce f')

Но зачем такой обходной путь необходим? Почему нельзя (<->) принуждаться напрямую?

Ответы [ 2 ]

9 голосов
/ 27 июня 2019

Проблема заключается в роли аргументов m в вашем общем типе Iso.

Рассмотрим: 

data T a b where
  K1 :: Int    -> T () ()
  K2 :: String -> T () (Identity ())

type (<->) = Iso T

Вы не можете ожидать, что сможете конвертировать T () () в T () (Identity ()), даже если () и Identity () являются принудительными.

Вам понадобится что-то вроде (псевдокод): 

type role m representational representational =>
          (Iso m) representational representational

но это не может быть сделано в текущем Haskell, я считаю.

2 голосов
/ 28 июня 2019

Не прямой ответ, но я хочу поделиться этой уловкой: всякий раз, когда m является profunctor (я подозреваю, что это обычно будет), вы можете использовать преобразование типа Yoneda, чтобы сделатьэквивалентный тип с аргументами представления. 

newtype ProYo m a b = Yo2 (forall x y. (x -> a) -> (b -> y) -> m x y)

ProYo m изоморфен m, за исключением того, что его роли аргументов являются репрезентативными по следующему изоморфизму: 

toProYo :: (Profunctor m) => m a b -> ProYo m a b
toProYo m = ProYo (\f g -> dimap f g m)

fromProYo :: ProYo m a b -> m a b
fromProYo (ProYo p) = p id id

Если мы определим вашIso в терминах этого 

data Iso m a b = Iso { to :: ProYo m a b, from :: ProYo m b a }

coerceIso проходит без изменений.

...