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

[Andreas Abel]

On 15.12.2012 08:44, Gabriel Scherer wrote:
>> 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.

Indeed.  One could say GADTs are weaker since they only along equalities 
between types, and families are stronger because they also allow 
equalities between values.

On the other hand, GADTs correspond to "large indices" which are not 
allowed in predicative type theory, so there GADTs are not subsumed by 
type equalities if one considers an predicative sizing of propositional 
equality.

Cheers,
Andreas

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


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