[Agda] Records and irrelevant fields

[Andreas Abel]

Hi Dan and Wren,

my take on making Squash a monad was to allow matching on irrelevant  
things if there is at most one match.  There is no theoretical  
foundation for this yet, so maybe it is unsound, but it seems to be  
consistent with erasure semantics.

   join : {A : Set} -> Squash (Squash A) -> Squash A
   join (squash (squash a)) = squash a

Well, that in essence says you cannot get more irrelevant than  
irrelevant.

Interestingly, the bind operation cannot be defined directly,

   bind : {A B : Set} -> Squash A -> (A -> Squash B) -> Squash B
   bind (squash a) f = f a -- a cannot be used here!

but in terms of map and join (as in the textbooks).

   bind sa f = join (map f sa)

That's a bit weird.  (Not the first weirdness, as we have seen.)

On another note:  I have implemented a bit of irrelevance analysis for  
MiniAgda (see my homepage). It cannot do the ETPS stuff yet (the  
useless variable analysis), but I am working to get there.  So far, I  
uses Size (universe levels) to find type arguments in functions and  
Edwin Brady's analysis to find index arguments in constructors.

Cheers,
Andreas


On Sep 18, 2010, at 8:07 AM, Dan Doel wrote:

> On Saturday 18 September 2010 1:42:28 am wren ng thornton wrote:
>> But I'm not terribly familiar with EPTSes yet. I've had some  
>> thoughts on
>> how to do irrelevance better than Coq (e.g., removing the Set/Prop
>> distinction). I'd thought my ideas were along the same lines as  
>> EPTSes,
>> though maybe not...
>
> They may well be along the same lines, in that irrelevance is  
> expressed by a
> modality. It may just not be the same modality.
>
> If you don't have it already, you might want to also look at Frank  
> Pfenning's
> Intensionality, Extensionality and Proof Irrelevance in Modal Type  
> Theory. *
> He has a theory with three different modalities (and equality  
> types). I
> haven't studied hard enough to know if/how his proof irrelevant  
> modality is
> different from the one in EPTSes, but I suspect it is.
>
> (I was going to send this off list, but it might be relevant to the  
> larger
> conversation. Andreas mentioned LiCS earlier, and that's by  
> Pfenning. Was it
> an implementation of something like the stuff in the above paper?)
>
> -- Dan
>
> [*] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.5884
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

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/