（我很抱歉我不知道如何更好地表達這個問題）
假設我有這樣的資料型別：
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))
但這在某種意義上是“不準確的”，因為當我們 destruct 時Foo2，我們總是必須處理實際上無法到達的情況，而編譯器卻沒有這樣的知識：
...
case v :: Foo2 of
...
Foo2 (A, A) -> error "unreachable"
...
我的問題是，有沒有更好的方法來準確表示“ Foo 的 n 元組，其中某些組合，如(A,A), 或(A,B,C)(when n=3) 是不可能的”？
附帶問題：減法/否定是代數資料型別中的一件事嗎？我認為我需要的基本上是一種與Foo^n - (forbidden combinations)n 元組同構的型別。
uj5u.com熱心網友回復：
A在 Haskell 中沒有簡單的方法來禁止“all 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 解決方案，但這是我能設法制作的第一個。）
uj5u.com熱心網友回復：
以下是我用 GADT 表達它的方式：
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs, TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-} -- for `Show`
import Data.Type.Bool
data Foo = A | B -- see singletons
data TypedFoo x where -- version belowbe
TypedA :: TypedFoo 'A -- for how to avoid
TypedB :: TypedFoo 'B -- boilerplate
deriving instance Show (TypedFoo x) -- / duplication
type family IsA x where
IsA 'A = 'True
IsA 'B = 'False
data Foo2 where
Foo2 :: ((IsA x && IsA y) ~ 'False)
=> TypedFoo x -> TypedFoo y -> Foo2
deriving instance Show Foo2
現在
ghci> Foo2 TypedA TypedB
Foo2 TypedA TypedB
ghci> Foo2 TypedA TypedA
<interactive>:6:1: error:
? Couldn't match type ‘'True’ with ‘'False’
arising from a use of ‘Foo2’
? In the expression: Foo2 TypedA TypedA
In an equation for ‘it’: it = Foo2 TypedA TypedA
并且以下內容不會給出不完整警告：
elim2 :: Foo2 -> Int
elim2 (Foo2 TypedA TypedB) = 0
elim2 (Foo2 TypedB TypedA) = 1
elim2 (Foo2 TypedB TypedB) = 2
使用相同的解決方案的singletons庫：
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs, TypeOperators #-}
{-# LANGUAGE StandaloneDeriving, StandaloneKindSignatures, TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
import Data.Type.Bool
import Data.Singletons.TH
$(singletons [d|
data Foo = A | B
isA :: Foo -> Bool
isA A = True
isA B = False
|])
deriving instance Show Foo
deriving instance Show (SFoo x)
data Foo2 where
Foo2 :: ((IsA x && IsA y) ~ 'False)
=> SFoo x -> SFoo y -> Foo2
deriving instance Show Foo2
我不確定用 Haskell 資料技術對這種約束進行編碼是否真的有用。IMO 一個簡單的智能建構式就可以了，只是不要匯出它，這樣人們也不會遇到不應該存在的案例的問題。相反，試著想想為什么兩個As 的情況沒有意義的更高層次的原因，并相應地設計該型別的公共介面。那么內部表示允許非法組合并不重要。
轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/407297.html
標籤：
下一篇：主執行緒和父執行緒一樣嗎？