Choice.gr

------
--- Module: Choice
--- Description: A datatype with two elements. The only way to consume it is by either choosing the first or the second element. You must choose exactly one.
--- Authors: Vilem-Benjamin Liepelt
--- License: BSD3
--- Copyright: (c) Authors 2018
--- Issue-tracking: https://github.com/dorchard/granule/issues
--- Repository: https://github.com/dorchard/granule
------

module Choice hiding (OneOf) where

data Choice a b = OneOf (a [0..1]) (b [0..1]) -- TODO: don't export

choice : forall {a : Type, b : Type} . a [0..1] -> b [0..1] -> Choice a b
choice x y = OneOf x y

-- To construct a `Choice a b`, we need an `a [0..1]` and a `b [0..1]` because
-- the consumer can pick either the `a` or the `b`, not both. (That is currently
-- a lie, we need to be able to make the Choice constructor abstract, i.e. not
-- export it, for this to hold.)
--
-- NB: Polymorphism allows further nonlinearity to be encapsulated inside of the
-- `a` and `b`. In other words, `[0..1]` is just the minimum amount of linearity
-- required. Example:
--
-- ```granule
-- choiceExample : forall a : Type, b : Type
--   . a [0..2] -> b [0..1] -> Choice (a [1..2]) b
-- choiceExample aBox bBox = choice (unflatten aBox) bBox
-- ```

choose1 : forall {a : Type, b : Type} . Choice a b -> a
choose1 (OneOf [x] [_]) = x

choose2 : forall {a : Type, b : Type} . Choice a b -> b
choose2 (OneOf [_] [y]) = y