0 | ||| The telescope data structures.
  1 | |||
  2 | ||| Indexing telescopes by their length (hopefully) helps inform the
  3 | ||| type-checker during inference.
  4 | module Data.Telescope.Telescope
  5 |
  6 | import Data.DPair
  7 | import Data.Nat
  8 | import Data.Fin
  9 |
 10 | %default total
 11 |
 12 | public export
 13 | plusAcc : Nat -> Nat -> Nat
 14 | plusAcc Z n = n
 15 | plusAcc (S m) n = plusAcc m (S n)
 16 |
 17 | export
 18 | plusAccIsPlus : (m, n : Nat) -> (m + n) === plusAcc m n
 19 | plusAccIsPlus Z n = Refl
 20 | plusAccIsPlus (S m) n =
 21 |   rewrite plusSuccRightSucc m n in
 22 |   plusAccIsPlus m (S n)
 23 |
 24 | public export
 25 | plusAccZeroRightNeutral : (m : Nat) -> plusAcc m 0 === m
 26 | plusAccZeroRightNeutral m =
 27 |   rewrite sym (plusAccIsPlus m 0) in
 28 |   rewrite plusZeroRightNeutral m in
 29 |   Refl
 30 |
 31 |
 32 | export infixl 4 -.
 33 | export infixr 4 .-
 34 |
 35 | namespace Left
 36 |
 37 |   mutual
 38 |     ||| A left-nested sequence of dependent types
 39 |     public export
 40 |     data Telescope : (k : Nat) -> Type where
 41 |       Nil  : Telescope 0
 42 |       (-.) : (gamma : Left.Telescope k) -> (ty : TypeIn gamma) -> Telescope (S k)
 43 |
 44 |     ||| A type with dependencies in the given context
 45 |     public export
 46 |     TypeIn : Left.Telescope k -> Type
 47 |     TypeIn gamma = (env : Environment gamma) -> Type
 48 |
 49 |     ||| A tuple of values of each type in the telescope
 50 |     public export
 51 |     Environment : Left.Telescope k -> Type
 52 |     Environment [] = ()
 53 |     Environment (gamma -. ty) = (env : Environment gamma ** ty env)
 54 |
 55 |   export
 56 |   weakenTypeIn : TypeIn gamma -> TypeIn (gamma -. sigma)
 57 |   weakenTypeIn ty env = ty (fst env)
 58 |
 59 |   public export
 60 |   uncons : (gamma : Telescope (S k)) ->
 61 |            (ty : Type
 62 |             ** delta : (ty -> Telescope k)
 63 |             ** (v : ty) -> Environment (delta v) -> Environment gamma)
 64 |   uncons ([] -. ty) = (ty () ** const [] ** \ v, _ => (() ** v))
 65 |   uncons (gamma@(_ -. _) -. ty) =
 66 |     let (sigma ** delta ** left) = uncons gamma in
 67 |     (sigma ** (\ v => delta v -. (\ env => ty (left v env)))
 68 |            ** (\ v, (env ** w) => (left v env ** w)))
 69 |
 70 |   public export
 71 |   (++) : {n : Nat} -> (gamma : Left.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
 72 |          Telescope (plusAcc n m)
 73 |   (++) {n = Z} gamma delta = gamma
 74 |   (++) {n = S n} gamma delta = (gamma -. sigma) ++ uncurry theta where
 75 |
 76 |     sigma : Environment gamma -> Type
 77 |     sigma env = fst (uncons (delta env))
 78 |
 79 |     theta : (env : Environment gamma) -> sigma env -> Telescope n
 80 |     theta env val with (uncons (delta env))
 81 |       theta env val | (sig ** omega ** _) = omega val
 82 |
 83 |   public export
 84 |   cons : {k : Nat} -> (ty : Type) -> (ty -> Left.Telescope k) -> Left.Telescope (S k)
 85 |   cons sigma gamma =
 86 |     rewrite plusCommutative 1 k in
 87 |     rewrite plusAccIsPlus k 1 in
 88 |     ([] -. const sigma) ++ (gamma . snd)
 89 |
 90 |   ||| A position between the variables of a telescope, counting from the _end_:
 91 |   ||| Telescope:   Nil -. ty1 -. ... -. tyn
 92 |   ||| Positions: ^k    ^k-1   ^k-2   ^1     ^0
 93 |   public export
 94 |   Position : {k : Nat} -> Telescope k -> Type
 95 |   Position {k} _ = Fin (S k)
 96 |
 97 |   ||| The position at the beginning of the telescope
 98 |   public export
 99 |   start : {k : Nat} -> (gamma : Telescope k) -> Position gamma
100 |   start {k} gamma = last
101 |
102 | namespace Right
103 |
104 |   mutual
105 |     ||| A right-nested sequence of dependent types
106 |     public export
107 |     data Telescope : (k : Nat) -> Type where
108 |       Nil  : Telescope 0
109 |       (.-) : (ty : Type) -> (gamma : ty -> Right.Telescope k) -> Telescope (S k)
110 |
111 |     ||| A tuple of values of each type in the telescope
112 |     public export
113 |     Environment : Right.Telescope k -> Type
114 |     Environment [] = ()
115 |     Environment (ty .- gamma) = (v : ty ** Environment (gamma v))
116 |
117 |   export
118 |   empty : (0 gamma : Right.Telescope Z) -> Environment gamma
119 |   empty {gamma = []} = ()
120 |
121 |   export
122 |   snoc : (gamma : Right.Telescope k) -> (Environment gamma -> Type) -> Right.Telescope (S k)
123 |   snoc [] tau   = tau () .- const []
124 |   snoc (sigma .- gamma) tau = sigma .- \ v => snoc (gamma v) (\ env => tau (v ** env))
125 |
126 |   export
127 |   unsnoc : {k : Nat} -> (gamma : Right.Telescope (S k)) ->
128 |            (delta : Right.Telescope k
129 |             ** sigma : (Environment delta -> Type)
130 |             ** (env : Environment delta) -> sigma env -> Environment gamma)
131 |   unsnoc {k = Z} (sigma .- gamma) = ([] ** const sigma ** \ (), v => (v ** empty (gamma v)))
132 |   unsnoc {k = S k} (sigma .- gamma)
133 |     = (sigma .- delta ** uncurry tau ** \ (v ** env) => transp v env) where
134 |
135 |     delta : sigma -> Right.Telescope k
136 |     delta v = fst (unsnoc (gamma v))
137 |
138 |     tau : (v : sigma) -> Environment (delta v) -> Type
139 |     tau v = fst (snd (unsnoc (gamma v)))
140 |
141 |     transp : (v : sigma) -> (env : Environment (delta v)) -> tau v env -> Environment (sigma .- gamma)
142 |     transp v env w = (v ** (snd (snd (unsnoc (gamma v))) env w))
143 |
144 |   export
145 |   (++) : (gamma : Right.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (m + n)
146 |   [] ++ delta = delta ()
147 |   (sigma .- gamma) ++ delta = sigma .- (\ v => (gamma v ++ (\ env => delta (v ** env))))
148 |
149 |   export
150 |   split : (gamma : Right.Telescope m) -> (delta : Environment gamma -> Right.Telescope n) ->
151 |           Environment (gamma ++ delta) ->
152 |           (env : Environment gamma ** Environment (delta env))
153 |   split [] delta env = (() ** env)
154 |   split (sigma .- gamma) delta (v ** env) =
155 |     let (env1 ** env2) = split (gamma v) (\env => delta (v ** env)) env in
156 |     ((v ** env1) ** env2)
157 |
158 | namespace Tree
159 |
160 |   export infixl 4 ><
161 |
162 |   mutual
163 |     ||| A tree of dependent types
164 |     public export
165 |     data Telescope : (k : Nat) -> Type where
166 |       Nil  : Telescope 0
167 |       Elt  : Type -> Telescope 1
168 |       (><) : (gamma : Tree.Telescope m) ->
169 |              (delta : Tree.Environment gamma -> Tree.Telescope n) ->
170 |               Telescope (m + n)
171 |
172 |     ||| A tuple of values of each type in the telescope
173 |     public export
174 |     Environment : Tree.Telescope k -> Type
175 |     Environment [] = ()
176 |     Environment (Elt t) = t
177 |     Environment (gamma >< delta) = (env : Environment gamma ** Environment (delta env))
178 |
179 |   export
180 |   concat : (gamma : Tree.Telescope k) -> (delta : Right.Telescope k ** Environment delta -> Environment gamma)
181 |   concat Nil = ([] ** id)
182 |   concat (Elt t) = ((t .- const []) ** fst)
183 |   concat (gamma >< delta) =
184 |     let (thetaL ** transpL) = concat gamma in
185 |     ((thetaL ++ \ envL => fst (concat (delta (transpL envL))))
186 |     ** \ env =>
187 |          let (env1 ** env2) = split thetaL (\ envL => fst (concat (delta (transpL envL)))) env in
188 |          (transpL env1 ** snd (concat (delta (transpL env1))) env2)
189 |     )
190 |
191 | export infix 5 <++>
192 |
193 | public export
194 | (<++>) : (gamma : Left.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (plusAcc m n)
195 | [] <++> delta = delta ()
196 | (gamma -. sigma ) <++> delta = gamma <++> (\ env => sigma env .- \ v => delta (env ** v))
197 |
198 | export infix 5 >++<
199 |
200 | (>++<) : {m, n : Nat} -> (gamma : Right.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
201 |          Left.Telescope (plusAcc m n)
202 | [] >++< delta = delta ()
203 | gamma@(_ .- _) >++< delta =
204 |   let (gamma ** sigma ** transp) = unsnoc gamma in
205 |   gamma >++< \ env => (cons (sigma env) (\ v => delta (transp env v)))
206 |
207 | export
208 | leftToRight : Left.Telescope m -> Right.Telescope m
209 | leftToRight gamma = rewrite sym (plusAccZeroRightNeutral m) in (gamma <++> const [])
210 |
211 | export
212 | rightToLeft : {m : Nat} -> Right.Telescope m -> Left.Telescope m
213 | rightToLeft gamma = rewrite sym (plusAccZeroRightNeutral m) in (gamma >++< const [])
214 |