Notions of Type

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.

Thanks!

• Keith -- Fraud 6