Haskell: сочетание экзистенциальных и универсальных квантификаторов неожиданно завершается - PullRequest
Новая
       55

Haskell: сочетание экзистенциальных и универсальных квантификаторов неожиданно завершается

6 голосов
/ 18 января 2020

Я пытаюсь смоделировать следующее логическое значение в Haskell с GH C, версия 8.6.5:

(∀ a. ¬ Φ (a)) → ¬ (∃ a: Φ (a))

Я использовал следующие определения: 

{-# LANGUAGE RankNTypes, GADTs #-}

import Data.Void

-- Existential quantification via GADT
data Ex phi where
  Ex :: forall a phi. phi a -> Ex phi

-- Universal quantification, wrapped into a newtype
newtype All phi = All (forall a. phi a)

-- Negation, as a function to Void
type Not a = a -> Void

-- Negation of a predicate, wrapped into a newtype
newtype NotPred phi a = NP (phi a -> Void)

-- The following definition does not work:
theorem :: All (NotPred phi) -> Not (Ex phi)
theorem (All (NP f)) (Ex a) = f a

Здесь GH C отклоняет реализацию theorem со следующим сообщением об ошибке: 

* Couldn't match type `a' with `a0'
  `a' is a rigid type variable bound by
    a pattern with constructor:
      Ex :: forall a (phi :: * -> *). phi a -> Ex phi,
    in an equation for `theorem'
    at question.hs:20:23-26
* In the first argument of `f', namely `a'
  In the expression: f a
  In an equation for `theorem': theorem (All (NP f)) (Ex a) = f a
* Relevant bindings include
    a :: phi a (bound at question.hs:20:26)
    f :: phi a0 -> Void (bound at question.hs:20:18)

Я не очень понимаю, почему GH C не должен соответствовать двум типам. Компилируется следующий обходной путь: 

theorem = flip theorem' where
    theorem' (Ex a) (All (NP f)) = f a

Для меня две реализации theorem эквивалентны. Почему GH C принимает только второй?

1 Ответ

5 голосов
/ 18 января 2020

Когда вы сопоставляете шаблон All prf со значением типа All phi, prf извлекается как сущность полиморфа c типа forall a. phi a. В этом случае вы получите no :: forall a. NotPred phi a. Однако вы не можете выполнить сопоставление с образцом для объекта этого типа. В конце концов, это функция от типов к значениям. Вам нужно применить его к указанному типу c (назовите его _a), и вы получите no @_a :: NotPred phi _a, который теперь можно сопоставить для извлечения f :: phi _a -> Void. Если вы расширите свое определение ... 

{-# LANGUAGE ScopedTypeVariables #-}
-- type signature with forall needed to bind the variable phi
theorem :: forall phi. All (NotPred phi) -> Not (Ex phi)
theorem prf wit = case prf of
    All no -> case no @_a of -- no :: forall a. NotPred phi a
        NP f -> case wit of -- f :: phi _a -> Void
            Ex (x :: phi b) -> f x -- matching against Ex extracts a type variable, call it b, and then x :: phi b

Итак, вопрос в том, какой тип следует использовать для _a? Итак, мы применяем f :: phi _a -> Void к x :: b (где b - переменная типа, хранящаяся в wit), поэтому мы должны установить _a := b. Но это грубое нарушение. b извлекается только путем сопоставления с Ex, что происходит после того, как мы специализировали no и извлекли f, поэтому тип f не может зависеть от b. Таким образом, не существует выбора _a, который может заставить эту работу работать, не позволяя экзистенциальной переменной покинуть ее область действия. Ошибка.

Решение, как вы обнаружили, состоит в том, чтобы сопоставить с Ex (таким образом извлекая тип из него) перед применением этого типа к no. 

theorem :: forall phi. All (NotPred phi) -> Not (Ex phi)
theorem prf wit = case wit of
    Ex (x :: phi b) -> case prf of
        All no -> case no @b of
            NP f -> f x
-- or
theorem :: forall phi. All (NotPred phi) -> Not (Ex phi)
theorem (All no) (Ex x) | NP f <- no = f x
...