Changes between Version 39 and Version 40 of Records/NameSpacing

Timestamp:

01/22/12 12:51:15 (16 months ago)

Author:

GregWeber

Comment:

explain Agda

Records/NameSpacing

@@ -1 @@
-See [wiki:Records] for the bigger picture. This is a proposal to solve the records name-spacing issue with simple name-spacing and simple type resolution.
+See [wiki:Records] for the bigger picture. This is a proposal to solve the records name-spacing issue with name-spacing and how to expand on that to make record access more convenient.
 
 This approach is an attempt to port the records solution in [http://code.google.com/p/frege/ Frege], a haskell-like language on the JVM. Please read Sections 3.2 (primary expressions) and 4.2.1 (Algebraic Data type Declaration - Constructors with labeled fields) of the [http://code.google.com/p/frege/downloads/detail?name=Language-411.pdf Frege user manual]
@@ -40 +40 @@
 
 
-== A case for why name-spacing alone is a decent solution ==
+== Agda: A case for why name-spacing alone is a good enough solution ==
 
  * You can use a type synonym to abbreviate the namespace part (as
@@ -56 +56 @@
 The Agda language [http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Records generates a module (name space) for each record and also allows a record, like any module to be placed into the global scope by the programmer (opened in Agada terms)].
 
-== Getting rid of the Verbosity with the dot operator ==
+The downside of the pure module system is needing to always prefix the field: `Record.a r`. In Agda, a record is a module, and a module can be opened up. The "Record opening example" from the Agda page is transferred to a Haskell-like syntax here:
+
+{{{
+  data Record = Record { a :: String }
+  r = Record "A"
+
+  module Open where
+    open Record
+
+    -- record is in scope
+    aOK :: String
+    aOK = a r
+
+  -- alternative Agda syntax
+  again : String
+  again = a r where open Record
+}}}
+
+This works better in Agda which can have multiple modules per file, but could be very useful in Haskell even without local modules.
+
+
+== Frege: Getting rid of the Verbosity with the dot operator ==
 
 We have name-spaces, but it is hard to see how this is better than the current practice of adding prefixes to record fields: `data Record = Record { recordA :: String }`
@@ -133 +154 @@
 This is overly-simplistic for Haskell (see above)
 
-Frege has a detailed explanation of the semantics of its record implementation, and the language is *very* similar to Haskell. After reading the Frege manual sections, one is still left wondering: how does Frege implement type resolution for its dot syntax. The answer is fairly simple: overloaded record fields are not allowed. So you can't write code that works against multiple record types. Please see the comparison with Overloading in [wiki:Records], which includes a discussion of the relative merits. Note that the DDC thesis takes the same approach.
-
-Back to simple type resolution. From the Frege Author:
+From the Frege Author:
 
  * Expressions of the form T.n are trivial, just look up n in the namespace T.
@@ -143 +162 @@
 
 Note that this means it is possible to improve upon Frege in the number of cases where the type can be inferred - we could look to see if there is only one record namespace containing n, and if that is the case infer the type of x -- Greg Weber
-
-So lets see examples behavior from the Frege Author:
 
 For example, lets say we have:
@@ -244 +261 @@
 
 instance Rextension1 R where
-     -- implementation for new functions
-}}}
-
-the new functions `f` and `g` are accessible (only) through R.
+     -- implementation for f and g
+}}}
+
+the new functions `f` and `g` are accessible (only) through R: `r.f, r.g`.
 So we have a technique for lifting new functions into the Record namespace.
 For the initial records implementaion we would want to maintain `f` and `g` at the top-level, but should consider also adding through the record name-space. See related discussion below on future directions.