[Agda] Irrelevant record fields

[Andreas Abel]

Hi,

I just pushed a patch that allows now irrelevant fields in records.   
They work similar as discussed with Dan Doel on a recent thread.   
Irrelevant fields cannot be projected, internally they have been erased.

One can define a projection into the Squash type manually, whether  
Agda will do this for you in the future remains to be seen.  If in  
practice this should emerge as a convenient way to work with  
irrelevant fields, it might be added.

This is all very experimental, the printing of irrelevant things is  
still broken (there are dots all over the place).  Bug and experience  
reports welcome.

Andrea's example:

{-# OPTIONS --universe-polymorphism #-}
module AndreaVezzosi where

data Squash {a} (A : Set a) : Set a where
  squash : .A -> Squash A

open import Level
open import Relation.Binary.PropositionalEquality

module IrrRecord where

   record SemiG : Set1 where
    constructor _,_,_,_,_,_
    field
      M    : Set
      unit : M
      _+_  : M -> M -> M
      .assoc     : ∀ {x y z} ->  x + (y + z) ≡ (x + y) + z
      .leftUnit  : ∀ {x} -> unit + x ≡ x
      .rightUnit : ∀ {x} -> x + unit ≡ x

   dual : SemiG -> SemiG
   dual (M , e , _+_ , assoc , leftUnit , rightUnit) =
     M , e , (λ x y -> y + x) , sym assoc , rightUnit , leftUnit

   -- note: needed to match, since projections assoc, rightUnit,  
leftUnit are not available

   dual∘dual≡id : ∀ {M} -> dual (dual M) ≡ M
   dual∘dual≡id = refl

Cheers,
Andreas

On Sep 24, 2010, at 12:54 AM, Andreas Abel wrote:

> Hi Andrea,
>
> since records do not support irrelevant fields yet, I suggest to use  
> data instead:
>
>  data SemiG : Set1 where
>    _,_,_ : (M     : Set) ->
>            (_+_   : M -> M -> M) ->
>            .(∀ {x y z} ->  x + (y + z) ≡ (x + y) + z) ->
>            SemiG
>
>  dual : SemiG -> SemiG
>  dual (M , _+_ , assoc) = M , (λ x y -> y + x) , sym assoc
>
>  dual∘dual≡id : ∀ {M} -> dual (dual M) ≡ M
>  dual∘dual≡id {_ , _ , _} = refl
>
> Cheers,
> Andreas
>
> On Sep 23, 2010, at 5:58 PM, Andrea Vezzosi wrote:
>
>>
>> {-# OPTIONS --universe-polymorphism #-}
>> module Monoid where
>>
>> data Squash {a} (A : Set a) : Set a where
>> squash : .A -> Squash A
>>
>> open import Relation.Binary.PropositionalEquality
>>
>> record SemiG : Set1 where
>> constructor _,_,_
>> field
>>   M : Set
>>   _+_ : M -> M -> M
>>   assoc : Squash (∀ {x y z} ->  x + (y + z) ≡ (x + y) + z)
>>
>>
>>
>> dual : SemiG -> SemiG
>> dual (M , _+_ , assoc) = M , (λ x y -> y + x) , lemma where
>>    lemma : Squash ({x y z : M} → (z + y) + x ≡ z + (y + x))
>>    lemma with assoc
>>    lemma | squash y = squash (\ {_} {_} {_} -> sym y)
>>
>>
>> dual∘dual≡id : ∀ {M} -> dual (dual M) ≡ M
>> dual∘dual≡id {_ , _ , squash _} = refl

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/