[Agda] Record scoping issue

[Jorn van Wijk]

Hi,

{-
While modelling some structure using a record, I was wondering if the
following is possible in Agda:
Having a property of given fields, defined inside a record, but useable to
instantiate/construct later record fields.
In the following bogus example, doubleA is a 'property' of field a. In
turn, b relies on this property. So I would like to use double to construct
b instead of redefining double.
-}

module RecordScope where

open import Data.Nat

module Problem where
  record R : Set where
    field
      a : ℕ
    doubleA : ℕ
    doubleA = a + a
    field
      b : ℕ
    squareB : ℕ
    squareB = b * b
    field
      c : ℕ

  example : R
  example =
    record
    { a = 2 -- we don't double because we have yet to define a
    ; b = {!doubleA + a!} -- I would like to have doubleA in scope here;
even a is not in scope
    ; c = {!doubleA * squareB!} -- 'c' relies on doubleA and squareB
    }

{-
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.
Such that given some r : R, we can just open R r, and bring everything into
scope.


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.
then when constructing a record we open the modules in a where block.
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.
The above example can possible be desugared into:
-}

module Solution where
  module R₀ where -- R₀ is anonymous or fresh and is not suppose to clash
with other modules
    module R₁ (a : ℕ) where
      doubleA : ℕ
      doubleA = a + a
      module R₂ (b : ℕ) where
        squareB = b * b

  record R : Set where
    open R₀ public
    field
      a : ℕ
    open R₁ a public
    field
      b : ℕ
    open R₂ b public
    field
      c : ℕ

  example : R
  example =
   record
   { a = a
   ; b = b
   ; c = c
   }
   where module _ where
            open R₀
            a : ℕ
            a = 2
            open R₁ a
            b : ℕ
            b = doubleA + a
            open R₂ b
            c : ℕ
            c = doubleA * squareB

  -- also, what does putting modules between fields have for functionality?:
  weird : R
  weird =
    record
    { R₀
    ; a = 2 -- we don't double because we have yet to define a
    ; R₀.R₁ 2 hiding (module R₂) renaming (doubleA to doubleA') -- what is
the purpose of a module assignment here?
    ; b = 4  -- doubleA' not in scope here..
    ; R₀
    ; c = 3
    }

--Or is there perhaps some other design pattern I should use to model the
problem?




Thanks for reading my post and kind regards,
Jorn
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160906/8736bae4/attachment.html