[Agda] default field values

[Andreas Abel]

As a work-around, you can define ``smart'' constructors that just need 
the values of a couple of fields and create the other ones from the 
given ones.

mkFoo n a = record { n = n; a = a; mb-b = mb-b n }
   where
     mb-b : ...
     mb-b zero    = nothing
     mb-b (suc _) = just a

On 18.01.14 11:32 AM, Sergei Meshveliani wrote:
> 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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>