[Agda] no-field record

[Andreas Abel]

It seems that in this case you really just want a module

   module Foo (foo1 : Bool) where
     ...

   let open Foo true
   in  foo9

Well "modules are not first class data", yes, but all you use of your 
record definition below is the associated record module.  So, you gain 
nothing by using a record instead of a module, in the contrary, you blow 
up all the definitions foo2...foo9 by a (hidden) dummy record argument.

Cheers,
Andreas

On 11.02.13 9:25 PM, Serge D. Mechveliani wrote:
> People,
> I have a beginner question about a  record with no `field':
>
>    record Foo (foo1 : Bool) : Set _ where
>                                     foo2 : Bool
>                                     foo2 = not foo1
>                                     foo3 : Foo3
>                                     foo3 = ...
>                                     ...
>                                     foo9 : Foo9
>                                     foo9 = ...
>
> I use it like this:  let r : Foo true
>                           r = _
>                       in  Foo.foo9 r
>
> 1. One of this style records is type-checked but not compiled
>     -- of which I have recently reported on Agda-2.3.2 MAlonzo.
>
> 2. Are parameterized modules better to use than such records?
>     (as I recall, modules are not first class data).
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/