Home » forums » LtU Forum

Blending static and dynamic typing

Oleg has an interesting piece that I haven't found mentioned on LtU (though it dates from 2000):

Blending static and dynamic typing: Scheme programming in ML

We show several examples of writing ML (OCaml) code in the style of Scheme programs, taking the fullest advantage of latent typing and placing no type annotations. The ML code features:

  • intentionally polymorphic functions: Scheme display
  • lists of variously intentionally typed elements
  • functions with a variable number of polymorphic arguments: *
  • self-application combinator
  • higher-order polyvariadic intensionally polymorphic function: Scheme for-each

[...]

The code is trivial -- and that is the point. Defining and using the Universal type in a statically typed language is indeed embarrassingly easy. The code has not a single type annotation, and looks as dynamically typed as Scheme code. The source language is still OCaml, with static typing present and available to the programmer. Thus ML offers a blend of dynamic and static type programming; it's a programmer who chooses the proportions of this blend.

(disclaimer: I'm not posting this to start another religious battle, but as an interesting example)

By dbfaken at 2007-03-08 17:05 | LtU Forum | previous forum topic | next forum topic | other blogs | 5790 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

imperfect blend

In some of the old typing discussions, we discussed this style, even if we didn't reference this particular article. I think it's a stretch to say that the code "looks as dynamically typed as Scheme code". In some places, that's true. In other places, it looks more like the output of a compiler from Scheme code to a typed language [i.e. a typed AST representation], because of the need for type constructors and the explicit use of an apply function.

By Anton van Straaten at Thu, 2007-03-08 17:45 | login or register to post comments

HW assignment based on this kind of embedding

In the undergrad PL course at CMU, we have used this kind of embedding to illustrate product, sum, and recursive types. Specifically, students compile a dynamically typed language by embedding it into a simply typed lambda-calculus with product, sum, and recursive types.
This makes all the run-time tag tests explicit, so it is easy to talk about optimizations like eliminating tests on values whose tags are readily apparent (which is just beta-reduction in the compiled code).

If you're curious, the assignment handout explains the compiler in more detail (warning: this link will not persist after this semester). The target of the compilation is a standard STLC with products, sums, and recursive types; see the course text for more details.

By Dan Licata at Thu, 2007-03-08 19:24 | login or register to post comments

Re: imperfect blend

Anton van Straaten wrote:
In other places, it looks more like the output of a compiler from Scheme code to a typed language [i.e. a typed AST representation], because of the need for type constructors and the explicit use of an apply function.
In the `pure Scheme' user code, the type constructors occur only by the literals. One may abbreviate Str to S, List to L, Int to I and write L[ S"string"; I(1); L[]]. We then declare S"..." to be the syntax of string literals, etc. Incidentally, it seems that ocamlbuild took exactly that approach. (Only instead of S"..." they use A"..." and instead of L[...] they use S[...]). The example of an ocamlbuild plug-in is quite illustrative. Because the type tags can be regarded as part of the literal syntax, camlp4 can make the syntax prettier, if so really desired.

As to the use of s_app: well, one could have used a shorter name and make it infix. Incidentally, because the meta-language is still typed, if we by accident omit s_app, we immediately get the type error. Like in Scheme, one may write s_app I(1) L[S"x"]; if that piece of code never gets executed, there is no error. But one may not write I(1) L[S"x"], because that is an invalid object level expression. A bit informally speaking, OCaml typechecker enforces the syntax of the embedded dynamic language...

By Oleg at Fri, 2007-03-09 00:44 | login or register to post comments