[Agda] eta expansion

[Andreas Abel]

If understands inductive families as least fixed-points, then one needs 
equality to be defined already before one can interpret Agda's data 
types.  Therefore I agree that identity types should be something 
special, and data types could be restricted to pattern inductive 
families.  Such a restriction is easy to implement.  (However, probably 
one should still provide the current liberal data types to users that 
rely on them...).

Cheers,
Andreas

On 09.03.13 7:31 PM, Peter Hancock wrote:
> My opinion on these:
>
>> (1) Pattern matching.
>>
>> Is fine provided refl is not a pattern (except for the definition of
>> J).  Good to have without-K, but not so good that there isn't a
>> theory of pattern matching without K, or any assurance that without-K
>> actually works. This is particularly relevant for the HoTT
>> enthusiasts using Agda.
>>
> ...
>> Id types should be treated separately, as well as Sigma types (?). I
>> don't believe in the generality of the "data" concept that allows Id,
>> Sigma and W, and many more things, under the same umbrella.
>
> The thing about trying to understand Id as an inductive definition
> is that it stands apart from honest-to-god inductive definitions in
> the non-linearity of the variables in the type of the constructor.
> Conor McBride calls this "focusing", which I think is a good word.
>
> It is some time since I knew anything about type-checking algorithms, but
> I think Id involves unification.  Unification between first order terms
> is one thing, and unification between the kind of higher order entities
> that are involved in dependent type theory is just too complicated and
> fraught with subtleties to be understandable, and therefore, to be
> implemented.
> (Except as an experiment, or personal entertainment.)
>
> So I agree that Id types, that seem to be a very worthwhile notion,
> should be treated separately, rather than cramming them into the
> Procustean bed
> of inductive types, in which bed, by the way, I think Pi-sets, Sigma-sets,
> W-sets, universes, and what-not nicely fit.
>
> The topic of pattern matching, and what more there may be to it than
> Martin-Lof-style eliminators is not new.  A predecessor of Agda, called
> Alf and implemented by Lena Magnusson raised this issue in the 90's.  It
> would
> allow you to define K.  In my opinion, the people who know most about this
> subject are Thierry Coquand and Conor McBride.  They have both changed
> their
> minds at least once about the topic, which is often a sign of thinking
> hard.
>
> About Sigma-types, it depends which ones you mean.  There are Sigma-types,
> perhaps, in the logical framework.  They are defined by their eliminators,
> the projections.  They seem to me pretty well captured by Agda's records,
> that have some kind of eta.  Then there are Sigma-sets, living in the
> "universe" Set, that are defined by their constructors, ie are inductively
> defined, and satisfy eta only wrt Id.  In my opinion, you should
> carefully distinguish these.  They are conflated in category theory.
>
> One more thing. I believe Thomas Streicher, knowing of the propositional
> eta-laws for Pi-sets
> and Sigma-sets, was led to ask how this phenomenon played-out for Id-sets,
> saw that it didn't, and naturally wondered why it missing. Thomas thought
> he'd detected something missing, and proposed K.  Another view, mine, is
> that he'd actually detected that Id-sets are something lying outside core
> type-theory, not "missing", but to be treated in an entirely different way,
> perhaps axiomatically.  Then there is the very urgent question of how
> this new
> kind of type should be understood computationally, which many clever people
> are thinking about.
>
> Hank
> _______________________________________________
> 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/