How can I restrict types based on input values in Haskell?

Question

I'm new to Haskell. Sorry if this question has an obvious answer.

I have

data Tmp = Foo Int
         | Bar Int
         | Baz Int

and

data Test = A Tmp Tmp

The constructor A Tmp Tmp can take any constructor for Tmp except for A (Baz i) (Baz j) where i and j are arbitrary Ints. Is there any way I can restrict the second Tmp in A Tmp Tmp from being Baz if the first Tmp is already Baz?

Answer 1

The answer depends on how you want your restriction to be enforced: At runtime or at compile time.

To enforce the restriction at runtime, you can add a function (say, makeA) that checks the restriction and then calls the constructor. Such a function that does a bit of stuff and then calls a constructor is also called a smart constructor. If you only export the smart constructor makeA but not the real constructor A from a module, you can be sure that other modules use the smart constructor, so the restriction is always checked.

Example:

module Test (Tmp (Foo, Bar, Baz), Test (), makeA) where
  data Tmp
     = Foo Int
     | Bar Int
     | Baz Int

  data Test = A Tmp Tmp

  makeA :: Tmp -> Tmp -> Tmp
  makeA (Baz _) (Baz _) = error "makeA: two baz problem"
  makeA tmp1 tmp2 = A tmp1 tmp2

The benefit of this technique is that you don't have to change your data types at all. The drawback is that the restriction is only enforced at run time.

To enforce the restriction at compile time, you need to change your data types somehow. The problem with your current data types is that the type checker cannot distinguish values constructed by Foo and Bar and values constructed by Baz. To the type checker, these are all Tmp values, so the type checker cannot enforce that some Tmp values are ok and others aren't. So we have to change the data types to encode "Bazness" of a Tmp value in the types.

One option for encoding the Bazness in the type would be to restructure Tmp as follows:

data TmpNotBaz
  = Foo Int
  | Bar Int

data Tmp
  = NotBaz TmpNotBaz
  | Baz Int

Now it is clear that a value of type TmpNotBaz cannot be Baz, but a value of type Tmp can be Baz. The benefit of this idea is that it only uses basic Haskell features. A minor drawback is that you need to put calls to NotBaz into your code. A major drawback is that we still cannot directly express the idea of "one of the arguments of A can be Baz if the other isn't". We would have to write multiple versions of A:

data Test
  = A1 TmpNotBaz Tmp
  | A2 Tmp TmpNotBaz

Now we can express all the values we want by choosing A1 or A2 as necessary, and we cannot express A (Baz ...) (Baz ...) anymore, as required. A problem with this solution is that there are multiple representations for what used to be, for example, A (Foo 1) (Foo 2) : Both A1 (Foo 1) (NotBaz (Foo 2)) and A2 (NotBaz (Foo 1)) (Foo 2) represent this value.

You can try to play around with the structure of the datatypes like this and create a version that works for your situation.

Another option for encoding the Bazness in the type would be to annotate a bit of type-level information to the Tmp type and use type-level programming to reason about this type-level information. The drawback of this idea is that it uses more advanced Haskell features. Actually, there are many emerging ways to do this sort thing, and it is not clear which of these will end up being considered "standard" advanced Haskell. That said, here is one approach:

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

data Bazness = IsBaz | NotBaz

data BothBazOrNot = BothBaz | NotBothBaz

type family AreBothBaz (b1 :: Bazness) (b2 :: Bazness) :: BothBazOrNot where
  AreBothBaz 'IsBaz 'IsBaz = 'BothBaz
  AreBothBaz _ _ = 'NotBothBaz

data Tmp (b :: Bazness) :: * where
  Foo :: Int -> Tmp 'NotBaz
  Bar :: Int -> Tmp 'NotBaz
  Baz :: Int -> Tmp 'IsBaz

data Test where
  A :: AreBothBaz b1 b2 ~ 'NotBothBaz => Tmp b1 -> Tmp b2 -> Test

Note how the type signatures of the constructors Foo, Bar and Baz talk about whether the constructor creates something that IsBaz or NotBaz. And how the type signature for A talks about some b1 and b2 choices so that NotBothBaz.

Using this code, we can write the following expressions:

• A (Foo 1) (Bar 2)
• A (Foo 1) (Baz 2)
• A (Baz 1) (Bar 2)

But if we try to write A (Baz 1) (Baz 2), the type checker complains:

Couldn't match type 'BothBaz with 'NotBothBaz
    arising from a use of A
 In the expression: A (Baz 1) (Baz 2)

So the type checker figured out that in this case, the arguments to A are BothBaz, but we annotated the type of A to only accept arguments that are NotBothBaz, so the type checker complains that BothBaz differs from NotBothBaz.