Re: Notions of Type

From: Bob Badour <bbadour_at_pei.sympatico.ca>
Date: Wed, 16 Aug 2006 21:50:57 GMT
Message-ID: <5rMEg.49122$pu3.577728@ursa-nb00s0.nbnet.nb.ca>

Keith H Duggar wrote:

> Bob Badour wrote:
> 

>>JOG wrote:
>>
>>>I still want to convince people of what I've learned -
>>>while your 'cut the crap' posting style has grown on me
>>>a lot, it doesn't seem to do that.
>>
>>One will never reach those who have no motivation to learn
>>and every motivation not to. That said, I have had my
>>share of successes among those who remain.

> 
> 
> Sorry for this topic shift but that reminded me of something
> specific I still would like to learn from you. I think maybe
> my question may have slipped through the cracks. Here is the
> excerpt from "What Databases Have Taught Me"
> 
> Keith H Duggar wrote:
> 

>>Bob Badour wrote:
>>
>>>Because computing science, in a sense, is the process of
>>>building abstract machines and formalisms, the fact that
>>>one can axiomatize is very useful. The fact that one can
>>>arbitrarily choose different axiomatizations is useful
>>>too.
>>
>>Ok. So it seems we agree that axiomatization is useful. I
>>think I should have just simply said from the start that the
>>definition of "type" that I currently find most useful in
>>programming is "type = algebraic structure". Now, I can't
>>remember if algebraic structures are permitted to have an
>>unlimited number of sets, operations, and axioms. If they
>>are then let me append "with a limited number of sets,
>>operations, and axioms" to the definition.
>>
>>Which definition(s) [or notions] do you find more useful?
>>Or what is it about the algebraic structure definition
>>that you find not useful or insufficient?
>>
>>I recall once you mentioned type theory had failed in some
>>manner. Can you elaborate? Do you know of any alternatives
>>or recent work in type (or category) theory that is doing
>>better and is more useful to computer science?

> 
> 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. 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.

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?

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?

Other than possibly the _Principle of Cautious Design_, I can think of no immediate objection to a type where the set of operations in the algebra is empty. On the other hand, it might be difficult to devise such a type that has any use. Received on Wed Aug 16 2006 - 16:50:57 CDT