Linear Pattern Inductive Famlies [Re: [Agda] no longer type checks]

[Andreas Abel]

On 14.12.12 8:24 PM, Peter Hancock wrote:
> On 14/12/2012 19:00, Martin Escardo wrote:
>> Thanks, Andreas. This is a helpful explanation.
>>
>> I think that maybe it is an open research question what kind of
>> pattern matching corresponds to (intensional) MLTT (without the K
>> axiom). That should be interesting to know for sure. But I am glad
>> that there is some preliminary experimental work in Agda going on.
>
> I agree.  Another important thing which does not seem to be clear is:
> what is an inductive definition without *any* non-linearity among the
> indices?
> So, one serious question is: what distinguishes an index from a parameter?
>
> To me, it is not unthinkable that such a version of type-theory might
> exclude the
> exciting identity type.  It may, perhaps, be formulated axiomatically,
> and justified by a model.  The model construction seems to be difficult
> and subtle.

I think a reasonable alternative to the inductive families we have now 
would be the following:

1. indices may only be linear patterns (excludes the identity type and 
awkward types)
2. identity is added as primitive
3. if you want a non-linear index or non-pattern index, use explicit 
identity proofs embedded in you data structure

Ad 1.  This removes major complications in the theory of inductive 
families.  Unification for patterns is decidable, so it could be decided 
if a constructor matches a family slice.  Also, it allows erasure of 
*all* index variables at runtime (Brady's "...need not store their 
indices").

Ad 2.  This would allow different identity types to play with, like 
Leibniz, heterogeneous, OTT, HTT-equality and more...

Ad 3.  Currently, if you want to match on an awkward family (non-pattern 
family), you need to rewrite it into form 3. in most cases anyway.

Cheers,
Andreas

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