Haskell 中是否有一种准确的方法来编码 Foo 的元组，其中某些组合是被禁止的？

Question

（提前抱歉，我不知道如何更好地表达这个问题）

假设我有这样的数据类型：

data Foo = A | B

现在我想要一对Foo，带有禁止的约束(A, A)。

我可以采用简单的方法，将它们全部列出来，如下所示：

data Foo2 = AB | BA | BB

但正如你所看到的，这很快就会失控：如果我们想要 n 元组怎么办Foo？或者如果有更多的选择怎么办Foo？

当然，另一种选择是使用newtype智能构造函数

newtype Foo2 = Foo2 (Foo, Foo)

mkFoo2 xy = Foo2 xy <$ guard (xy /= (A,A))

但这在某种意义上是“不准确的”，因为当我们析构时Foo2，我们总是必须处理实际上无法访问的情况，但编译器没有这样的知识：

...
case v :: Foo2 of
  ...
  Foo2 (A, A) -> error "unreachable"
...
      

我的问题是，是否有更好的方法来准确表示“Foo 的 n 元组，其中某些组合，例如(A,A)或(A,B,C)（当n=3）不可能”的想法？

附带问题：减法/求反是代数数据类型中的一件事吗？Foo^n - (forbidden combinations)我认为我需要的基本上是一个与 n 元组同构的类型。

Answer 1

在 Haskell 中没有简单的方法来禁止“all As”。

在像 Agda/Coq 这样的依赖类型语言中，我们可以使用 sigma 类型设置任意约束。然而，这需要程序员在每次使用构造函数时编写数学证明，证明我们实际上并没有尝试构造“禁止”值之一。

相反，在 Haskell 中，我们没有这样的选择。一种替代方法是定义一堆类型。

data NotA = B | C
data Any  = A | NA NotA

-- 1-tuple, not all As
data NotAllAs1 
  = N1 NotA
-- 2-tuple, not all As
data NotAllAs2 
  = N2 NotA Any
  | N2a NotAllAs1          -- first A implicit
-- 3-tuple, not all As
data NotAllAs3
  = N3 NotA (Any, Any)
  | N3a NotAllAs1          -- first A implicit

等等。这一点也不方便，因为我们需要使用大量的构造函数。即使最终结果与我们想要的同构，也太麻烦了。

使用某些类型族可以改进它，但看起来仍然很不方便。

另一种选择是也利用 GADT。

{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}

-- We define some tags for being A and not A
data IsA = IsA | NotA

-- Type T is indexed with the proper tag
data T (a :: IsA) where
   A :: T 'IsA
   B :: T 'NotA
   C :: T 'NotA

-- We want "at least one non-A" so we define an "or"
-- operation between two tags.
type family Or (a1 :: IsA) (a2 :: IsA) :: IsA where
   Or 'IsA a2 = a2
   Or 'NotA _ = 'NotA

-- Peano naturals to encode tuple length
data Nat = Z | S Nat

-- The wanted tuple type
type NotAllAs (n :: Nat) = NA n 'NotA

-- NA n t is the type for an n-tuple having either all As
-- (if t ~ IsA) or some non-A (if t ~ NotA)
data NA (n :: Nat) (t :: IsA) where
   Nil  :: NA 'Z 'IsA
   Cons :: T a1 -> NA n a2 -> NA ('S n) (Or a1 a2)

最后，进行一些测试，取消注释一项来尝试。

test :: NotAllAs ('S ('S ('S 'Z)))
test = 
   -- Cons A (Cons A (Cons A Nil))      -- Couldn't match type 'IsA with 'NotA
   -- Cons A (Cons A (Cons B Nil))      -- OK
   -- Cons A (Cons B (Cons A Nil))      -- OK
   -- Cons B (Cons A (Cons A Nil))      -- OK

下面的测试测试消除（模式匹配）。它不会触发不可能情况的警告A,A,A：匹配被认为是详尽的。

elim :: NotAllAs ('S ('S ('S 'Z))) -> Int
elim (Cons A (Cons A (Cons B Nil))) = 1
elim (Cons A (Cons A (Cons C Nil))) = 2
elim (Cons A (Cons B _           )) = 3
elim (Cons A (Cons C _           )) = 4
elim (Cons B _                    ) = 5
elim (Cons C _                    ) = 6

也没有警告：A,A这是不可能的。

elim2 :: NotAllAs ('S ('S 'Z)) -> Int
elim2 (Cons x (Cons A Nil)) = case x of B -> 1 ; C -> 2
elim2 (Cons _ (Cons B Nil)) = 3
elim2 (Cons _ (Cons C Nil)) = 4

在依赖类型语言中，执行消除并不那么容易，因为我们需要证明匹配确实是详尽的，通常是通过对所有情况执行依赖匹配，包括然后A,A 达到矛盾。相比之下，Coq 中的消除方式如下：

Inductive T: Set := A | B | C .

(* The constraint is trivial to specify. *)
Definition NotAllA2 := { p: T*T | p <> (A,A) } .

(* We will need this trivial lemma later *)
Lemma lem: forall x, (x,A) <> (A,A) -> x<>A .
Proof.
intros x h h2.
subst.
apply h.
reflexivity.
Qed.

Definition elim2 (v: NotAllA2): nat :=
   match v with
   | exist _ p h => (* h is the proof that our constraint holds *)
      match p return p<>(A,A) -> nat with
      | (x,A) => fun h2: (x,A)<>(A,A) => 
        match x return x<>A -> nat with
          (* We need to prove that A is impossible here *)
        | A => fun h3 => match h3 eq_refl with end
        | B => fun _ => 1
        | C => fun _ => 2
        end (lem x h2)
      | (_,B) => fun _ => 3
      | (_,C) => fun _ => 4
      end h
   end.

（可能有一个更短/更简单的 Coq 解决方案，但这是我能设法制作的第一个解决方案。）