Re: Notions of Type

Keith H Duggar wrote:
> Bob Badour wrote:
>

>>Keith H Duggar wrote:
>>
>>>When you have a chance I'd appreciate your thoughts. Oh,
>>>and of course same goes for any other type theory
>>>enthusiasts out there.
>>
>>I don't recall saying that type theory failed in any
>>manner. Perhaps you could point to where you reached that
>>conclusion? Perhaps I misspoke, or perhaps the comment
>>applies within a limited context.

>>My only objection to "type = algebraic structure" is the
>>requirement for closure within a single type.

That equates to my understanding of type, then, in the context of computing.

>>For any type, we can define the algebra as the type and
>>the subset of the type's operations that exhibit closure.
>>In my view, the type includes the entire set of operations
>>defined on the values of the type including those not
>>exhibiting closure.

What /defined/ means depends on the level and scope of discourse. Conceptually, any describable operation defined on the type is defined on the type. One may, of course, explicitly limit the scope to those operations describable using a given set of base operations, but at the conceptual level, I would contend that--even in this case--the type includes more than just the base operations. Then again, one may explicitly limit the scope to just about anything one wants to.

Mathematics is formal (unlike the informal conceptual level of discourse.) At the logical or formal level of discourse, only those operations with formal descriptions have meaning. In a sense, a formalism defines a language, which limits the scope of discourse.

What you provided above was just such a language.

When I refer to 'type' at the logical level of discourse, I generally mean it in it's broadest most encompassing meaning. ie. that which is closest to the meaning at the conceptual level of discourse given the available formalism.

Thus, if I start with an integer data type with addition and subtraction and if I then extend the system by writing a program for multiplication, I have not changed the type of values already recorded. All I have done is formally describe yet another of the operations defined on the type. Conceptually, that particular multiplication operation was always part of the type even before it had a formal description.

I say 'that particular multiplication operation' because one could write different programs that are more-or-less multiplication. For instance, while it is less likely for an integer type than a rational type, a poor choice of algorithm could lead to undesirable effects under certain conditions or a certain algorithm could have a bug under rare conditions etc. All of these variations are equally operations defined on the type, and we might call all of them multiplication within our formalism at one time or another.

It is, of course, possible to limit the scope of discourse arbitrarily and explicitly. Most implemented computing systems do that in one way or another. Thus, one can explicitly say that some set of operations defined on the type are part of the type specification and some other set of operations defined on the type are not. The distinction might depend on who created the programs or where the programs are stored etc. However, I don't see those distinctions as important to any theory.

The arbitrary distinctions can have strange repercussions like the security function changing the 'type' of a value depending on the user or application.

>>For instance, an operation might have a single character
>>string operand with non-negative integers as result as is
>>the case with the length operation. That operation is
>>certainly part of the character string type and arguably
>>part of the non-negative integer type. It is not part of
>>any algebraic structure. Or do I misunderstand something?

I think we more-or-less agree what constitutes type, regardless whether it is an algebraic structure.

>>Square root is part of the algebra for non-negative reals
>>and for perfect squares but not for integers. It is,
>>however, a valid operation on integers resulting in values
>>of a different type.

>>Division is not part of the algebra for any type that
>>includes zero as one of its values. Or is it?