[Agda] eta expansion

[Peter Hancock]

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