UnionType was developped with the goal of providing a less verbose alternative
to Sum types. It has similarities with the Haskell
While sum types will lead to stuff like:
record Whiskey where constructor MkWhiskey age: Nat record Beer where constructor MkBeer type: String data StandardAlcohol = AlcoholWhiskey Whiskey | AlcoholBeer Beer
unionType propose the following alternative:
record Whiskey where constructor MkWhiskey age: Nat record Beer where constructor MkBeer type: String Alcohol : Type Alcohol = Union [Whiskey, Beer]
myAlcohol : Alcohol myAlcohol = member $ MkBeer "Lupulus"
And comes with some helpers like the
get function that try to extract value
of a given type:
alcoholAsBeer : Alcohol -> Maybe Beer alcoholAsBeer x = get x
unionType is clumpsy when the same type is at appears several times in the
union. A solution is to use newtypes to differentiate them.