标签: functional-logic-progr

我正在尝试使用 GHC 8.6.5 版在 Haskell 中对以下逻辑含义进行建模：

(∀ 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 …