It's kind of hard to get into specifics because there are so many different type theories.
But my canonical example is the claim that boolean values are not integers. This is an egregious mistatement of history. George Boole's algebra was all about integers. But somewhere along the line boolean algebra was constrained to 1 and 0 values so that logical negation could be incorporated into it. And, later, some people building compilers decided that their lives would be simpler if they declared that boolean values were not integers. And while it's true that a set containing only 1 and 0 is a different set from a set which contains more of the integers, that doesn't mean that one is not a subset of the other. So nowadays it's popular to reject set theory entirely, bringing in a more ornate system (category theory) which includes in it constraints that allow one to implicitly have different forms of (for example) 1 and 0 where it's an error to even talk about them being equivalent. Rather than go into all those details, I summarized by saying that type theory avoids regularity. Does that make sense? Is this a problem though? In some contexts it's obviously not only not a problem - it's important to many people to be able to generate errors, and type theory is perfect. In other contexts though, it can be very much a problem. It all depends on what you are trying to accomplish (or, in many cases, what you are trying to prevent from being accomplished). That said, note also that I hold up J's notational system as an example of what I mean by "regularity". (And, also, I think about type theory in terms of how that might play out if we had compilers for subsets of J.) Thanks, -- Raul On Thu, Jun 5, 2014 at 3:46 AM, Marc Simpson <[email protected]> wrote: > [moving to chat@] > > Hi Raul, > > On Tue, Jun 3, 2014 at 4:49 PM, Raul Miller <[email protected]> wrote: > > One of the big problems is that the dogma of type theory mostly works by > > avoiding regularity. That's fairly natural: people want to shine. > > Would you mind clarifying what you mean by the above? > > Thanks, > Marc > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm > ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
