7 ms·
Lively Linear Lisp – 'Look Ma, No Garbage' (1991)
- agumonkey 10y agoI wonder how similar this linear logic is to other linear types language such as Rust, or the GHC paper recently shown here too.
- musicnarcoman 10y agoHmm, 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_affine_types_did_i_get_it_right/ https://www.reddit.com/r/rust/comments/4mdgux/rust_and_affin...
- agumonkey 10y agoRight, that's the kind of subtleties I wanted to understand.
- theseoafs 10y agoLinear 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.
- agumonkey 10y agoI see. Is the unused eliminated automatically on a later stage in the case of an affine type ?
- theseoafs 10y agoNot 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.
- jandrese 10y agoSo in this example when would you read or write the file?
- theseoafs 10y agoDepends 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.
- agumonkey 10y agoWild guess, this is monadic style friendly right ? threading implicit variables (rng, etc) is often used in tutorials.
- theseoafs 10y agoYep -- 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).
- srean 10y agoA shout out for LinearML https://github.com/pikatchu/LinearML https://github.com/pikatchu/LinearML Development kinda stopped after the author joined FB. Hoping for a revival.
- nonsince 10y agoAre 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.
- Solarsail 10y agoI'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 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.
- LfLxfxxLxfxx 10y agohttps://en.wikipedia.org/wiki/K_(programming_language) https://en.wikipedia.org/wiki/K_(programming_language)