3 ms·

I'm missing something on the discussion of correctness for Linear types: let file: File := openFile("test.txt"); writeString(file, "Hello, world!");

• tupshin 2y ago
  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.
• nine_k 2y ago
  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);
• beders 2y ago
  yes, I mistyped. I wanted to take the File object from writeString foo = writeString(file, "Hello world!"); g(foo);
  • dietr1ch 2y ago
    `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.
    • sparkie 2y ago
      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 https://github.com/austral/austral/tree/master/lib/builtin
• sweeter 2y ago
  looks like if Zig and Golang had a child. But I would expect something like file.writeString()
• assbuttbuttass 2y ago
  g also has to use file exactly once
  • deleted 2y ago
    [deleted]