Guaranteeing values in types in haskell

user_907981 0
Viewed 61

I have a data type called Interaction which is as follows:

data Interaction = Interaction AgentID AgentID Action Action
  deriving Show

I have a function which is designed to get the Action of the other agent (i.e. not "me") given an interaction:

getCounterAgentAction :: AgentID -> Interaction -> Maybe Action
getCounterAgentAction me (Interaction a b x y)
  | a == me   = Just y
  | b == me   = Just x
  | otherwise = Nothing

But I'd really like to get rid of the Maybe here and enforce that Interaction is an Interaction which contains the given AgentID (I guarantee this at runtime elsewhere in the codebase. Is there a way of doing this?

Some more context (updated)

This code is part of an evolutionary game-theory simulator. Each Interaction encodes how a pair of Agents interacted in a given frame of the simulator (which is basically a time-slice or "round" of the game). In order to calculate the scores, I need to understand how the Agents behaved, and so for each Agent, I check how they interacted with every other Agent. Therefore when I pass an Interaction to this scoring function, I'd like to be able to guarantee that the interactions I am passing have the AgentID I'm checking against in one of the fields. I already know they do at runtime because I'm filtering [Interaction] for those with that AgentID using this function:

findMyInteractions :: AgentID -> [Interaction] -> [Interaction]
findMyInteractions me = filter (\ (Interaction a b _ _) -> (a==me) || (b==me))

It seems to me, therefore, that my use of Maybe could be eliminated here if only I could somehow encode in the types that an Interaction is an Interaction of a given AgentID.

haskell types
1 Answers

The problem here is that Maybe Action is the correct answer to the question "what is the action in the Interaction associated with the AgentID who isn't me?" If you want the answer type to be Action you will have to ask a different question, or you will have to change the Interaction type. The only way to ensure that the answer will be an Action is to guarantee that one of a and b won't equal me. So lets create a type that can't express "a and b both of whom are me", that is, "me and b | a and me | two who aren't me":

data NotBothMe = MeAndA AgentID | MeAndB AgentID | NeitherAreMe AgentID AgentID
data Interaction = Interaction NotBothMe Action Action
getCounterAgentAction :: Interaction -> Action
getCounterAgentAction (Interaction (MeAndA a) x y) = y
getCounterAgentAction (Interaction (MeAndB b) x y) = x
getCounterAgentAction (Interaction (NeitherAreMe a b) x y) = x

Note that the me argument goes away, the me-ness is encoded in the NotBothMe value. Furthermore, the ActionID fields of the NotBothMe type are not used either, we've obtained the information we need to implement getCounterAgentAction in building the NotBothMe value.

Here is a version with the unused AgentID fields removed:

data NotBothMe = MeAndA | MeAndB | NeitherAreMe
data Interaction = Interaction NotBothMe Action Action
getCounterAgentAction :: Interaction -> Action
getCounterAgentAction (Interaction MeAndA x y) = y
getCounterAgentAction (Interaction MeAndB x y) = x
getCounterAgentAction (Interaction NeitherAreMe x _) = x
user_47796360
Related