Gradual Typing consequences?

A lucid and clear analysis of the current situation of gradual-typing: https://blog.sigplan.org/2019/07/12/gradual-typing-theory-practice/

It explains why gradual typing spread so well, the type system ideas they have invented or improved to support some of the many unusual ways dynamic language programmers use their languages, why some of the basic purposes of gradual typing (type soundness) are currently under-developed in practice, and how this problem could be solved in future.

One thing it doesn’t discuss is if and what kind of effect and consequences all this world of gradual typing will have on statically typed languages, like Rust. Do you have ideas?

I expect that (as it usually happens) programmers that have used gradual typing a lot will start asking for some of those new type system tricks in statically typed languages too, but most of such gradual typing handy features look unfit for statically typed languages.

1 Like

C# dynamic is a kind of gradual typing. If this approach is applied to Rust, the runtime has to implement the rather heavy trait-solving algorithm, which at least requires a lot of work.

That being said, it is joyful to imagine what semantics dynamic have. Especially with Rust’s unique affine types and lifetime system. Another thing is unsized lvalues are required.

Edit: more thought

Affine type itself can be implemented as having a “dropped” state and accessing this state is a runtime error.

Dynamic borrow checking probably be similar to MIRI currently being developed.

Gradual typing is mainly to support transitions from untyped languages like JavaScript to TypeScript.

If start with a properly designed language with a type system and type inference, there’s no need for “gradual typing”.

At most there could be an argument for allowing global type inference in Rust (i.e. omitting and inferring static, function return, parameter and struct/enum field types) during development.

2 Likes

While this may be the case with industry applications of gradual typing, where all types are effectively gone at runtime and only exist for the benefit of static tooling, this doesn’t have to be the case.

The article in the original post covers a lot of the theory of gradual typing, and benefits of using it on a typed runtime as opposed to untyped/monotyped.

Gradual typing doesn’t have to mean static type annotations on a dynamic runtime, and it doesn’t need to mean dynamic runtime capabilities inside a static system (like C# dynamic). There’s lots of space to learn from if you allow it to be more than a way to add partial type coverage to an untyped code base.

I found a problematic case with type inference.

struct X;

impl X {
    fn get<T: Default>(self) -> T {
        T::default()
    }
}

fn main() {
    let x = X;
    let y = x.get();
    let z: i32 = y;
}

This works fine. But if x and z's type are dynamic, what is the type of y? This example demonstrates the difficulty of preserving the important property of gradual typing “a well-typed program is given and change every type to dynamic then it should works the same”.

This. And in my experience, in TypeScript/JavaScript as well as in various other implementations (Python’s mypy comes to mind), this is very apparent, in a negative way. All of the gradual typing systems I’ve used so far feel like they are just bolted onto a dynamically-typed language, because the idioms of said dynamically-typed language don’t really change, and these in turn just don’t play nicely with real, up-front, well-designed static typing.

“You can’t pass a string where a number is expected” is great, but it’s not the ultimate static guarantee, and basically anything more sophisticated ends up being painful. Consequently, people tend to give up fighting a badly-designed type system, and resort to Any (or the equivalent) whenever they don’t find an easy way out.

Bottom line: I don’t think true statically-typed languages are going away anytime soon, nor do I think that any static-from-the-origins type system needs the sloppy escape hatch that is gradual typing.

6 Likes

I have thought about gradual typing for static languages a tiny bit, mostly in regards to migrating a code base over to a type and effect system, and exporting functions which are inexpressible in the weaker language to it.

But it does seem like gradual typing should work whenever you move from a weaker to a stronger language in the lambda cube. But I haven’t looked around to see if anyone has tried to do so yet, not gotten into the details.

For the opposite perspective, I work in C# and every time someone uses dynamic it causes unexpected problems. Serialization breaks, memory leaks in the runtime, all kinds of badness.

The core problem with gradual typing seems to be that it requires a full dynamic- or reflection-enabled runtime underneath, while actually making performance worse than just using that directly. I don’t see any good way of incorporating that into Rust without losing most of what makes Rust special.

I think I’d be more interested in things that allow structural features and anonymous types, or similar – imagine, perhaps, a structural trait that lets you accept anything with public x and y fields in your 2D math library.

4 Likes

Similarly, working in TypeScript can be great, and I do occasionally miss some of its type system features… but none of them have to do with the fact that the type system is gradual. The bits I miss are its structural typing (including untagged unions, though when working in TS I profoundly miss tagged unions: really I want both!) and its—limited, but extremely useful—ability to refine/narrow types based on control flow.

After more thoughts, I agree that C# dynamic approach is a bad idea.

Another gradual typing approach is zero-cost dependent types. ATS is where I got idea from. I just read the tutorial but if I’m correct, “dataview” can be used such as “this structure represents a valid doubly linked list” with no run-time cost.

I consider ad-hoc / structural interfaces a feature of gradual typing as well.

I think most of what a strictly typed language can learn from gradual typing (at this time) is that structural typing (as opposed to nominal typing) definitely has its use cases as well, and should be supported where possible.

3 Likes

Rust does have a modicum of structural typing: tuples and parameterisation of generics.

1 Like

I think refinement types address this. If you need gradual typing, then implement the type’s full range as an enum, but restrict down over time.

Anything else requires some downcast method for trait objects I’d think.

I’ll note that refinement types, if done well, should also improve formal verification efforts and make safer interfaces’s possible.

Also, refinement types would superced the repeated requests for a let .. else feature, well by itself a let .. else sounds unworkable.