Mercurial > urweb
comparison doc/tlc.ur @ 1507:ca8c8b8cc477
Tutorial: TLC meets type classes and modules
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 17 Jul 2011 13:04:07 -0400 |
parents | 44fda91f5fa0 |
children | d236dbf1b3e3 |
comparison
equal
deleted
inserted
replaced
1506:44fda91f5fa0 | 1507:ca8c8b8cc477 |
---|---|
200 (Some v, Some vs) => Some ({nm = v} ++ vs) | 200 (Some v, Some vs) => Some ({nm = v} ++ vs) |
201 | _ => None) | 201 | _ => None) |
202 (Some {}) fl r | 202 (Some {}) fl r |
203 | 203 |
204 (* See <tt>lib/ur/top.urs</tt> for the types of <tt>foldR</tt> and some other handy folding functions. *) | 204 (* See <tt>lib/ur/top.urs</tt> for the types of <tt>foldR</tt> and some other handy folding functions. *) |
205 | |
206 | |
207 (* * Working with First-Class Disjointness Obligations *) | |
208 | |
209 (* The syntax <tt>[r1 ~ r2]</tt> in a function definition introduces a constraint that the type-level records <tt>r1</tt> and <tt>r2</tt> share no field names. The same syntax may also be used with anonymous function definitions, which can be useful in certain kinds of record traversals. To pick a simple example, let's pretend that the general value-level <tt>++</tt> operator is missing form the language, so that we must implement it ourselves on top of a version of <tt>++</tt> that can only add one field at a time. This code demonstrates the use of the syntax <tt>!</tt> to discharge a disjointness obligation explicitly. This will generally only be needed when working with the <tt>@</tt> version of an identifier, which not only requires that folders be passed explicitly, but also disjointness proofs (which are always written as just <tt>!</tt>) and type class witnesses. *) | |
210 | |
211 fun concat [ts1 ::: {Type}] [ts2 ::: {Type}] [ts1 ~ ts2] | |
212 (fl : folder ts1) (r1 : $ts1) (r2 : $ts2) : $(ts1 ++ ts2) = | |
213 @foldR [id] [fn ts1 => ts2 ::: {Type} -> [ts1 ~ ts2] => $ts2 -> $(ts1 ++ ts2)] | |
214 (fn [nm ::_] [v ::_] [r ::_] [[nm] ~ r] v | |
215 (acc : ts2 ::: {Type} -> [r ~ ts2] => $ts2 -> $(r ++ ts2)) | |
216 [ts2] [[nm = v] ++ r ~ ts2] r => | |
217 {nm = v} ++ acc r) | |
218 (fn [ts2] [[] ~ ts2] (r : $ts2) => r) fl r1 ! r2 | |
219 | |
220 (* begin hide *) | |
221 val show_r = mkShow (fn r : {A : int, B : string, C : float, D : bool} => | |
222 "{A = " ^ show r.A ^ ", B = " ^ show r.B ^ ", C = " ^ show r.C ^ ", D = " ^ show r.D ^ "}") | |
223 (* end *) | |
224 | |
225 (* begin eval *) | |
226 concat {A = 1, B = "x"} {C = 2.3, D = True} | |
227 (* end *) | |
228 | |
229 | |
230 (* * Type-Level Computation Meets Type Classes *) | |
231 | |
232 (* Ur's treatment of type classes makes some special allowances for records. In particular, a record of type class witnesses may be inferred automatically. Our next example shows how to put that functionality to good use, in writing a function for pretty-printing records as strings. The type class <tt>show</tt> is part of the Ur standard library, and its instances are valid arguments to the string-producing function <tt>show</tt>. *) | |
233 | |
234 fun showRecord [ts ::: {Type}] (fl : folder ts) (shows : $(map show ts)) | |
235 (names : $(map (fn _ => string) ts)) (r : $ts) : string = | |
236 "{" ^ @foldR3 [fn _ => string] [show] [id] [fn _ => string] | |
237 (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] name shower value acc => | |
238 name ^ " = " ^ @show shower value ^ ", " ^ acc) | |
239 "...}" fl names shows r | |
240 | |
241 (* begin eval *) | |
242 showRecord {A = "A", B = "B"} {A = 1, B = 2.3} | |
243 (* end *) | |
244 | |
245 (* One natural complaint about this code is that field names are repeated unnecessarily as strings. Following Ur's design rationale, this is a consequence of a "feature," not a "bug," since allowing the syntactic analysis of type-level data would break the celebrated property of <b>parametricity</b>. *) | |
246 | |
247 | |
248 (* * Type-Level Computation Meets Modules *) | |
249 | |
250 (* To illustrate how the features from this chapter integrate with Ur's module system, let's reimplement the last example as a functor. *) | |
251 | |
252 functor ShowRecord(M : sig | |
253 con ts :: {Type} | |
254 val fl : folder ts | |
255 val shows : $(map show ts) | |
256 val names : $(map (fn _ => string) ts) | |
257 end) : sig | |
258 val show_ts : show $M.ts | |
259 end = struct | |
260 open M | |
261 | |
262 val show_ts = mkShow (fn r : $ts => | |
263 "{" ^ @foldR3 [fn _ => string] [show] [id] [fn _ => string] | |
264 (fn [nm ::_] [t ::_] [r ::_] [[nm] ~ r] name shower value acc => | |
265 name ^ " = " ^ @show shower value ^ ", " ^ acc) | |
266 "...}" fl names shows r) | |
267 end | |
268 | |
269 open ShowRecord(struct | |
270 con ts = [A = int, B = float, C = bool] | |
271 val names = {A = "A", B = "B", C = "C"} | |
272 end) | |
273 | |
274 (* begin eval *) | |
275 show {A = 1, B = 2.3, C = True} | |
276 (* end *) | |
277 | |
278 (* A few important points show up in this example. First, Ur extends the standard ML module system feature base by allowing functors to be applied to structures with omitted members, when those members can be inferred from the others. Thus, we call <tt>ShowRecord</tt> omitting the fields <tt>fl</tt> and <tt>shows</tt>. Second, merely calling a functor that produces an output with a type class instance can bring that instance into scope, so that it is applied automatically, as in our evaluation example above.<br> | |
279 <br> | |
280 To illustrate the mixing of constraints and functors, we translate another of our earlier examples in a somewhat silly way: *) | |
281 | |
282 functor Concat(M : sig | |
283 con f :: Type -> Type | |
284 con r1 :: {Type} | |
285 con r2 :: {Type} | |
286 constraint r1 ~ r2 | |
287 end) : sig | |
288 val concat : $(map M.f M.r1) -> $(map M.f M.r2) -> $(map M.f (M.r1 ++ M.r2)) | |
289 end = struct | |
290 fun concat r1 r2 = r1 ++ r2 | |
291 end | |
292 | |
293 structure C = Concat(struct | |
294 con f = id | |
295 con r1 = [A = int] | |
296 con r2 = [B = float, C = bool] | |
297 end) | |
298 | |
299 (* begin eval *) | |
300 show (C.concat {A = 6} {B = 6.0, C = False}) | |
301 (* end *) |