[Agda] Inheriting fields

[Andreas Abel]

Hi Raghu,

record fields can be omitted if type inference reconstructs them through 
unification.  In this case, the values of Carrien and _\approx_ are 
determined by the type of isEquivalence, so the unifier puts them in.

Note: if the unifier does not find the missing record field values, you 
will see some yellow and Agda reports unsolved meta variables.

Cheers,
Andreas

On 12.02.2015 05:48, N. Raghavendra wrote:
> The Algebra module of stdlib defines
>
> --8<---------------cut here---------------start------------->8---
> record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
>    infixl 7 _∙_
>    infix  4 _≈_
>    field
>      Carrier     : Set c
>      _≈_         : Rel Carrier ℓ
>      _∙_         : Op₂ Carrier
>      isSemigroup : IsSemigroup _≈_ _∙_
>
>    open IsSemigroup isSemigroup public
>
>    setoid : Setoid _ _
>    setoid = record { isEquivalence = isEquivalence }
> --8<---------------cut here---------------end--------------->8---
>
> and Relation.Binary defines
>
> --8<---------------cut here---------------start------------->8---
> record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
>    infix 4 _≈_
>    field
>      Carrier       : Set c
>      _≈_           : Rel Carrier ℓ
>      isEquivalence : IsEquivalence _≈_
> --8<---------------cut here---------------end--------------->8---
>
> So to specify setoid within the Semigroup definition, we don't need to
> write
>
> --8<---------------cut here---------------start------------->8---
> ...
>    setoid : Setoid
>    setoid = record { Carrier = Carrier
>                    ; _≈_ = _≈_
>                    ; isEquivalence = isEquivalence
>                    }
> --8<---------------cut here---------------end--------------->8---
>
> The Carrier and _≈_ fields in setoid seem to be inherited from the
> Semigroup.  Is there some document which describes such inheritance?
> I've seen the records section and tutorial in the reference manual, but
> couldn't find this.
>
> Thanks,
> Raghu.
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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