There is no simple way to forbid "all As" in Haskell.
In dependently typed languages like Agda/Coq, we can put arbitrary constraints using sigma types. This however would require the programmer to write a mathematical proof each time the constructor is used, proving that we are not in fact trying to construct one of the "forbidden" values.
In Haskell, instead, we have no such option. One alternative could be to define a bunch of types.
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
And so on. It's not convenient at all, since we need to use a large number of constructors. Even if the end result is isomorphic to what we want, it's too cumbersome.
It could be improved using some type families, but it still looks rather inconvenient.
Another option could be to also exploit GADTs.
{-# 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)
Finally, a few tests, uncomment one to try.
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
The test below tests elimination (pattern matching). It does not trigger a warning for the impossible case A,A,A: the match is considered to be exhaustive.
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
No warnings as well: A,A is impossible.
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
In a dependently types language, it would not be that easy to perform elimination, since we would need to prove that the match is indeed exhaustive, usually by performing a dependent match on all cases including A,A and then reaching a contradiction. By comparison, here's how elimination would look like in 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.
(There likely is a shorter/simpler Coq solution, but this is the first I could manage to produce.)
