Changes between Version 39 and Version 40 of Records/NameSpacing

Jan 22, 2012 8:51:15 PM (4 years ago)

explain Agda


  • Records/NameSpacing

    v39 v40  
    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.
     1See [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.
    33This approach is an attempt to port the records solution in [ 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 [ Frege user manual]
    42 == A case for why name-spacing alone is a decent solution ==
     42== Agda: A case for why name-spacing alone is a good enough solution ==
    4444 * You can use a type synonym to abbreviate the namespace part (as
    5656The Agda language [ 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)].
    58 == Getting rid of the Verbosity with the dot operator ==
     58The 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:
     61  data Record = Record { a :: String }
     62  r = Record "A"
     64  module Open where
     65    open Record
     67    -- record is in scope
     68    aOK :: String
     69    aOK = a r
     71  -- alternative Agda syntax
     72  again : String
     73  again = a r where open Record
     76This works better in Agda which can have multiple modules per file, but could be very useful in Haskell even without local modules.
     79== Frege: Getting rid of the Verbosity with the dot operator ==
    6081We 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 }`
    133154This is overly-simplistic for Haskell (see above)
    135 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.
    137 Back to simple type resolution. From the Frege Author:
     156From the Frege Author:
    139158 * Expressions of the form T.n are trivial, just look up n in the namespace T.
    144163Note 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
    146 So lets see examples behavior from the Frege Author:
    148165For example, lets say we have:
    245262instance Rextension1 R where
    246      -- implementation for new functions
    247 }}}
    249 the new functions `f` and `g` are accessible (only) through R.
     263     -- implementation for f and g
     266the new functions `f` and `g` are accessible (only) through R: `r.f, r.g`.
    250267So we have a technique for lifting new functions into the Record namespace.
    251268For 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.