Showing posts with label statically typed. Show all posts
Showing posts with label statically typed. Show all posts

Thursday, July 5, 2012

What is the ML Module System?, Part 1

Browsing through the heated Scala mail list discussion from 2009 on OOP versus functional programming, I ran into a number of messages which indicate some confusion as to the role and mechanism of the ML module system. The natural question that was raised is how is a module system different from a "low-level" object system. I am not entirely sure what a "low-level" object system is but in this post I would like to compare and contrast the ML module system and object systems, principally class-based object system but also classless object systems. First, what role do these language features serve? There is some overlap in purpose but also significant differences. The ML module system was originally designed to serve to roles:

  1. To support programming-in-the-large organization of large system architecture
  2. To facilitate the construction of a type-safe container library
In contrast, OOP is typically defined as supporting design goals of encapsulation, inheritance, and subtype polymorphism. On the surface, this suggests some overlap. Programming-in-the-large may sound like encapsulation, but as I will discuss, the reality is considerably more nuanced.

Wednesday, December 7, 2011

Substructural Type Systems and Performance, Part 1

Why is the name of this blog "substructural"? In turns out that in the realm of advanced type systems, there is a family of type systems derived from a family of logical systems called substructural logics. The chief distinction of substructural type systems is that one or more of the "structural properties" of type environments are eliminated. These rules are exchange, weakening, and contraction. Exchange allows arbitrarily reordering bindings in the type environment. Weakening enables adding new bindings. A type derivation is deemed "weakened" in the sense that if a program already typechecks using a certain type environment, adding new bindings to that environment won't negate the well-typing of the program.

Tuesday, November 22, 2011

Static Type System and Numerical Computing

The programming languages with which most people are familiar, such C/C++, Java, Python, JavaScript, and Ruby, presents a very stark contrast. On the one hand, you have statically typed languages (C/C++ and Java) which are amenable to a wide assortment of compile-time optimizations due to the presence of types. On the other, you have dynamically typed languages (Python, JavaScript, and Ruby) which are "fun" to program and amenable to rapid prototype due to more succinct syntax partly due to the absence of explicit type annotations. The sweet spot, in my humble opinion, is statically type but with type inference, a subject of my expertise and doctoral studies. I plan to write a few posts on this subject, near and dear to my heart. Heavy duty Numerical computing is one area where dynamically typed languages such as Matlab, R, and NumPy/Python have gained a considerable mindshare. Since NumPy offloads computations to efficient C libraries, this is quite reasonable. I would like to discuss where I think numerical computing and statistical analysis programs can benefit from a more sophisticated static type system with type inference. To whet your appetite, consider the case that C++'s Boost Library contains the functionality needed to statically check for units (i.e., dimensional analysis). The performance difference between code generated from statically typed languages and from dynamically typed languages is not just the absence of dynamic type checks. Types in static type systems enable a considerable array of optimizations to get rid of that last tiny ounce of latency.