First-class positivity and injectivity [Re: [Agda] A type for positive type functors?]

[Andreas Abel]

Hi Nicolas,

abstracting out (strictly) positive functions works via polarities in 
MiniAgda.  See e.g. my paper

Polarized Subtyping for Sized Types
Mathematical Structures in Computer Science, vol. 18, pp. 797-822, 
special issue on subtyping. © Cambridge University Press.

I am very interested also in injective functions.  Do you know a good 
reference for this.  Does someone have a type system for injectivity? 
The only reference I have is:

@InProceedings{	  pfenning:strictness,
   author	= {Frank Pfenning and Carsten Sch\"urmann},
   title		= {Algorithms for equality and unification in the presence of
		  notational definitions},
   booktitle	= {Types for Proofs and Programs},
   pages		= {179--193},
   year		= 1998,
   volume	= 1657,
   series	= {LNCS},
   publisher	= {Springer-Verlag},
}

Cheers,
Andreas

On 11/18/10 10:20 PM, Nicolas Pouillard wrote:
> On Thu, 18 Nov 2010 19:55:07 +0100, Andreas Abel<andreas.abel at ifi.lmu.de>  wrote:
>> Hi Dominique,
>>
>> in your case, I am afraid, you have to turn off the positivity checker.
>>    Agda checks positivity by unfolding definitions, this is why the
>> concrete version with Maybe works.  However, if you abstract Maybe to a
>> variable M, positivity hold only if M is positive itself.
>>
>> Currently Agda cannot handle this.  In my toy language MiniAgda it
>> works, because you can declare M to be strictly positive as follows:
>>
>>     data EventHandlerMonad ++(M : Set ->  Set) (E : Set) (A : Set) : Set ...
>>
>> telling the positivity checker that M is assumed to be strictly positive
>> and can only be instantiated with strictly positive type functions.
>
> This would be a very nice addition to Agda! In the same vein being able to
> abstract over injective functions/constructors would be really helpful.
>
> Actually any syntactic criterion could be equiped with a way to abstract over
> things having this criterion.
>

-- 
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/