3 ms·

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