[Agda] default field values

[Sergei Meshveliani]

On Fri, 2014-01-17 at 16:50 -0500, Wolfram Kahl wrote:
> On Tue, Jan 14, 2014 at 04:44:43PM +0400, Sergei Meshveliani wrote:
> > -- I -----------------------------------------------------------------
> > record Foo {α α=} (A : Setoid α α=) : Set α
> >   where
> >   open Setoid A
> > 
> >   field  n    : ℕ
> >          a    : Carrier
> > 	 mb-b : Maybe Carrier
> > 
> >   default-mb-b : n ≤ 1 → Maybe Carrier
> >   default-mb-b _ =  just a
> > 
> >   mb-b-law : n ≤ 1 → Set _
> >   mb-b-law _ =  mb-b ≡ just a
> > ---------------------------------------------------------------------- 
> > 
> > I need to specify that 
> >  
> >   mb-b  is assigned  (just a)  for all the record instances in which 
> >                                                                n ≤ 1.
> > 
> > The two lines of  default-mb-b  express something close to this -- but  
> > not precisely.
> > mb-b-law  is another attempt.
> 
> I'd say that  mb-b-law  wants to be a  field .
> 

I am not sure that I understand the idea.
Let us simplify the example:

  record Foo {α α=} (A : Setoid α α=) : Set α
    where
    open Setoid A
 
    field  a : Carrier

 	   mb : Maybe Carrier
           mb = just a        -- default implementation


mb  is a field. And the last line is not allowed in the Agda language.
Right?

And I suggest that this line of  mb = ...
to work as  default.
This means that  
1) the   mb  implementation in any Foo instance overrides the default 
   one (that is a special case overrides, it is stronger), 
2) the checker sets the default implementation for each instance of Foo 
   in which the field   mb  is skipped.

This `default' construct in languages is well-known. Its purpose is to
make instances simpler to program: if the programmer does not consider
the case as special with respect to the field  foo,  one skips its
implementation.

Has this sense in Agda ?

I think, its model in Agda is like this:

  record Foo {α α=} (A : Setoid α α=) : Set α
    where
    open Setoid A
 
    field  a : Carrier
 	   mb : Maybe Carrier
           
    default-mb : Maybe Carrier
    default-mb = just a

Now, when the programmer implements an Foo instance, one sets

     record{ ...
             mb = default-mb    -- a common instance
           }

for a general case, and   ...
                          mb = <special-implementation>   
for a special case. 
So, the code overhead in  Agda-without-default  is only this: 
a) a new function name  `default-...'  is introduced,
b) an additional line of   ... = default-...  is inserted in many
instances. 
              
As to the example with a conditional default, like by  n ≤ 1,  it is an
unclear complication which could be considered later. 

Am I missing something?

Thanks,

------
Sergei