A shout out for LinearML

https://github.com/pikatchu/LinearML

Development kinda stopped after the author joined FB. Hoping for a revival.

Are there any languages that have dynamic typing but linear/affine memory management or C-style manual malloc+free? I reckon there would be some real productivity benefits in such a language if you wanted fast code with good C interop (Rust shows that affine types combined with destructors allows fantastic C interop) with faster development speed.

I'm a bit curious about combining RAII or similar with dynamic types myself. It's been discussed at mild length here: https://news.ycombinator.com/item?id=9356925

If we assume some sort of object orientation, or first class functions are available, affine types become (I think) impossible; If a value T with lifetime 'a is handed to a completely unknown method on an unknown object, or to an arbitrary lambda, we can't prove that the method will not destroy T in the middle of lifetime 'a. In otherwords, if typechecking is ruled out, we cannot do borrowchecking either.

I wonder how similar this linear logic is to other linear types language such as Rust, or the GHC paper recently shown here too.

Hmm, I thought Rust uses something like affine types [0] (which is similar to linear types).

[0] https://www.reddit.com/r/rust/comments/4mdgux/rust_and_affin...

Right, that's the kind of subtleties I wanted to understand.

Linear types = "you must use this value exactly one time" Affine (uniqueness) types = "you can use this value either zero or one times, but you can't use it more than once"

As an example, compare two languages: one with linear types and one with affine types. Let's say that you had a "File" type, a function "open()" that creates a file (either linear or affine as appropriate), and a function "close()" that consumes the file. Then this code would be legal in both languages with linear types and languages with affine types:

    let f: File = open()
    close(f)

Note that "f" is used once and only once, at which point the value is consumed. In a language with affine types, this is also kosher:

    let f: File = open()
    // Do nothing

This fails to compile in the language with linear types because "f" is never used. Finally, this code is never legal in either language:

    let f: File = open()
    close(f)
    close(f)

... because "f" is used twice here, and neither linear types nor affine types allow that.

So affine types give you a little more leeway.

So in this example when would you read or write the file?

Depends on the implementation of the language. In a typical functional language with linear types, the functions that mutate an object return a "new value" that is conceptually a modified version of the first value. So fleshing out our example:

    open : () -> File
    close : File -> ()
    write : (File, String) -> File
    let f: File = open()
    let new_f : File = write(f, "Hello world!\n")
    close(new_f)

If this seems clumsy or error-prone, notice that you can't accidentally close() f instead of new_f, and you can't forget to close() new_f, so there is actually very little room for error here.

Wild guess, this is monadic style friendly right ? threading implicit variables (rng, etc) is often used in tutorials.

Yep -- actually, if you look at how the IO type is defined in Haskell, it looks basically like this (there is an object that represents the "state of the world" that gets threaded through computations).

Alright. One distinction though is that vanilla IO monad has no logical constraint on consumption. You could technically thread a resource through a function many times and Haskell wouldn't complain. (This is blurry but I had something clear in mind, someone at a Haskeel meetup showed how to enforce constraints on monads through some kind of Phantom Type trick)

Given the importance of zero in mathematics to simplify a lot of things (see Roman numerals), my intuition is that affine types are much more flexible without losing the nice properties of linear types?

What kind of guarantees do you want from your type system? Strictly speaking the only guarantee that linear types give you is that every single linear value will be consumed at some point, which generally means that no resources ever get "leaked". If the idea of accidentally leaking a resource is unacceptable to you then you might find that affine types are too flexible, as languages that implement affine types generally give you some way to leak a value.

In practice I don't know if anyone is overly concerned about this. While Rust doesn't have linear types, I find you have to bend over backwards to introduce a situation where you might accidentally leak a resource.

Tarean makes a good point with respect to fusion, but "guaranteeing" fusion requires additional assistance from the compiler in addition to the basic implementation of linear types.

I never quite got the finer points but apparently affine types are great if you want to manage sharing in the presence of mutability and linear types are great if you want to guarantee fusion.

I see. Is the unused eliminated automatically on a later stage in the case of an affine type ?

Not sure what you're asking here. Usually the semantics behind what happens to an unused variable (i.e. is the file automatically closed, etc.) come down to how the language is designed. It could be automatically destroyed (like RAII in C++) or it could just be forgotten.

In a purely functional language with affine types, unused variables are usually just optimized out.