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

[Gabriel Scherer]

> 3. if you want a non-linear index or non-pattern index, use explicit
> identity proofs embedded in you data structure

Note that this counter-attacks the comment that "GADTs are just a weak
form of dependent types". The core mechanism of GADTs is equalities
between indices (types in a ML/Haskell language, while terms would be
more proper), and people claiming that they're entirely subsumed by
dependent types indeed replace this by non-linear inductive
constructors. That you need to expand this again into explicit
equations shows that the equality business is there to stay.

On Sat, Dec 15, 2012 at 1:52 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda