0 | module Data.Fun.Extra
  1 |
  2 | import Data.Fun
  3 | import Data.Rel
  4 | import Data.Vect.Quantifiers
  5 |
  6 | %default total
  7 |
  8 | ||| Apply an n-ary function to an n-ary tuple of inputs
  9 | public export
 10 | uncurry : {0 n : Nat} -> {0 ts : Vect n Type} -> Fun ts cod -> HVect ts -> cod
 11 | uncurry f [] = f
 12 | uncurry f (x::xs) = uncurry (f x) xs
 13 |
 14 | ||| Apply an n-ary function to an n-ary tuple of inputs
 15 | public export
 16 | curry : {n : Nat} -> {0 ts : Vect n Type} -> (HVect ts -> cod) -> Fun ts cod
 17 | curry {ts = []    } f = f []
 18 | curry {ts = _ :: _} f = \x => curry (\xs => f (x :: xs))
 19 |
 20 | {-
 21 |
 22 | The higher kind Type -> Type has a monoid structure given by
 23 | composition and the identity (Cayley). The type (n : Nat ** Vect n a)
 24 | has a monoid structure given by `(n, rs) * (m, ss) := (n + m, rs +
 25 | ss)` and `(0,[])`.
 26 |
 27 |   `Fun' : (n : Nat ** Vect n Type) -> Type -> Type`
 28 |
 29 | is then a monoid homomorphism between them. I guess this is some
 30 | instance of Cayley's theorem, but because of extensionality we can't
 31 | show we have an isomorphism.
 32 | -}
 33 | public export
 34 | homoFunNeut_ext : Fun [] cod -> id cod
 35 | homoFunNeut_ext = id
 36 |
 37 | public export
 38 | homoFunMult_ext : {n : Nat} -> {0 rs : Vect n Type} -> Fun (rs ++ ss) cod -> (Fun rs . Fun ss) cod
 39 | homoFunMult_ext {rs = []  } = id
 40 | homoFunMult_ext {rs = _::_} = (.) homoFunMult_ext
 41 |
 42 | public export
 43 | homoFunNeut_inv : id cod -> Fun [] cod
 44 | homoFunNeut_inv = id
 45 |
 46 | public export
 47 | homoFunMult_inv : {n : Nat} -> {0 rs : Vect n Type} -> (Fun rs . Fun ss) cod -> Fun (rs ++ ss) cod
 48 | homoFunMult_inv {rs = []  } = id
 49 | homoFunMult_inv {rs = _::_} = (.) homoFunMult_inv
 50 |
 51 |
 52 | ||| Apply an n-ary function to an n-ary tuple of inputs
 53 | public export
 54 | applyPartially : {n : Nat} -> {0 ts : Vect n Type}
 55 |                -> Fun (ts ++ ss) cod -> (HVect ts -> Fun ss cod)
 56 | applyPartially = uncurry . homoFunMult_ext
 57 |
 58 |
 59 | {- -------- (slightly) dependent versions of the above ---------------
 60 |    As usual, type dependencies make everything complicated          -}
 61 |
 62 | ||| Apply an n-ary dependent function to its tuple of inputs (given by an HVect)
 63 | public export
 64 | uncurryAll : {0 n : Nat} -> {0 ts : Vect n Type} -> {0 cod : Fun ts Type}
 65 |         -> All ts cod -> (xs : HVect ts) -> uncurry cod xs
 66 | uncurryAll f [] = f
 67 | uncurryAll f (x :: xs) = uncurryAll (f x) xs
 68 |
 69 | public export
 70 | curryAll : {n : Nat} -> {0 ts : Vect n Type} -> {0 cod : Fun ts Type}
 71 |         -> ((xs : HVect ts) -> uncurry cod xs)
 72 |         -> All ts cod
 73 | curryAll {ts = []  } f = f []
 74 | curryAll {ts = _::_} f = \x => curryAll (\xs => f (x :: xs))
 75 |
 76 | chainGenUncurried : {n : Nat} -> {0 ts : Vect n Type} -> {0 cod,cod' : Fun ts Type} ->
 77 |            ((xs : HVect ts) -> uncurry cod xs -> uncurry cod' xs) ->
 78 |            All ts cod -> All ts cod'
 79 | chainGenUncurried {ts = []  } f gs = f [] gs
 80 | chainGenUncurried {ts = _::_} f gs = \x => chainGenUncurried (\u => f (x :: u)) (gs x)
 81 |
 82 | public export
 83 | homoAllNeut_ext : Fun [] cod -> id cod
 84 | homoAllNeut_ext = id
 85 |
 86 | -- Not sure it's worth it getting the rest of Cayley's theorem to work
 87 |
 88 | public export
 89 | extractWitness : {n : Nat} -> {0 ts : Vect n Type} -> {0 r : Rel ts} -> Ex ts r -> HVect ts
 90 | extractWitness {ts = []  }  _       = []
 91 | extractWitness {ts = _::_} (w ** f) = w :: extractWitness f
 92 |
 93 | public export
 94 | extractWitnessCorrect : {n : Nat} -> {0 ts : Vect n Type} -> {0 r : Rel ts} -> (f : Ex ts r) ->
 95 |                         uncurry {ts} r (extractWitness {r} f)
 96 | extractWitnessCorrect {ts = []  } f = f
 97 | extractWitnessCorrect {ts = _::_} (w ** f) = extractWitnessCorrect f
 98 |
 99 | public export
100 | introduceWitness : {0 r : Rel ts} -> (witness : HVect ts) ->
101 |                    uncurry {ts} r witness -> Ex ts r
102 | introduceWitness []             f = f
103 | introduceWitness (w :: witness) f = (w ** introduceWitness witness f)
104 |
105 | ----------------------------------------------------------------------
106 | public export
107 | data Pointwise : (r : a -> b -> Type) -> (ts : Vect n a) -> (ss : Vect n b) -> Type where
108 |   Nil  : Pointwise r [] []
109 |   (::) : {0 ss, ts : Vect n Type} ->
110 |          (f : r t s) -> Pointwise r ts ss -> Pointwise r (t::ts) (s::ss)
111 |
112 | public export
113 | precompose : Pointwise (\a,b => a -> b) ts ss -> Fun ss cod -> Fun ts cod
114 | precompose [] h = h
115 | precompose (f :: fs) h = precompose fs . h . f
116 |
117 | ||| Uncurrying a Fun and then composing with a normal function
118 | ||| is extensionally equal to
119 | ||| composing functions using `chain`, then uncurrying.
120 | public export
121 | chainUncurry :
122 |   {0 ts : Vect n Type}
123 |   -> (g : Fun ts r)
124 |   -> (f : r -> r')
125 |   -> (elems : HVect ts)
126 |   -> f (uncurry g elems)  = uncurry (chain {ts} f g) elems
127 | chainUncurry g f []   =  Refl
128 | chainUncurry g f (x :: xs)  = rewrite chainUncurry (g x) f xs in Refl
129 |