[Agda] default field values

[Sergei Meshveliani]

A least there is an evident special case:  unconditional default. 
That is if in the instance 
                          record{ ... }

the field  foo  is skipped,  the checker sets the default value declared
in the record declaration.

In the general case, one may be need to somehow set indexes for
additional arguments and transfer the corresponding values inside  
record{ ... }  by using some keyword.
 
------
Sergei


On Tue, 2014-01-14 at 16:44 +0400, Sergei Meshveliani wrote:
> People,
> I have a question about a  default value in a record  
> in the Agda language
> 
> (I do not know, may be I am missing some simple consideration).
> 
> Consider the example:
> 
> -- 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.
> With both these expressions, the programmer will have certain
> difficulties with using the corresponding default value.
> 
> Try another way:
> 
> -- II -------------------------------------------------------------
> record Pre-Foo {α α=} (A : Setoid α α=) : Set α
>   where
>   open Setoid A
>   field  n    : ℕ
>          a    : Carrier
>          mb-b : Maybe Carrier
> 
> record Foo {α α=} (A : Setoid α α=) : Set α
>   where
>   open Setoid A
> 
>   field  preFoo : Pre-Foo A
> 
>   open Pre-Foo preFoo
> 
>   foo : Pre-Foo A
>   foo = record { n    = n;
>                  a    = a;
>                  mb-b = case n ≤? 1 of \ { (yes _) → just a
>                                          ; (no _)  → mb-b   }
>        	       }
> --------------------------------------------------------------------
> 
> Foo  takes  Pre-Foo  and updates the field  mb-b  respectively.
> I doubt of whether this approach is better than (I).
> 
> It occurs that 
> 
>   one needs to program a value for  mb-b  individually for each record  
>   instance,
>   while is is desirable to define a default case value, and to declare 
>   it as a part of the record declaration.
> 
> 
> Consider a new syntax with a keyword `default' :
> 
>   record Foo {α α=} (A : Setoid α α=) : Set α
>     where
>     open Setoid A
> 
>     field  n    : ℕ
>            a    : Carrier
>            mb-b : Maybe Carrier        
> 
>     default                                                        
>       mb-b : n ≤ 1 → Maybe Carrier    
>       mb-b _ = just a   
> 
> (I doubt about the precise signature) 
> 
> -- with the meaning of a default for the field  mb-b  by the condition
> n ≤ 1.
> 
> There arise the questions:
> 
> 1) Can this notion be nicely expressed in the current Agda ?
> 2) What will happen with the language after introducing `default' ?
> 3) If it has sense, is it difficult to implement?
> 
> Thanks,
> 
> ------
> Sergei
>  
> 
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>