Typing system vs. Java

[Michael Abbott]

[posted and mailed]

Alex, I'd like to say more in response to your very interesting message 
below, but it's difficult to know where to begin.  I agree wholeheartedly 
with your sentiments, but I'm wondering if you're aware of just how 
difficult what you're describing is to achieve!?

For example, there is a type system known as Coq (http://coq.inria.fr/) 
which uses a type system similar in spirit to what you describe (but Coq is 
oriented towards the automation of formal mathematical proofs).  Coq is 
based upon dependent types, and demonstrates that type checking of the sort 
you are talking about is, in principle, at least as difficult as solving an 
arbitrary mathematical problem!  Also, it has to be said that expressing 
mathematics in Coq is *very* hard work (formalising the "fundamental 
theorem of algebra", ie, the result that polynomials over C have roots, was 
worth several PhDs recently).

I also remember a recent language in a similar spirit (don't have the 
reference to hand) where a two-level language was developed: one level for 
expressing programs, the other level for expressing assertions about 
programs (and building proofs of those assertions, if I recall correctly).  

I'm of the opinion that work on dependent types is the way forwards, but 
there are some big (gigantic?) obstacles to be overcome first...


"Alex Martelli" <aleaxit at yahoo.com> wrote in 
news:9kb8mq02bd2 at enews1.newsguy.com:

> "Christian Tanzer" <tanzer at swing.co.at> wrote in message
> news:mailman.996682083.19421.python-list at python.org...
>     ...
> """
>> Back to Python -- programming in Python has always felt to me a *LOT*
>> like generic programming 
> 
> Yup. Only, in Python it's very implicit.
> """
> ...just about as in C++, except more so:-).
> 
> 
> """
> The nice thing about Ada and Eiffel generics is that the requirements
> on the generic parameters are spellt out explicitly. For most
> """
> The problem with Ada and Eiffel generics is that the requirements
> on the generic parameters are to be spelled out explicitly.  Type
> inference (as in Haskell) or signature-based polymorphism (as in
> C++ templates and in Python) is smooth indeed (although the ability
> to state out loud what you think the compiler will infer, if it
> could be done without really adding any significant complexity,
> would be a nice extra).
> 
> The issue from my POV is: what defines "a type", except the
> signatures of that subset of its interfaces that a given generic
> component is actually using?  Presumably the programming-as-
> contracting preconditions/postconditions/invariants on those
> interfaces -- but those are *runtime*-checked, and even that
> hardly catches a significant portion of the "type semantics".
> 
> Consider the issue of: what predicate-parameter P can I pass to
> a generic such as C++'s std::sort.  Of course, I have some
> signature constraints -- P(x,y) must be callable for certain
> x and y and return something usable as a boolean value; C++
> catches errors about this at compile-time, while Python, if
> I try calling mylist.sort(unsuitableP) where unsuitableP is
> not callable with two parameters that are items of mylist,
> will only catch it at run-time.  Having the check happen at
> compile-time gives me the error diagnostics slightly earlier
> (5 to 10 minutes, if I use a sensible testing policy) AND
> makes it easy for C++ to generate stupendous code (if P is
> inline or can be inlined).
> 
> But that barely scratches the surface!  The REAL conditions
> that define the type of P are:
>     not P(x,x) for any x
>     P(x, y) implies not P(y, x) for any x, y
>     P(x, y) and P(y, z) implies P(x, z) for any x, y, z
> Note the universal-quantifier 'any' liberally used here:
> it's not something quaint and peculiar, it's TYPICAL of
> real type-constraints, making them uncheckable in the
> general case, even at runtime (much less compiletime).
> 
> THIS is the kind of thing I'd really like to express in a
> compiler-usable way!  THIS is the kind of thing that would
> make my programs MUCH clearer to human readers, and really
> get mileage out of type-checking.  What, if anything, the
> compiler is able to do with such a hypothetically formalized
> expression of my real design intentions is a minor issue.
> 
> If *sometimes* a runtime check (or, joy!, even a compile
> time one, saving me several precious extra minutes) can be
> inferred from such type-constraints (maybe only in some
> kind of debug-mode, if, as likely, checks would burden
> the program), then great.  If *sometimes* the compiler is
> able to optimize away some computation by *relying* on my
> assertions, then super (maybe only in some kind of optimize
> mode, if, as likely, it would slow down compilation a lot).
> 
> But existing languages appear to me to have things
> backwards.  They *start* from what they'll be able to
> check, and/or able to exploit for optimization, and
> use THAT criterion to decide what subset of my design
> intentions I'm allowed (or, more often, required) to
> formally express in the language.
> 
> That's like the drunkard looking for his keys under
> the streetlamp, even though he knows he's dropped them
> at the other end of the road, because it's too dark
> over there...:-).  A language should let me say what
> I mean, and do of that what it can.  Compilers and
> supporting tools do evolve, old applications tend to
> live forever; basing what a language lets me express
> (or forces me to express) on today's compiler and
> tool technology is back-asswards.
> 
> Given the incomplete and unsatisfactory state of the
> way various languages let me (or rather force me to)
> express my design intentions, I'd rather do away with
> all the complexity, and just use Python (or C++
> templates).  Give me an URL to a usable language that
> lets me express the most basic typing constraints,
> such as symmetry or antisymmetry, reflexivity or
> antireflexivity, and transitivity, as above, and I'll
> be more than happy to give it a try.  But Ada, Eiffel,
> C++ (what it DOES do for typechecking), Java, and,
> sigh, even Haskell, don't really cut the mustard today.
> Therefore, Python's *simplicity* wins the day, as
> you say...:
> 
> """
> application areas, Python still wins hands down, though.
> """
> I agree, but I hope you can now better see WHY I do
> so fully agree.  Complication must bring a payoff that
> offsets its undeniable costs.  Today's type-checking,
> as applied in the above-listed languages, doesn't, in
> terms of useful earlier-detection of errors -- it's
> little use to find out about an error 10 minutes
> earlier, if it takes me 15 more minutes to write the
> code snippet because of extra language complication.
> Most interesting checks happen at runtime if at all,
> and in fact most important properties can't even be
> stated formally in the languages, because of a lack
> of existential and universal quantifiers.
> 
> Today's typechecks DO help hugely in terms of
> optimization, even though Self, the Scheme compiler
> stalin, and good Common Lisp compilers all prove
> that static typing is nowhere near a NEED to get
> such optimizations, that type inference even in
> a hugely dynamic language can get there too.  But
> C++'s generics are an excellent example of the way
> lack of type-constraint declaration in no way
> inhibits type-based optimization -- given signature
> based polymorphism, type-inference in any actual
> instantiation of a generic IS pretty trivial:-).
> 
> 
> Alex
> 
> 
>