🚀 go-pugleaf

In article <STEPHEN.92Apr15014937@estragon.uchicago.edu> stephen@estragon.uchicago.edu (Stephen P Spackman) writes:
   In article <BEVAN.92Apr14015933@panda.cs.man.ac.uk> bevan@cs.man.ac.uk (Stephen J Bevan) writes:
   | ... Why can't I
   | punt on the issue and call the type field an instance of special
   | "type" which itself can't appear in the "type" field?  (Forgive me if
   | this is straying too far, but isn't a similar "trick" done in category
   | theory, where there are "small" and "large" categories?)

   (1) there are perfectly sound type theories with type: type (even if I
   don't personally understand why), as has been known for many years.

Like? (I'm not doubting their existance, I'm just enquiring which
theories your refering to)


   (2) you were claiming that every value has a type field associated
   with it, and the value of the type field is optimised out. So the
   content of a type field is a value. So it has a type field, which has
   a value. It was your idea, not mine....

I think this is _your_ interpretation of idea.  Why does the contents
of a "type" field have to be a "value" like any other "value"?  In the
above model it has special status as I've pointed out already.


   It happens that I think your analysis is perfectly reasonable on an
   intuitive level, and I normally think about it in almost this way, but
   I think it's crucial to insist that the process is founded somewhere:

I agree, but where does it end?  IMHO all you can do is base the
definition on another model in the hope that this is well founded.
However, all you are doing is punting the issue to the well
foundedness of that model.  Is there some basis which you would like
to propose about which there is no doubt about its soundess?  If so,
how is that model "grounded"?

Stephen J. Bevan				bevan@cs.man.ac.uk