Data.OpenUnion

This module is inspired by the open union used in the paper
Freer Monads, More Extensible Effects
by Oleg Kiselyov and Hiromi Ishii

By using an AtIndex proof, we are able to get rid of all of
the unsafe coercions in the original module.

Definitions

data UnionT : (a -> Type) -> List a -> Type

  An open union transformer takes
  @ts   a list of type descriptions
  @elt  a method to turn descriptions into types
  and returns a union of the types described in the list.
  Elements are given by an index selecting a value in the list
  together with a value of the appropriately decoded type.

Totality: total
Visibility: public export
Constructor: 

Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> UnionT elt ts

Hint: 

Uninhabited (UnionT elt [])

Union : List Type -> Type

  A union of types is obtained by taking the union transformer
  where the decoding function is the identity.

Totality: total
Visibility: public export

inj : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> UnionT elt ts

  Injecting a value into an open union, provided we know the index of
  the appropriate type family.

Totality: total
Visibility: export

prj : (k : Nat) -> (0 _ : AtIndex t ts k) -> UnionT elt ts -> Maybe (elt t)

  Projecting out of an open union, provided we know the index of the
  appropriate type family. This may obviously fail if the value stored
  actually corresponds to another family.

Totality: total
Visibility: export

split : Subset Nat (flip HasLength ss) -> UnionT elt (ss ++ ts) -> Either (UnionT elt ss) (UnionT elt ts)

  By doing a bit of arithmetic we can figure out whether the union's value
  came from the left or the right list used in the index.

Totality: total
Visibility: public export

decomp : UnionT elt (t :: ts) -> Either (UnionT elt ts) (elt t)

  We can inspect an open union over a non-empty list of families to check
  whether the value it contains belongs either to the first family or any
  other in the tail.

Totality: total
Visibility: public export

decomp0 : UnionT elt [t] -> elt t

  An open union over a singleton list is just a wrapper

Totality: total
Visibility: public export

weakenR : UnionT elt ts -> UnionT elt (ts ++ us)

  Inserting new union members on the right leaves the index unchanged.

Totality: total
Visibility: public export

weakenL : Subset Nat (flip HasLength ss) -> UnionT elt ts -> UnionT elt (ss ++ ts)

  Inserting new union members on the left, requires shifting the index by
  the number of members introduced. Note that this number is the only
  thing we need to keep around at runtime.

Totality: total
Visibility: public export