0 | ||| This module is inspired by the open union used in the paper
 1 | ||| Freer Monads, More Extensible Effects
 2 | ||| by Oleg Kiselyov and Hiromi Ishii
 3 | |||
 4 | ||| By using an AtIndex proof, we are able to get rid of all of
 5 | ||| the unsafe coercions in the original module.
 6 |
 7 | module Data.OpenUnion
 8 |
 9 | import Data.DPair
10 | import Data.List.AtIndex
11 | import Data.List.HasLength
12 | import Data.Nat
13 | import Data.Nat.Order.Properties
14 | import Decidable.Equality
15 | import Syntax.WithProof
16 |
17 | %default total
18 |
19 | ||| An open union transformer takes
20 | ||| @ts   a list of type descriptions
21 | ||| @elt  a method to turn descriptions into types
22 | ||| and returns a union of the types described in the list.
23 | ||| Elements are given by an index selecting a value in the list
24 | ||| together with a value of the appropriately decoded type.
25 | public export
26 | data UnionT : (elt : a -> Type) -> (ts : List a) -> Type where
27 |   Element : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> UnionT elt ts
28 |
29 | ||| A union of types is obtained by taking the union transformer
30 | ||| where the decoding function is the identity.
31 | public export
32 | Union : List Type -> Type
33 | Union = UnionT Prelude.id
34 |
35 | ||| An empty open union of families is empty
36 | public export
37 | Uninhabited (UnionT elt []) where
38 |   uninhabited (Element _ p _) = void (uninhabited p)
39 |
40 | ||| Injecting a value into an open union, provided we know the index of
41 | ||| the appropriate type family.
42 | export
43 | inj : (k : Nat) -> (0 _ : AtIndex t ts k) -> elt t -> UnionT elt ts
44 | inj = Element
45 |
46 | ||| Projecting out of an open union, provided we know the index of the
47 | ||| appropriate type family. This may obviously fail if the value stored
48 | ||| actually corresponds to another family.
49 | export
50 | prj : (k : Nat) -> (0 _ : AtIndex t ts k) -> UnionT elt ts -> Maybe (elt t)
51 | prj k p (Element k' q t) with (decEq k  k')
52 |   prj k p (Element k q t) | Yes Refl = rewrite atIndexUnique p q in Just t
53 |   prj k p (Element k' q t) | No neq = Nothing
54 |
55 | ||| By doing a bit of arithmetic we can figure out whether the union's value
56 | ||| came from the left or the right list used in the index.
57 | public export
58 | split : Subset Nat (flip HasLength ss) ->
59 |         UnionT elt (ss ++ ts) -> Either (UnionT elt ss) (UnionT elt ts)
60 | split m (Element n p t) with (@@ lt n (fst m))
61 |   split m (Element n p t) | (True ** lt)
62 |     = Left (Element n (strengthenL m lt p) t)
63 |   split m (Element n p t) | (False ** notlt)
64 |     = let 0 lte : lte (fst m) n === True
65 |                 = LteIslte (fst m) n (notltIsGTE n (fst m) notlt)
66 |       in Right (Element (minus n (fst m)) (strengthenR m lte p) t)
67 |
68 | ||| We can inspect an open union over a non-empty list of families to check
69 | ||| whether the value it contains belongs either to the first family or any
70 | ||| other in the tail.
71 | public export
72 | decomp : UnionT elt (t :: ts) -> Either (UnionT elt ts) (elt t)
73 | decomp (Element 0     (Z)   t) = Right t
74 | decomp (Element (S n) (S p) t) = Left (Element n p t)
75 |
76 | ||| An open union over a singleton list is just a wrapper
77 | public export
78 | decomp0 : UnionT elt [t] -> elt t
79 | decomp0 elt = case decomp elt of
80 |   Left t => absurd t
81 |   Right t => t
82 |
83 | ||| Inserting new union members on the right leaves the index unchanged.
84 | public export
85 | weakenR : UnionT elt ts -> UnionT elt (ts ++ us)
86 | weakenR (Element n p t) = Element n (weakenR p) t
87 |
88 | ||| Inserting new union members on the left, requires shifting the index by
89 | ||| the number of members introduced. Note that this number is the only
90 | ||| thing we need to keep around at runtime.
91 | public export
92 | weakenL : Subset Nat (flip HasLength ss) -> UnionT elt ts -> UnionT elt (ss ++ ts)
93 | weakenL m (Element n p t) = Element (fst m + n) (weakenL m p) t
94 |