<div dir="ltr">Hi,<br><br>{-<br>While modelling some structure using a record, I was wondering if the following is possible in Agda:<br>Having a property of given fields, defined inside a record, but useable to instantiate/construct later record fields.<br>In the following bogus example, doubleA is a &#39;property&#39; of field a. In turn, b relies on this property. So I would like to use double to construct b instead of redefining double.<br>-}<br><br>module RecordScope where<br><br>open import Data.Nat<br><br>module Problem where<br>  record R : Set where<br>    field<br>      a : ℕ<br>    doubleA : ℕ<br>    doubleA = a + a  <br>    field<br>      b : ℕ<br>    squareB : ℕ<br>    squareB = b * b<br>    field<br>      c : ℕ<br><br>  example : R<br>  example =<br>    record<br>    { a = 2 -- we don&#39;t double because we have yet to define a<br>    ; b = {!doubleA + a!} -- I would like to have doubleA in scope here; even a is not in scope<br>    ; c = {!doubleA * squareB!} -- &#39;c&#39; relies on doubleA and squareB<br>    }<br><br>{-<br>In the above example, doubleA is not in scope at b (same for squareB and doubleA at c). Is there any way around this, to still have one definition of doubleA and squareB while maintaining the other benefits of this example.<br>Such that given some r : R, we can just open R r, and bring everything into scope.<br><br><br>Towards solving this problem, I came up with a solution consisting of nesting the definitions inside modules; each field block comes with a potential module before it.<br>then when constructing a record we open the modules in a where block.<br>Since, as far as i know, there is no syntax to specify a where block for each field. I defined a single where block and an anonymous module to define the fields.<br>The above example can possible be desugared into:<br>-}<br><br>module Solution where<br>  module R₀ where -- R₀ is anonymous or fresh and is not suppose to clash with other modules<br>    module R₁ (a : ℕ) where<br>      doubleA : ℕ<br>      doubleA = a + a<br>      module R₂ (b : ℕ) where<br>        squareB = b * b<br>    <br>  record R : Set where<br>    open R₀ public<br>    field<br>      a : ℕ<br>    open R₁ a public<br>    field<br>      b : ℕ<br>    open R₂ b public<br>    field<br>      c : ℕ<br><br>  example : R<br>  example =<br>   record<br>   { a = a<br>   ; b = b<br>   ; c = c<br>   }<br>   where module _ where<br>            open R₀ <br>            a : ℕ<br>            a = 2<br>            open R₁ a<br>            b : ℕ<br>            b = doubleA + a<br>            open R₂ b<br>            c : ℕ<br>            c = doubleA * squareB<br><br>  -- also, what does putting modules between fields have for functionality?:<br>  weird : R<br>  weird = <br>    record<br>    { R₀<br>    ; a = 2 -- we don&#39;t double because we have yet to define a<br>    ; R₀.R₁ 2 hiding (module R₂) renaming (doubleA to doubleA&#39;) -- what is the purpose of a module assignment here?<br>    ; b = 4  -- doubleA&#39; not in scope here..<br>    ; R₀<br>    ; c = 3<br>    }<br>   <br>--Or is there perhaps some other design pattern I should use to model the problem?<br><br><br><br><br>Thanks for reading my post and kind regards,<br>Jorn<br></div>