Могу ли я доказать, что (для x. Coercible (ax) (bx)) подразумевает Coercible ab? - PullRequest
Новая
       17

Могу ли я доказать, что (для x. Coercible (ax) (bx)) подразумевает Coercible ab?

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

Я манипулирую доказательствами принуждения: 

data a ~=~ b where
  IsCoercible :: Coercible a b => a ~=~ b
infix 0 ~=~

sym :: (a ~=~ b) -> (b ~=~ a)
sym IsCoercible = IsCoercible

instance Category (~=~) where 
  id = IsCoercible
  IsCoercible . IsCoercible = IsCoercible

coerceBy :: a ~=~ b -> a -> b
coerceBy IsCoercible = coerce

Я могу доказать тривиально Coercible a b => forall x. Coercible (a x) (b x)

introduce :: (a ~=~ b) -> (forall x. a x ~=~ b x)
introduce IsCoercible = IsCoercible

Но не наоборот, (forall x. Coercible (a x) (b x)) => Coercible a b) не так бесплатен: 

eliminate :: (forall x. a x ~=~ b x) -> (a ~=~ b)
eliminate IsCoercible = IsCoercible
{-
   • Could not deduce: Coercible a b
        arising from a use of ‘IsCoercible’
      from the context: Coercible (a x0) (b x0)
        bound by a pattern with constructor:
                   IsCoercible :: forall k (a :: k) (b :: k).
                                  Coercible a b =>
                                  a ~=~ b,
                 in an equation for ‘eliminate’
-}

Я вполне уверен, что мое утверждение верно (хотя я открыт для опровержения), но у меня нет каких-либо блестящих идей о том, как доказать это в Haskell, если не считать unsafeCoerce.

1 Ответ

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

Нет, вы не можете. Как намекают Доминик Девризе и HTNW в своих комментариях, GHC вообще не допускает такой вывод. Эта более требовательная версия не скомпилируется: 

{-# language QuantifiedConstraints, RankNTypes #-}

import Data.Coerce
import Data.Type.Coercion

eliminate :: (forall a. Coercible (f a) (g a)) => Coercion f g
eliminate = Coercion

Ваша версия еще более обречена. Чтобы сопоставить образец с полиморфным аргументом Coercion (или ~=~), его необходимо создать для конкретного типа. GHC создаст экземпляр для f Any ~=~ g Any, который затем будет мономорфным и, следовательно, не докажет, чего вы хотите. Поскольку GHC Core напечатан, он не будет летать.

Примечание: я очень расстраиваюсь из-за того, что нет возможности написать 

f :: (forall a. c a :- d a)
  -> ((forall a. c a => d a) => r)
  -> r
...