A way to generalize Haskell's Either type for arbitrarily many types?

Question

I am creating a turn based game. I want to define a datatype that encodes one type out of many possible types. Here is the motivating example:

I have defined a Turn type using GADTs, so the type of each value of Turn a says something about it's value.

data Travel
data Attack
data Flee
data Quit

data Turn a where
   Travel :: Location -> Turn Travel
   Attack :: Int -> Turn Attack
   Flee :: Turn Flee
   Quit :: Turn Quit

Now I can write types like this decideTravel :: GameState -> Turn Travel, very expressive and nice.

The problem arises when I want to return one of multiple possible turn types. I want to write functions similar to the following:

-- OneOf taking two types
decideFightingTurn :: GameState -> OneOf (Turn Attack) (Turn Flee)
-- OneOf takes three types
decideTurn :: GameState -> OneOf (Turn Attack) (Turn Travel) (Turn Quit)

Where this OneOf datatype carries the notion of "one type out of many possible types". The problem lies in defining this datatype, I need to somehow handle a list of types at the type level.

There are two subpar solutions I have as of now:

Solution 1: Create a wrapper sum type

Simply create a new type that has a constructor for each Turn a constructor:

data AnyTurn
   = TravelTurn (Turn Travel)
   | TravelAttack (Turn Attack)
   | TravelFlee (Turn Flee)
   | TravelQuit (Turn Quit)

This doesn't help me in the way I want it to. Now I have to pattern match all cases of AnyTurn and account for invalid input types. Additionally the type level information is obscured by the AnyTurn type, since it fails to indicate which specific turns are actually possible at the type level.

Solution 2: Create "Either" types for different numbers of types

This solution gives me what I want at the type level, but is cumbersome to use. Basically create an Either-like type for any number of combinations, like so:

data OneOf2 a b
   = OneOf2A a
   | OneOf2B b

data OneOf3 a b c
   = OneOf3A a
   | OneOf3B b
   | OneOf3C c

-- etc, for as many as are needed.

This conveys what I want at the type level, so I can now write the previous examples as:

decideFightingTurn :: GameState -> OneOf2 (Turn Travel) (Turn Flee)
decideTurn :: GameState -> OneOf3 (Turn Attack) (Turn Travel) (Turn Quit)

This works, however it would be nice to express this with just one type OneOf. Is there any way to write the generalized OneOf type in Haskell?

Lodestone

Answer 1

Something like this, I guess:

data OneOf as where
    ThisOne :: a -> OneOf (a : as)
    Later :: OneOf as -> OneOf (a : as)

Then you can write, for example:

decideFightingTurn :: GameState -> OneOf [Turn Travel, Turn Flee]

You might also like to:

type family Map f xs where
    Map f '[] = '[]
    Map f (x:xs) = f x : Map f xs

This way you can write something like:

decideFightingTurn :: GameState -> OneOf (Map Turn [Travel, Flee])

Or you could build the Map into the GADT if you think you'll always be doing it:

data OneOfF f as where
    ThisOneF :: f a -> OneOfF f (a : as)
    LaterF :: OneOfF f as -> OneOfF f (a : as)

And then:

decideFightingTurn :: GameState -> OneOfF Turn [Travel, Flee]

Various things can be done to make this more efficient if that becomes a concern; the first thing I'd try would be using binary indexing rather than unary as shown here.

Sprinkler

Answer 2

There's a Haskell library called row-types that might give you what you want. Specifically, it provides an extensible variant that is kind of like Either but tagged and with arbitrarily many options.

In your case, you could make your types:

import Data.Row

decideFightingTurn :: GameState -> Var ("travel" .== Turn Travel .+ "flee" .== Turn Flee)
decideTurn :: GameState -> Var ("attack" .== Turn Attack .+ "travel" .== Turn Travel .+ "quit" .== Turn Quit)

The easiest way to work with variants is to turn OverloadedLabels on. Then, to create one, you write:

decideFightingTurn gs = case gs of
  Foo -> IsJust #travel $ Travel loc
  Bar -> IsJust #flee Flee

Deconstructing can be done in a few different ways. If you just want to check for a particular type, you can use trial or view (exported by Data.Row.Variants), but if you want to deal with all the options at once, you may want to use switch. You'd write something like this:

handleTravelOrFlee :: Var ("travel" .== Turn Travel .+ "flee" .== Turn Flee) -> GameState -> GameState
handleTravelOrFlee v gs = switch v $
     #travel .== (\(Travel loc) -> updateGameStateWithLoc gs loc)
  .+ #flee   .== (\Flee -> updateGameStateFlee gs)

Check out the documentation and the examples file for more info.

Penknife

Answer 3

Another option could be activating and deactivating constructors in the sum type:

{-# LANGUAGE GADTs, TypeOperators, DataKinds, PolyKinds, 
             TypeFamilies, StandaloneKindSignatures #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns -Werror=overlapping-patterns #-}
import Data.Void
import Data.Kind

data TurnType =
      Travel
    | Attack
    | Flee
    | Quit

type Turn :: TurnType -> Type
data Turn tt  where
   TurnTravel :: Location -> Turn Travel
   TurnAttack :: Int -> Turn Attack
   TurnFlee :: Turn Flee
   TurnQuit :: Turn Quit

type X :: TurnType -> [TurnType] -> Type
type family X x tts :: Type where
    X _ '[] = Void 
    X x (x : xs) = ()
    X x (_ : xs) = X x xs

-- Exhaustiveness checker knows that branches where
-- X returns Void are impossible.
type AnyTurn :: [TurnType] -> Type
data AnyTurn allowed
   = TravelTurn !(X Travel allowed) (Turn Travel)
   | TravelAttack !(X Attack allowed) (Turn Attack)
   | TravelFlee  !(X Flee allowed) (Turn Flee)
   | TravelQuit  !(X Quit allowed) (Turn Quit)

Putting it to work:

someTurn :: AnyTurn '[Travel, Attack]
someTurn = TravelAttack () (TurnAttack 0)

-- This doesn't give an exhaustiveness error because other branches are impossible.
-- The problem is that we now have those annoying () cluttering every match.
turn2string :: AnyTurn '[Travel, Attack] -> String
turn2string t = case t of
   TravelTurn () _ -> "foo" 
   TravelAttack () _ -> "bar"
   -- TravelQuit _ _ -> "doesn't compile"

Cystitis

I like it. You can eliminate the ()s by making it a constraint. For example, type family Elem x xs where Elem x [] = False; Elem x (x:xs) = True; Elem x (_:xs) = Elem x xs and then data AnyTurn allowed where AnyTurn :: Elem x allowed ~ True => Turn x -> AnyTurn. – Sprinkler