Language with extensible type system?

Question

Is there a practical programming language that has an extensible type system? Or alternatively, an add-on type system that can be used with existing languages?

With extensible I mean that the typing rules are specified externally and can be changed by the user without rewriting the typechecking code.

The use would be to add additional checkable constraints to a program (for example physical dimensions, uniqueness types, reference frames, nulled memory etc.).

In the programming language part, one would annotate the expressions with their types:

    import units # library for physical units
    # x has type float and the type meter
    x:{float,units.meter}
    y:{float,units.meter**2}
    def f(x): return x*x
    y=f(x)

(I am using Python as an example language as the semantics are independent of the optional type annotations, but any language would do)

In the above case x has multiple types: float and a physical dimension. Each of those have different typing rules, and it makes sense to treat them differently. In the units type library, we would provide typing rules of the following form (assuming that the rules for float are defined elesewhere): $$\frac{\Gamma \vdash x:Meter, n:Nat, m:Nat}{\Gamma \vdash x^\frac{n}{m}:Meter^\frac{n}{m}}$$

While for example physical dimensions can be dealt with through a runtime library somewhat unsatisfactorily, doing dimensional analysis with the tools of types is much more elegant, doesn't incur any runtime overhead and proves dimensional correctness.

For example, the only mainstream language that I am aware of that provides physical dimensions is F#, but unfortunately it is broken as it does not support fractional exponents https://stackoverflow.com/questions/11333135/fractional-power-of-units-of-measures-in-f/11334159#11334159 Providing the physical dimensions as a typing library instead of a language internal would allow the user to fix this problem and add other dimensional systems, like directional units or Siano's orientational dimensions.

The annotated AST and the typing rules would be processed by a constraint solver to issue type errors and warnings for insufficiently typed expressions.

Why am I asking for this?

1. It would be great for understanding type systems
2. Existing software could be made more secure by adding extra type constraints.

Answer 1

There's support for extensible type systems in JetBrains MPS (http://www.jetbrains.com/mps/). Basically it has a constraint solving engine which supports both equations (type equalities) and inequalities (subtyping). Extensions add new rules of adding constraints which are solved by the engine.

P.S. I think the question is more appropriate for stackoverflow than cstheory.