Thu Sep 3 08:43:56 CEST 2009

Types vs. Staging vs. Abstract Interpretation

I'd like to know more about the formal relation between types and
abstract interpretation[1][3], and types and staging[2].  On an
intuitive plane it does seem reasonable to blur the 3 concepts: type
checkers / inference engines interpret programs in the compilation

Following some links I ended up here[4]. Frank Atanassow:

  ``Personally, I think the hits of the near future (ten or fifteen
    years) in the statically typed realm will be staged/reflective
    programming languages like MetaML, generic programming as in
    Generic Haskell and languages which support substructural logics
    like linear logic. I see opportunities for combining these in a
    powerful way to support lawful datatypes, i.e., datatypes which
    satisfy invariants in a decidable way. The underlying ideas will
    probably also pave the way for decidable behavioral subtyping in
    OO-like languages. A unified foundation for functional,
    procedural, OO and logic languages is also something I predict we
    will see soon. The aspect-oriented stuff will be probably sorted
    out and mapped onto existing concepts in current paradigms. (I
    don't think there is anything really new there.)

    Also, I think that in twenty years there will no longer be any
    debate about static vs. dynamic typing, and that instead most
    languages will instead provide a smooth continuum between the two,
    as people realize that there is no fundamental dichotomy
    there. Also languages will have more than one level of types: the
    types themselves will have types, and so on. But we will be able
    to treat types in a similar way to the way in which we treat
    values: we will be doing computations with them.

    There will be an increased emphasis on efficiency in the future,
    and I think we will see fewer aggressively optimizing compilers;
    instead it will be the programmer's job to write his programs in
    such a way that they are pretty much guaranteed to be efficient
    with any reasonable compiler. This sounds like a step backward,
    but it won't be because we will be better able to separate
    concerns of specification from implementation.

    (The reason I see more emphasis on efficiency is partly because I
    think that wearable computers and other small computers will
    become ubiquitous, partly because I think we will have the
    technology to do it when substructural logics invade static
    typing, and partly because we are starting to understand how to
    assign static type systems to low-level languages like assembly

[1] http://www.di.ens.fr/~cousot/COUSOTpapers/POPL97.shtml
[2] http://lambda-the-ultimate.org/node/2575
[3] http://lambda-the-ultimate.org/node/220#comment-1695
[4] http://lambda-the-ultimate.org/classic/message6475.html#6506