Mercurial > urweb
comparison demo/prose @ 417:e0e9e9eca1cb
Fix nasty de Bruijn substitution bug; TcSum demo
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 23 Oct 2008 12:58:35 -0400 |
| parents | 679b2fbbd4d0 |
| children | ad7e854a518c |
comparison
equal
deleted
inserted
replaced
| 416:679b2fbbd4d0 | 417:e0e9e9eca1cb |
|---|---|
| 98 An unusual part of the third argument is the syntax <tt>[t1 ~ t2]</tt> within a multi-argument <tt>fn</tt>. This syntax denotes a proof that row types <tt>t1</tt> and <tt>t2</tt> have no field names in common. The proof is not named, because it is applied automatically as needed. Indeed, the proof appears unused in this case, though it is actually needed to ensure the validity of some inferred types, as well as to unify with the type of <tt>foldUR</tt>.</p> | 98 An unusual part of the third argument is the syntax <tt>[t1 ~ t2]</tt> within a multi-argument <tt>fn</tt>. This syntax denotes a proof that row types <tt>t1</tt> and <tt>t2</tt> have no field names in common. The proof is not named, because it is applied automatically as needed. Indeed, the proof appears unused in this case, though it is actually needed to ensure the validity of some inferred types, as well as to unify with the type of <tt>foldUR</tt>.</p> |
| 99 | 99 |
| 100 <p>The general syntax for constant row types is <tt>[Name1 = t1, ..., NameN = tN]</tt>, and there is a shorthand version <tt>[Name1, ..., NameN]</tt> for records of <tt>Unit</tt>s.</p> | 100 <p>The general syntax for constant row types is <tt>[Name1 = t1, ..., NameN = tN]</tt>, and there is a shorthand version <tt>[Name1, ..., NameN]</tt> for records of <tt>Unit</tt>s.</p> |
| 101 | 101 |
| 102 <p>With <tt>sum</tt> defined, it is easy to make some sample calls. The form of the code for <tt>main</tt> does not make it apparent, but the compiler must "reverse engineer" the appropriate <tt>{Unit}</tt> from the <tt>{Type}</tt> available from the context at each call to <tt>sum</tt>.</p> | 102 <p>With <tt>sum</tt> defined, it is easy to make some sample calls. The form of the code for <tt>main</tt> does not make it apparent, but the compiler must "reverse engineer" the appropriate <tt>{Unit}</tt> from the <tt>{Type}</tt> available from the context at each call to <tt>sum</tt>.</p> |
| 103 | |
| 104 tcSum.urp | |
| 105 | |
| 106 <p>It's easy to adapt the last example to use type classes, such that we can sum the fields of records based on any numeric type.</p> |