Changes between Version 39 and Version 40 of Records/NameSpacing

Jan 22, 2012 8:51:15 PM (3 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.