Hacker News Reader

Comment by beders | Hacker News Reader

I'm missing something on the discussion of correctness for Linear types:

     let file: File := openFile("test.txt");
     writeString(file, "Hello, world!");
     g(file);

If I have any other function 'g' that takes a File and returns Unit, wouldn't the compiler be ok with that. Now I have a dangling file pointer.

View on HN

AFAICT the compiler would forbid to use `file` after the `writeString(file)` line, because it has been consumed.

You can get something like affine types out of the linear types constructed this way, by returning new one-time value every time when operations on an object can continue:

  let file_1: File := openFile("test.txt");
  let file_2 := writeString(file_1, "Hello, world!");
  g(file_2);

Linear typed are "use exactly once". In this case you consume "file" when you pass it into writeString and then it is (compile time) unavailable to be used with g, afterwards.

looks like if Zig and Golang had a child. But I would expect something like file.writeString()

yes, I mistyped. I wanted to take the File object from writeString

    foo = writeString(file, "Hello world!");
    g(foo);

`g` still has to make `foo`, the new handle for `file` disappear.

I guess the question is around. If the File library can implement `fn CloseFile(f: File) -> ()`, why can't I implement `fn g(f: File) -> ()`?

At least I should be able to do so using `File::CloseFile` underneath, but what guarantees that only the module defining a type can define sinks for it?

I guess this is an implicit restriction that isn't talked in depth. It should be fine to add sources and sinks to a linear type, but only if they are implemented through the module's own sources and sinks.

A function like `closeFile` will consume the linear value but not produce a new linear value - it returns `Unit`. It does this via a destructuring assignment (For example, File would be a record type with a field named handle).

    function closeFile (file : File) : Unit is
        let { handle } := file;    (* This consumes the file *)
        fclose(handle);
        return nil;
    end;

A module will usually provide opaque types, with the actual definitions encapsulated by an implementation file, similar to how C and C++ do it. Users of this library don't know what is in the type `File`, so they're unable to use the destructuring assignment themselves - so their only option is to call `closeFile`, or the compiler will complain that the linear value is not consumed.

You can of course, call `closeFile` from `g`, and then it's fine to make `g` return Unit.

    function g (file : File) : Unit is
        let file0 := (* do something with file *);
        return closeFile(file0);
    end;

The compiler actually enforces this. If g takes a `file` argument and returns Unit, then it MUST call `closeFile`. Failure to do so won't compile.

For a real example, check how the RootCapability type is defined in `builtin/Pervasive`[1]. It's declared as an opaque type in the .aui file, along with `surrenderRoot`. This is all the user of the type knows about it.

    type RootCapability : Linear;

    function surrenderRoot(cap: RootCapability): Unit;

In the .aum file both the type and surrenderRoot are actually defined.

    record RootCapability: Linear is
        value: Unit;
    end;

    function surrenderRoot(cap: RootCapability): Unit is
        let { value: Unit } := cap;
        return nil;
    end;

[1]:https://github.com/austral/austral/tree/master/lib/builtin

g also has to use file exactly once

Reply on news.ycombinator.com