0 | module Data.DPair
  1 |
  2 | import Decidable.Equality
  3 |
  4 | %default total
  5 |
  6 | namespace Pair
  7 |
  8 |   ||| Constructive choice: a function producing pairs of a value and a proof
  9 |   ||| can be split into a function producing a value and a family of proofs
 10 |   ||| for the images of that function.
 11 |   public export
 12 |   choice :
 13 |      {0 p : a -> b -> Type} ->
 14 |      ((x : a) -> (b ** p x b)) ->
 15 |      (f : (a -> b) ** (x : a) -> p x (f x))
 16 |   choice pr = ((\ x => fst (pr x)) ** \ x => snd (pr x))
 17 |
 18 | namespace DPair
 19 |
 20 |   ||| Constructive choice: a function producing pairs of a value and a proof
 21 |   ||| can be split into a function producing a value and a family of proofs
 22 |   ||| for the images of that function.
 23 |   public export
 24 |   choice :
 25 |      {0 b : a -> Type} ->
 26 |      {0 p : (x : a) -> b x -> Type} ->
 27 |      ((x : a) -> (y : b x ** p x y)) ->
 28 |      (f : ((x : a) -> b x) ** (x : a) -> p x (f x))
 29 |   choice pr = ((\ x => fst (pr x)) ** \ x => snd (pr x))
 30 |
 31 |   ||| A function taking a pair of a value and a proof as an argument can be turned
 32 |   ||| into a function taking a value and a proof as two separate arguments.
 33 |   ||| Use `uncurry` to go in the other direction
 34 |   public export
 35 |   curry : {0 p : a -> Type} -> ((x : a ** p x) -> c) -> ((x : a) -> p x -> c)
 36 |   curry f x y = f (x ** y)
 37 |
 38 |   ||| A function taking a value and a proof as two separates arguments can be turned
 39 |   ||| into a function taking a pair of that value and its proof as a single argument.
 40 |   ||| Use `curry` to go in the other direction.
 41 |   public export
 42 |   uncurry : {0 p : a -> Type} -> ((x : a) -> p x -> c) -> ((x : a ** p x) -> c)
 43 |   uncurry f s = f s.fst s.snd
 44 |
 45 |   ||| Given a function on values and a family of proofs that this function takes
 46 |   ||| p-respecting inputs to q-respecting outputs,
 47 |   ||| we can turn:  a pair of a value and a proof it is p-respecting
 48 |   ||| into:         a pair of a value and a proof it is q-respecting
 49 |   public export
 50 |   bimap : {0 p : a -> Type} -> {0 q : b -> Type} ->
 51 |           (f : a -> b) ->
 52 |           (prf : forall x. p x -> q (f x)) ->
 53 |           (x : a ** p x) -> (y : b ** q y)
 54 |   bimap f g (x ** y) = (f x ** g y)
 55 |
 56 |   public export
 57 |   DecEq k => ({x : k} -> Eq (v x)) => Eq (DPair k v) where
 58 |     (k1 ** v1) == (k2 ** v2) = case decEq k1 k2 of
 59 |                                  Yes Refl => v1 == v2
 60 |                                  No _     => False
 61 |
 62 | namespace Exists
 63 |
 64 |   ||| A dependent pair in which the first field (witness) should be
 65 |   ||| erased at runtime.
 66 |   |||
 67 |   ||| We can use `Exists` to construct dependent types in which the
 68 |   ||| type-level value is erased at runtime but used at compile time.
 69 |   ||| This type-level value could represent, for instance, a value
 70 |   ||| required for an intrinsic invariant required as part of the
 71 |   ||| dependent type's representation.
 72 |   |||
 73 |   ||| @type The type of the type-level value in the proof.
 74 |   ||| @this The dependent type that requires an instance of `type`.
 75 |   public export
 76 |   record Exists {0 type : Type} this where
 77 |     constructor Evidence
 78 |     0 fst : type
 79 |     snd : this fst
 80 |
 81 |   public export
 82 |   curry : {0 p : a -> Type} -> (Exists p -> c) -> ({0 x : a} -> p x -> c)
 83 |   curry f = f . Evidence _
 84 |
 85 |   public export
 86 |   uncurry : {0 p : a -> Type} -> ({0 x : a} -> p x -> c) -> Exists p -> c
 87 |   uncurry f ex = f ex.snd
 88 |
 89 |   export
 90 |   evidenceInjectiveFst : Evidence x p = Evidence y q -> x = y
 91 |   evidenceInjectiveFst Refl = Refl
 92 |
 93 |   export
 94 |   evidenceInjectiveSnd : Evidence x p = Evidence x q -> p = q
 95 |   evidenceInjectiveSnd Refl = Refl
 96 |
 97 |   public export
 98 |   bimap : (0 f : a -> b) -> (forall x. p x -> q (f x)) -> Exists {type=a} p -> Exists {type=b} q
 99 |   bimap f g (Evidence x y) = Evidence (f x) (g y)
100 |
101 | namespace Subset
102 |
103 |   ||| A dependent pair in which the second field (evidence) should not
104 |   ||| be required at runtime.
105 |   |||
106 |   ||| We can use `Subset` to provide extrinsic invariants about a
107 |   ||| value and know that these invariants are erased at
108 |   ||| runtime but used at compile time.
109 |   |||
110 |   ||| @type The type-level value's type.
111 |   ||| @pred The dependent type that requires an instance of `type`.
112 |   public export
113 |   record Subset type pred where
114 |     constructor Element
115 |     fst : type
116 |     0 snd : pred fst
117 |
118 |   public export
119 |   curry : {0 p : a -> Type} -> (Subset a p -> c) -> (x : a) -> (0 _ : p x) -> c
120 |   curry f x y = f $ Element x y
121 |
122 |   public export
123 |   uncurry : {0 p : a -> Type} -> ((x : a) -> (0 _ : p x) -> c) -> Subset a p -> c
124 |   uncurry f s = f s.fst s.snd
125 |
126 |   export
127 |   elementInjectiveFst : Element x p = Element y q -> x = y
128 |   elementInjectiveFst Refl = Refl
129 |
130 |   export
131 |   elementInjectiveSnd : Element x p = Element x q -> p = q
132 |   elementInjectiveSnd Refl = Refl
133 |
134 |   public export
135 |   bimap : (f : a -> b) -> (0 _ : forall x. p x -> q (f x)) -> Subset a p -> Subset b q
136 |   bimap f g (Element x y) = Element (f x) (g y)
137 |
138 |   public export
139 |   Eq type => Eq (Subset type pred) where
140 |     (==) = (==) `on` fst
141 |
142 |   public export
143 |   Ord type => Ord (Subset type pred) where
144 |     compare = compare `on` fst
145 |
146 |   ||| This Show implementation replaces the (erased) invariant
147 |   ||| with an underscore.
148 |   export
149 |   Show type => Show (Subset type pred) where
150 |     showPrec p (Element v _) = showCon p "Element" $ showArg v ++ " _"
151 |