Re: dual-language systems increase modularity

[Shriram Krishnamurthi <address@hidden>]

Grant Miner wrote:

> > - Have a deep understanding of types of all sorts, but aren't
> >   comfortable with them for reasons that'll take an hour to explain.
> 
> Would you mind expounding on that? :)
> Seriously...I'm interested.

Well, I was grossly exaggerating when I said it would take an hour --
exaggerating downwards, that is.  Types easily reward a few years of
study.  All I can do here is list some of the dimensions in the design
space of a type system:

- whether or not to permit union types
- whether or use inclusion or equality constraints
- whether or not to support polyvariance/polymorphism
- what semantics of recursive types to support
- whether to allow polymorphic recursion
- how to provide principal types
- how to provide principal typings
- many algorithmic complexity issues
- whether, and what kind of dependent types to allow

and these are just in the realm of ML-like languages.  Complicating
matters is the question of how to explain the type errors that these
increasingly complex type systems cough up.  And in the above list, we
haven't even really touched (except in a very weak way) on subtyping.

Note that this is just a list of the *themes* to consider.  It doesn't
even cover the *possibilities* under each theme (often more than two),
much less the subtle *tradeoffs* that represent each position, and not
at all the very subtle interactions between choices in each dimension.

Now, the discomfort some people experience with types is that, having
studied most or all of the above dimensions, and having taken into
account other needs (whether user-interface issues such as error
reporting or language constructs such as subtyping, mixins, recursive
modules, macros, etc), they don't find type systems that adequately
capture their needs.

If you want to learn the technical details behind some of the above
issues, you could look at Benjamin Pierce's recent book on type
systems.  Even that, however, will not fully expose you to all the
tradeoffs, but it will be a start.

Shriram