4 ms·

Can you give some examples of what it looks like to destroy a linear value? Elsewhere in the thread you said the compiler doesn't privilege destructor function

by _dain_ 4y ago

Can you give some examples of what it looks like to destroy a linear value? Elsewhere in the thread you said the compiler doesn't privilege destructor functions over anything else. I'm a bit confused how it works. The function to close a database connection has to take in a linear value for a database handle, but it returns nil. How do you actually get rid of the handle? And how does the compiler stop you from doing it incorrectly (or does it?)? --- Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program?

zetalyrae 4y ago
The idea is: linear interface, free core. Free types are the opposite of linear: they're unrestricted and can be used any number of types. For example: you can define a record type that contains only free values, but tell the compiler you want it to be linear. record Foo: Linear is x: Int32; -- machine-sized ints are free y: Int32; -- but `Foo` is declared to be linear end; Then instances of `Foo` behave like any other linear type. To destroy it, you'd destructure its contents: let foo: Foo := Foo(x => 10, y => 20); let { x: Int32, y: Int32 } := foo; So, how does this relate to safety? Because you can have something like: record File: Linear is ptr: Pointer[Nat8]; end; Where `File` is a linear record that contains a free (unsafe) file pointer. You can hide this behind an API, as an opaque type: module Filesystem is type File: Linear; -- `File` is opaque -- etc. end module. Opaque types can be imported from the outside, but clients don't know what they contain. So they can't construct them directly or destructure them or access record fields. Instead, you have to expose constructors and destructors in the API: module Filesystem is type File: Linear; function openFile(path: String): File; function closeFile(file: File): Unit; end module. The implementation of `closeFile` would simply be: function closeFile(file: File): Unit is let { ptr: Pointer[Nat8] } := file; fclose(ptr); -- FFI-defined function return nil; end; >Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program? Borrowing allows you to relax the linearity constraints for some time: https://austral-lang.org/tutorial/borrowing https://austral-lang.org/tutorial/borrowing
- _dain_ 4y ago
  Ah great! So to summarize: - we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it - we can make a type opaque to importers of our module, which precludes direct destructuring by the user - the compiler forces the user to eventually destroy the linear value - therefore the user must call our cleanup function And it's our responsibility to ensure the function implements the correct cleanup logic.
  - zetalyrae 4y ago
    Yes, that's correct >we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it I think I'll borrow this for the tutorial because it's very succinctly put.
    - all_factz 4y ago
      Trying to understand: what’s to prevent someone from calling an FFI-defined function on a free type without going through the whole linear types rigmarole? E.g. could I call `fopen` and `fclose` directly to circumvent the whole `File` interface? I’m sure there’s a good answer. This is a really cool and impressive project. EDIT: Ah, just got to the section on "The FFI Boundary". Makes sense!
deleted 4y ago
[deleted]

by _dain_ 4y ago

zetalyrae 4y ago

The idea is: linear interface, free core. Free types are the opposite of linear: they're unrestricted and can be used any number of types. For example: you can define a record type that contains only free values, but tell the compiler you want it to be linear. record Foo: Linear is x: Int32; -- machine-sized ints are free y: Int32; -- but `Foo` is declared to be linear end; Then instances of `Foo` behave like any other linear type. To destroy it, you'd destructure its contents: let foo: Foo := Foo(x => 10, y => 20); let { x: Int32, y: Int32 } := foo; So, how does this relate to safety? Because you can have something like: record File: Linear is ptr: Pointer[Nat8]; end; Where `File` is a linear record that contains a free (unsafe) file pointer. You can hide this behind an API, as an opaque type: module Filesystem is type File: Linear; -- `File` is opaque -- etc. end module. Opaque types can be imported from the outside, but clients don't know what they contain. So they can't construct them directly or destructure them or access record fields. Instead, you have to expose constructors and destructors in the API: module Filesystem is type File: Linear; function openFile(path: String): File; function closeFile(file: File): Unit; end module. The implementation of `closeFile` would simply be: function closeFile(file: File): Unit is let { ptr: Pointer[Nat8] } := file; fclose(ptr); -- FFI-defined function return nil; end; >Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program? Borrowing allows you to relax the linearity constraints for some time: https://austral-lang.org/tutorial/borrowing https://austral-lang.org/tutorial/borrowing

_dain_ 4y ago
Ah great! So to summarize: - we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it - we can make a type opaque to importers of our module, which precludes direct destructuring by the user - the compiler forces the user to eventually destroy the linear value - therefore the user must call our cleanup function And it's our responsibility to ensure the function implements the correct cleanup logic.
- zetalyrae 4y ago
  Yes, that's correct >we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it I think I'll borrow this for the tutorial because it's very succinctly put.
  - all_factz 4y ago
    Trying to understand: what’s to prevent someone from calling an FFI-defined function on a free type without going through the whole linear types rigmarole? E.g. could I call `fopen` and `fclose` directly to circumvent the whole `File` interface? I’m sure there’s a good answer. This is a really cool and impressive project. EDIT: Ah, just got to the section on "The FFI Boundary". Makes sense!

deleted 4y ago

[deleted]