CODEWITHSUNDEEP
haskell
marcosh
marcosh

Reputation: 9008

Model selective usage of sum type

I'm not sure how to model correctly something. Consider a sum type

data Choice
    = A
    | B
    | C

and two types

data Foo = Foo
    { name : String
    , choice : Choice
    }

data Bar = Bar
    { name : String
    , choice : Choice
    }

As it is they are equal. I would like to impose that Foo could use only A and B as Choice, while Bar could use just B and C.

For the moment I solved this splitting Choice in two, like

data ChoiceFoo
    = FooA
    | FooB

data ChoiceBar
    = BarB
    | BarC

but it doesn't look a very scalable approach. Is there a better and/or more elegant solution?

Upvotes: 2

Views: 136

Answers (2)

Li-yao Xia
Li-yao Xia

Reputation: 33569

Modular sums

How about using the generic sum type Either:

data A = A
data B = B
data C = C

type (+) = Either

data Foo = Foo
  { name :: String
  , choice :: A + B
  }

data Bar = Bar
  { name :: String
  , choice = B + C
  }

Modularity is good, but it's not really convenient to have to remember to use the right combination of Left and Right when constructing and pattern-matching values. Furthermore, adding a case requires changing previously existing patterns.

However there are variants of this technique that address this problem. Basically, use a typeclass to select/inject a variant in a sum. See for example Data.Vinyl.CoRec in vinyl, where in particular, the match function makes it possible to pattern-match variants without worrying about order or nesting. In the comments I have a snippet that does something similar with prisms and the total library.

Flat parameterized sum

Another approach, which seems closer to your initial idea, is to declare a single sum type, but with type parameters that can forbid some constructors selectively.

chi already gave an example using GADTs. Here's one with regular ADTs.

data Choice a b c
  = A a
  | B b
  | C c

For there to be no A choice, just set a ~ Void (from Data.Void), which is an empty type.

data Foo = Foo
  { name :: String
  , choice :: Choice () () Void
    -- Two inhabitants: (A ()), (B ())
  }

We must still pattern-match on C to avoid warnings, but the case is systematically dispatched using -XEmptyCase or Data.Void.absurd.

case c :: Choice () () Void of
  A () -> 1
  B () -> 2
  C v -> case v of {}
  -- or  absurd v

This technique also allows some subtyping.

A () :: forall b c. Choice () b c
     :: Choice () () ()
     :: Choice () Void Void
     :: Choice () () Void

The downside is that to support a new (optional) choice means to change the number of type parameters, which is cumbersome.

Upvotes: 1

chi
chi

Reputation: 116174

A possible approach is to use a GADT as follows. It is not that general, though, since a constructor can be associated to either a single type (e.g. ForFoo,ForBar), or to any type (using forAny as a type variable).

data Purpose = ForFoo | ForBar

data Choice (p :: Purpose) where
    A :: Choice 'ForFoo
    B :: Choice forAny  -- can be any Purpose
    C :: Choice 'ForBar

data Foo where
    Foo :: { nameF :: String , choiceF :: Choice 'ForFoo } -> Foo

data Bar where
    Bar :: { nameB :: String , choiceB :: Choice 'ForBar } -> Bar

If we need to express that a choice is for Foo,Bar but not Baz, this approach can not be used.

A more general approach could be:

data Choice2 (a::Bool) (b::Bool) (c::Bool) where
    A2 :: Choice2 'True 'False 'False
    B2 :: Choice2 'False 'True 'False
    C2 :: Choice2 'False 'False 'True

data Foo2 where
    Foo2 :: { nameF2 :: String
            , choiceF2 :: Choice2 b1 b2 'False  } -> Foo2

data Bar2 where
    Bar2 :: { nameB2 :: String
            , choiceB2 :: Choice2 'False b1 b2 } -> Bar2

data Baz2 where
    Baz2 :: { nameZ2 :: String
            , choiceZ2 :: Choice2 b1 'False b2 } -> Baz2

This, in principle, allows one to express any "subset" requirement. We only need to require False in those cases we do not want, and use (existentially quantified) variables for the other cases.

It is still not completely general, and has its shortcomings. For instance, we should be able to write a constant-time implementation for

coerce :: [Choice2 'True b1 b2] -> [Choice2 'True 'False 'False]

but we can not, since we do not really have subtypes.

Upvotes: 3

Related Questions