Re: Notions of Type

From: Bob Badour <bbadour_at_pei.sympatico.ca>
Date: Thu, 17 Aug 2006 16:28:50 GMT
Message-ID: <6P0Fg.50703$pu3.588153@ursa-nb00s0.nbnet.nb.ca>

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.

>
> I was not able to find it. Either my search failed or I
> confused a statement by another as yours or I imagined it.
> My apologies. It was more a recollection that you had some
> insight into what type theory should have been, or how it
> could be improved, or how poor type theories had adversely
> affected the art of programming, or something like that.
> Hence my interest in further details.
>
>

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

>
> I don't think closure over a single type is a requirement.
> For example a Linear Algebra is an Algebra which is an
> Algebric Structure over two sets: a basis field and a
> vector space over that field. Wikipedia has:
>
> "an algebraic structure consists of one or more sets closed
> under one or more operations, satisfying some axioms."
>
> Hopefully someone can confirm this for us.

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.

>
> Well I definitely agree with you there that the type should
> include the set of all operations /defined/ on the values.
> However, as above I think algebras can accommodate closure
> over multiple sets and hence can include all operations
> defined.
>
> Now, I think before we disagreed about what /defined/ meant.
> I mean those operation signatures explicitly written, described,
> represented, or whatever in some symbolic language. Is that
> also your meaning? For example if I write only the following
> signatures for types V and K
>
> + : V V -> V
> - : V V -> V
> * : K V -> V
> * : V K -> V
>
> and no other signatures include V or K then the "entire set
> of operations defined on types V and K" is { + - * }.

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?

>
> In my view it is part of the algebraic structure. I certainly
> agree that it should be. The only question is whether my
> understanding of "algebraic structure" is correct.

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.

>
> I think that would be part of a larger algebra then. With
> domains and signatures such as:
>
> { N N^2 Z R*+ C ... }
>
> sqrt : R*+ -> R*+
> sqrt : N^2 -> N
> sqrt : Z -> C
>
> ...
>
>

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

>
> Division rings and fields (such as R) are considered
> algebraic structures. But I'm not clear on how one would
> express the signature for a division operator. This points
> to a useful property: when there is trouble expressing the
> algebraic structure there is a possibility of trouble in the
> computer. In this case exceptions, divide-by-zero, etc.
>
> -- Keith -- Fraud 6
>
Received on Thu Aug 17 2006 - 11:28:50 CDT