小编Nic*_*che的帖子

考虑以下Haskell代码:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
    FunctionalDependencies #-}

class C a b c | a b -> c

instance C (l (i,j)) (r i j)   j
instance C (l i j)   (r (i,j)) j
-- Conflict between the following two lines
instance C (l (i,j)) (r (i,j)) j  
instance C (l i j)   (r i j)   j

这里,GHC在最后两行之间产生功能依赖性错误.如果我删除最后两个实例声明中的任何一个,代码将编译.我尝试使用类型系列的类比,这也产生了冲突.我的第一个问题是:为什么最后两行冲突,而其他声明一起工作得很好？

另外,如果我将最后一行更改为

instance C (l i j)   (r i j)   i

GHC接受该代码.这似乎很奇怪,因为唯一改变的是依赖类型变量c.有人可以解释这种行为吗？

我正在尝试使用 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 …