Можно ли написать псевдоним для принуждения?

Question

Допустим, для целей этого вопроса я хочу создать псевдоним coerce. Я начинаю с очевидного

import Data.Coerce

q = coerce

немного удивительно, это вызывает ошибку:

coerce.hs:3:5: error:
    • Couldn't match representation of type ‘a0’ with that of ‘b0’
        arising from a use of ‘coerce’
    • In the expression: coerce
      In an equation for ‘q’: q = coerce
    • Relevant bindings include q :: a0 -> b0 (bound at coerce.hs:4:1)
  |
4 | q = coerce
  |     ^^^^^^

Эта ошибка довольно непрозрачна, поэтому я ввел подпись типа ¹ из coerce на q:

{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Coerce
import GHC.Exts

q :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b
q = coerce

Но это вызывает ошибку:

coerce.hs:8:5: error:
    Cannot use function with levity-polymorphic arguments:
      coerce :: a -> b
    Levity-polymorphic arguments: a :: TYPE k
  |
8 | q = coerce
  |     ^^^^^^

Эта ошибка не очень полезна. Он сообщает мне, что существует проблема с полиморфизмом левитации, и это все.

Что действительно очень любопытно, так это то, что когда я делаю q bottom: уходит, и код компилируется нормально.

Я не уверен, возможен ли такой псевдоним, и в чем вообще проблема с псевдонимом.

Возможен ли такой псевдоним, где q поддерживает тип coerce? С какой проблемой компилятор работает с моим кодом?

^{1: Как указано в комментариях, эта сигнатура типа имеет только левитационный полиморфизм, начиная с base-4.13 или gh c 8.8. Для целей этого вопроса нам нужен полиморфизм легкомыслия.}

Answer 1

Ответ

@ dfeuer охватывает обходной путь, но я думаю, что issue # 17670 объясняет , почему это происходит. Поскольку coerce является примопом, он должен быть полностью насыщен, поэтому любое использование неявно расширяется с помощью eta. Когда вы пишете:

q = coerce

, вы действительно пишете:

q = \x -> coerce x

Первоначальное сообщение об ошибке, которое вы получаете, на самом деле является результатом ограничения мономорфизма. Если вы напишете либо:

q x = coerce x

, либо добавите расширение NoMonomorphismRestriction, программа будет принята. К сожалению, полученный q не является полиморфом легкомыслия c. Он создается с поднятыми типами.

Если попытаться вызвать проблему, добавив соответствующий полиморф c сигнатуру типа:

q :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k). Coercible a b => a -> b
q = coerce

, то последующие версии GH C (например, "8.11", созданный из исходного кода в прошлом месяце) дает подробное сообщение об ошибке:

BadCoerce.hs:11:5: error:
    Cannot use function with levity-polymorphic arguments:
      coerce :: a -> b
    (Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
    are eta-expanded internally because they must occur fully saturated.
    Use -fprint-typechecker-elaboration to display the full expression.)
    Levity-polymorphic arguments: a :: TYPE k

В конечном итоге вы сталкиваетесь с запретом, что никакая переменная (в данном случае неявная переменная, введенная в eta-expand coerce) разрешено быть levity polymorphi c. Причина, по которой q = q работает, заключается в том, что нет расширения eta и, следовательно, нет переменной. Попробуйте q x = q x, и он завершится ошибкой с сообщением об ошибке «тип levity-polymorphi c здесь не разрешен».

Answer 2

Не похоже, что это возможно, но вы можете подойти очень близко. Примечание: вполне возможно, это можно будет сократить.

blop
  :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k) q r.
     Coercible a b
  => q :~: (a -> a)
  -> r :~: (a -> b)
  -> Coercion q r
blop Refl Refl = Coercion

bloverce
  :: forall (k :: RuntimeRep) (a :: TYPE k) (b :: TYPE k) q r.
     Coercible a b
  => q :~: (a -> a)
  -> r :~: (a -> b)
  -> q -> r
bloverce qaa rab = case blop qaa rab of Coercion -> coerce

gloerce
  :: forall (r :: RuntimeRep).
     (forall (x :: TYPE r). x -> x) -> Coe r
gloerce kid = Coe (bloverce Refl Refl (kid :: a -> a) :: forall (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b)

newtype Coe (r :: RuntimeRep) = Coe (forall (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b)

Пока вы можете предоставить функцию идентификации polymorphi c для определенного представления среды выполнения, вы можете использовать gloerce, чтобы получить ее coerce.

Конечно, на практике все это довольно глупо: в тех редких случаях, когда вам нужна функция принуждения c полиморфного представления, вы можете просто использовать coerce напрямую.