Принуждение и роли - не могут компилироваться с подписью типа GHCi - PullRequest
Новая
       7

Принуждение и роли - не могут компилироваться с подписью типа GHCi

0 голосов
/ 15 ноября 2018

Введите следующее в GHCi 

>:set -XAllowAmbiguousTypes
>import Data.Coerce
>fcm f = coerce . foldMap (coerce . f)
>:t fcm
fcm
  :: (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) =>
     (a3 -> a2) -> t a3 -> c

Хорошо, это то, что я ожидаю. Скопируйте и вставьте это в файл. 

{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Coerce

fcm :: (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) 
    => (a3 -> a2) -> t a3 -> c
fcm f = coerce . foldMap (coerce . f)

Теперь, если вы загрузите это в GHCi, вы получите ошибку - 

Weird.hs:7:9: error:
    • Couldn't match representation of type ‘a0’ with that of ‘c’
    arising from a use of ‘coerce’
      ‘c’ is a rigid type variable bound by
    the type signature for:
      fcm :: forall (t :: * -> *) a1 c a2 a3.
             (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) =>
             (a3 -> a2) -> t a3 -> c
    at Weird.hs:(5,1)-(6,30)
    • In the first argument of ‘(.)’, namely ‘coerce’
      In the expression: coerce . foldMap (coerce . f)
      In an equation for ‘fcm’: fcm f = coerce . foldMap (coerce . f)
    • Relevant bindings include
    fcm :: (a3 -> a2) -> t a3 -> c (bound at Weird.hs:7:1)

А? Откуда взялся a0? Если вы удалите сигнатуру типа, код снова будет хорошо скомпилирован. Похоже, у нас теперь есть функция, тип которой мы не можем объяснить компилятору, и GHCi не может сказать нам, что это за тип (он может только давать нам ошибки). GHC, похоже, говорит о внутренних переменных типа (в данном случае a0), которые не предназначены для пользователя.

Это имеет какое-то отношение к черной магии, окружающей Кэррибли? От GHC. Типы : 

Note [Kind-changing of (~) and Coercible]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

(~) and Coercible are tricky to define. To the user, they must appear as
constraints, but we cannot define them as such in Haskell. But we also cannot
just define them only in GHC.Prim (like (->)), because we need a real module
for them, e.g. to compile the constructor's info table.

Furthermore the type of MkCoercible cannot be written in Haskell
(no syntax for ~#R).

So we define them as regular data types in GHC.Types, and do magic in TysWiredIn,
inside GHC, to change the kind and type.

Правильно ли я понимаю вещи? Или можно написать сигнатуру типа для функции и успешно скомпилировать код? Что бы это ни стоило, вещь, которую я хочу написать, немного проще - 

fcm :: (Monoid m, Coercible m b, Coercible b m, Foldable f) => (a -> b) -> f a -> b
fcm f = coerce . foldMap (coerce . f)

sumBy = fcm @Sum

1 Ответ

0 голосов
/ 15 ноября 2018

Вот что происходит, на более простом примере: 

> :set -XAllowAmbiguousTypes
> import Data.Coerce
> f = coerce . coerce
> :t f
f :: (Coercible a1 c, Coercible a2 a1) => a2 -> c

Пока все хорошо.Все выглядит разумно.Однако, если следующий код не удастся скомпилировать: 

f :: (Coercible a1 c, Coercible a2 a1) => a2 -> c
f = coerce . coerce

• Couldn't match representation of type ‘a0’ with that of ‘c’
    arising from a use of ‘coerce’
  ‘c’ is a rigid type variable bound by
    the type signature for:
      f :: forall a1 c a2. (Coercible a1 c, Coercible a2 a1) => a2 -> c

Почему это происходит?Откуда берется a0?

Проще говоря, в coerce . coerce GHC должен выбрать промежуточный тип, результат первого принуждения.В принципе это может быть что угодно, поэтому GHC генерирует для него свежую переменную типа: выше для этого выбирается a0.

Затем код проверяется на тип и требует ограничений Coercible a0 c, Coercible a2 a0.Те, что указаны в подписи, разные.Здесь GHC НЕ будет пытаться «сопоставить» их и выберет a0 = a1.Действительно, в некоторых контекстах классов типов это может быть неправильным выбором.

Например: (надуманный пример) 

foo :: Read a => String -> ...
foo s = let
   x = read s && True
   in ...

Было бы неправильно использовать ограничение Read a для разрешенияread s.Действительно, для этого нам нужно использовать глобальный экземпляр Read Bool и игнорировать ограничение.Возможно, позже в коде есть еще один вызов read s, в котором нам нужно ограничение, но здесь мы не должны его фиксировать.

Чтобы исправить ваш код, вам нужно явно указать свои приведения, сообщивGHC вы действительно хотите использовать свои ограничения.Например, следующие проверки типов (ScopedTypeVariables on). 

f :: forall a1 a2 c . (Coercible a1 c, Coercible a2 a1) => a2 -> c
f = coerce . (coerce :: a2 -> a1)

Теперь мы сообщаем GHC, что промежуточный тип действительно является нашим a1.

. Вы можете исправить свой код с помощьюдобавление аннотаций аналогичного типа.

...