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

Question

(我很抱歉我不知道如何更好地表达这个问题)
假设我有这样的数据类型:

data Foo = A | B

现在我想要一对 Foo ，约束条件为 (A, A)禁止。
我可以用简单的方式列出它们，如下所示:

data Foo2 = AB | BA | BB

但正如你所看到的，这很快就会失控:如果我们想要 Foo 的 n 元组怎么办？ ?或者如果有更多 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 中没有简单的方法来禁止“所有 A s”。
在像 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 解决方案，但这是我能设法制作的第一个。)