90 | | === Proposal 1 |
91 | | |
92 | | Use syntax similar to functional dependencies. The injectivity declaration |
93 | | begins with `|` following type family declaration head. `|` is followed by a |
94 | | list of comma-separated injectivity conditions. Each injectivity condition has |
95 | | the form: |
96 | | |
97 | | {{{#!hs |
98 | | result A -> B |
99 | | }}} |
100 | | |
101 | | where `A` is a possibly-empty list of type variables declared in type family |
102 | | head and `B` is non-empty list of said type variables. Things on the left and |
103 | | right of `->` are called LHS and RHS of an injectivity condition, |
104 | | respectively. `result` becomes a restricted word that cannot be used as a type |
105 | | variable's identifier in a type family head. I think this is identical to how |
106 | | the `role` word is treated. Examples (taken from the previous section): |
107 | | |
108 | | {{{#!hs |
109 | | type family Id a | result -> a where |
110 | | type family F a b c | result -> a b c |
111 | | type family G a b c | result -> a b where |
112 | | type family Plus a b | result a -> b, result b -> a where |
113 | | type family H a b c | result a -> b c, result b -> a c |
114 | | }}} |
| 89 | We decided to use syntax similar to functional dependencies. The injectivity |
| 90 | declaration begins with `|` following type family declaration head. `|` is |
| 91 | followed by a list of comma-separated injectivity conditions. Each injectivity |
| 92 | condition has the form: |
| 93 | |
| 94 | {{{#!hs |
| 95 | A -> B |
| 96 | }}} |
| 97 | |
| 98 | where `A` and `B` are non-empty lists of type variables declared in type family |
| 99 | head. Things on the left and right of `->` are called LHS and RHS of an |
| 100 | injectivity condition, respectively. The user must be able to name the result of |
| 101 | a type family. To achieve that we extend syntax of type family head by allowing |
| 102 | to write `= tyvar` or `= (tyvar :: kind)` annotations in addition to already |
| 103 | allowed `:: kind` annotation. In other words all these declaration are |
| 104 | well-formed: |
| 105 | |
| 106 | {{{#!hs |
| 107 | type family Plus (a :: Nat) (b :: Nat) where ... |
| 108 | type family Plus (a :: Nat) (b :: Nat) :: Nat where ... |
| 109 | type family Plus (a :: Nat) (b :: Nat) = c where ... |
| 110 | type family Plus (a :: Nat) (b :: Nat) = (c :: Nat) where ... |
| 111 | }}} |
| 112 | |
| 113 | but the third or fourth form is required if the user wants to introduce |
| 114 | injectivity declaration. Here are examples of injectivity declarations using |
| 115 | proposed syntax: |
| 116 | |
| 117 | {{{#!hs |
| 118 | type family Id a = result | result -> a where |
| 119 | type family F a b c = d | d -> a b c |
| 120 | type family G a b c = foo | foo -> a b where |
| 121 | type family Plus a b = (sum :: Nat) | sum a -> b, sum b -> a where |
| 122 | type family H a b c = xyz | xyz a -> b c, xyz b -> a c |
| 123 | }}} |
| 124 | |
| 125 | Note that above examples demonstrate all three types of injectivivity but for |
| 126 | now we only plan to implement injectivity A. |
125 | | * steals `result` identifier in the type family head. This means it would be |
126 | | illegal to have a type variable named `result` in a type family. |
127 | | |
128 | | * the above makes this proposal backwards incompatible with `TypeFamilies` |
129 | | extension. |
130 | | |
131 | | Further proposals are based on this one in an attempt to solve the problem of |
132 | | stealing syntax and backwards incompatibility. |
133 | | |
134 | | |
135 | | === Proposal 2 |
136 | | |
137 | | Use `Result` instead of `result`: |
138 | | |
139 | | {{{#!hs |
140 | | type family Id a | Result -> a where |
141 | | type family F a b c | Result -> a b c |
142 | | type family G a b c | Result -> a b where |
143 | | type family Plus a b | Result a -> b, Result b -> a where |
144 | | type family H a b c | Result a -> b c, Result b -> a c |
145 | | }}} |
146 | | |
147 | | Pros: |
148 | | |
149 | | * has natural reading |
150 | | |
151 | | * extensible for the future |
152 | | |
153 | | * allows to have type variables named `result` (does not steal syntax) |
154 | | |
155 | | Cons: |
156 | | |
157 | | * all other keywords in Haskell are lower case. This would be the first one |
158 | | that is capitalized. |
159 | | |
160 | | * confusion could arise if we have a type `Result` and use it in the type |
161 | | family head. |
162 | | |
163 | | Unknowns (for me): |
164 | | |
165 | | * not sure if it would be possible to avoid name clash between `Result` and |
166 | | type of the same name. If not then this proposal would also be backwards |
167 | | incompatible with `TypeFamilies`. |
168 | | |
169 | | |
170 | | === Proposal 3 |
171 | | |
172 | | Use `type` instead of `result`: |
173 | | |
174 | | {{{#!hs |
175 | | type family Id a | type -> a where |
176 | | type family F a b c | type -> a b c |
177 | | type family G a b c | type -> a b where |
178 | | type family Plus a b | type a -> b, type b -> a where |
179 | | type family H a b c | type a -> b c, type b -> a c |
180 | | }}} |
181 | | |
182 | | Pros: |
183 | | |
184 | | * extensible for the future |
185 | | |
186 | | * no syntax stealing |
187 | | |
188 | | Cons: |
189 | | |
190 | | * no natural reading |
191 | | |
192 | | * usage of `type` here might seem unintuitive |
193 | | |
194 | | |
195 | | === Proposal 4 |
196 | | |
197 | | Use name of the type family instead of `result`: |
198 | | |
199 | | {{{#!hs |
200 | | type family Id a | Id -> a where |
201 | | type family F a b c | F -> a b c |
202 | | type family G a b c | G -> a b where |
203 | | type family Plus a b | Plus a -> b, Plus b -> a where |
204 | | type family H a b c | H a -> b c, H b -> a c |
205 | | }}} |
206 | | |
207 | | Pros: |
208 | | |
209 | | * extensible for the future |
210 | | |
211 | | * no syntax stealing |
212 | | |
213 | | Cons: |
214 | | |
215 | | * writing something like `Plus a` might be confusing. It looks as if `Plus` |
216 | | could be partially applied. |
217 | | |
218 | | === Proposal 5 |
219 | | |
220 | | A major drawback of all proposals 1-4, 6-7 is that if we only implement A injectivity then writing things like `result -> a b c d` is a lot of boilerplate (since there is only one possible injectivity condition anyway). We could avoid that by introducing `injective` keyword: |
221 | | |
222 | | {{{#!hs |
223 | | injective type family Id a where |
224 | | injective type family F a b c |
225 | | injective type family G a b c where |
226 | | injective type family Plus a b where |
227 | | injective type family H a b c |
228 | | }}} |
229 | | |
230 | | Pros: |
231 | | |
232 | | * no boilerplate for declaring A injectivity |
233 | | |
234 | | * probably backwards compatible, since there is only one place where the `injective` keyword may go. |
235 | | |
236 | | * could be extended in the future be allowing any of the proposals 1-4 to be used alternatively |
237 | | |
238 | | Cons: |
239 | | |
240 | | * steals "injective" identifier in type family head (I think) |
241 | | |
242 | | * not directly extensible. Introducing syntax from proposals 1-4 sometime in the future will end up with redundancy |
243 | | |
244 | | === Proposal 6 |
245 | | |
246 | | Don't write the `result`: |
247 | | |
248 | | {{{#!hs |
249 | | type family Id a | -> a where |
250 | | type family F a b c | -> a b c |
251 | | type family G a b c | -> a b where |
252 | | type family Plus a b | a -> b, b -> a where |
253 | | type family H a b c | a -> b c, b -> a c |
254 | | }}} |
255 | | |
256 | | Pros: |
257 | | |
258 | | * extensible for the future |
259 | | |
260 | | * backwards compatible |
261 | | |
262 | | Cons: |
263 | | |
264 | | * might be a bit confusing? |
265 | | |
266 | | === Proposal 7 |
267 | | |
268 | | Use type variable that names the RHS instead of `result`: |
269 | | |
270 | | {{{#!hs |
271 | | type family Id a :: result | result -> a where |
272 | | type family F a b c :: d | d -> a b c |
273 | | type family G a b c :: foo | foo-> a b where |
274 | | type family Plus a b :: sum | sum a -> b, sum b -> a where |
275 | | type family H a b c :: xyz | xyz a -> b c, xyz b -> a c |
276 | | }}} |
277 | | |
278 | | Pros: |
279 | | |
280 | | * extensible for the future |
281 | | |
282 | | * backwards compatible |
283 | | |
284 | | * we already allow naming the RHS in this way |
285 | | |
286 | | Cons: |
287 | | |
288 | | * ? |
| 138 | * since we only plan to implement injectivity of form A we require that there |
| 139 | is only one injectivity condition, its LHS contains only a type variable |
| 140 | naming the result and its RHS contains all type variables naming the |
| 141 | arguments to a type family. This might be a bit annoying. |
| 142 | |