Re: Notions of Type

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.

> 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 { + - * }.

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

> 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