3 ms·

I was a bit disappointed with linearity in QTT as I couldn't figured out how to create a safe API around a resizable array. The example given in the paper is a

by phlip9 5y ago

I was a bit disappointed with linearity in QTT as I couldn't figured out how to create a safe API around a resizable array. The example given in the paper is a LinArray (https://github.com/idris-lang/Idris2/blob/main/libs/contrib/Data/Linear/Array.idr https://github.com/idris-lang/Idris2/blob/main/libs/contrib/...). Unfortunately, as the community discovered, a user can "leak" a non-linear binding outside of the `newArray` constructor (which is what attempts to enforce linearity for all bindings). With multiple unrestricted handles, a user can accidentally double-free for instance. (https://github.com/idris-lang/Idris2/issues/613 https://github.com/idris-lang/Idris2/issues/613) The fundamental issue in this case is that linearity in QTT is a property of the parameter bindings and _not_ the type itself, meaning we can't easily express linearity as a _global_ property of the type. On the other hand, only affecting the parameter bindings makes it really easy to use runtime-erased/comptime stuff without reimplementing a bunch of common types as runtime- and comptime-only versions. ATS chooses the other path and makes linearity and runtime-erasure a part of the type (not without paying a hefty syntactic cost however).

dwohnitmok 5y ago
I thought I'd read over `Data.Linear.Array` before, but maybe not? My intuition for linear types would be that for any function that uses the array you basically almost always want to return a pair of the value and new linear version of the array (i.e. `Res a (const (arr t))`). The only exceptions are a set of "terminal" operations that convert it to a non-linear type (in this case probably the things that end up returning an `IArray`). So I'm a bit confused why e.g. `read` is `(1 _ : arr t) -> Int -> Maybe t` and not `(1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))`. But also isn't the `newArray` fixed by just rewrapping the output? data Unrestricted : Type -> Type where MkUnrestricted : a -> Unrestricted a newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> Unrestricted a) -> Unrestricted a -- You'll need this if you actually make use of the outer linear multiplicity -- in the function argument to newArray -- which is also why newArray returns Unrestricted useUnrestricted : (1 _ : Unrestricted a) -> (a -> b) -> b useUnrestricted (MkUnrestricted x) f = f x This is e.g. how Linear Haskell does it. The unrestricted multiplicity of the argument to `MkUnrestricted` prevents the bug here by only allowing you to output non-linear things (so it rejects wrapping the linear input in `MkUnrestricted`; you have to first convert it via a terminal operation into something else). The entire `Data.Linear.Array` seems to be in need of a once-over unless I'm misunderstanding something. EDIT: Never mind, reading too quickly, I see the mread now that has the signature I'd imagine it should.

by phlip9 5y ago

dwohnitmok 5y ago

I thought I'd read over `Data.Linear.Array` before, but maybe not? My intuition for linear types would be that for any function that uses the array you basically almost always want to return a pair of the value and new linear version of the array (i.e. `Res a (const (arr t))`). The only exceptions are a set of "terminal" operations that convert it to a non-linear type (in this case probably the things that end up returning an `IArray`). So I'm a bit confused why e.g. `read` is `(1 _ : arr t) -> Int -> Maybe t` and not `(1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))`. But also isn't the `newArray` fixed by just rewrapping the output? data Unrestricted : Type -> Type where MkUnrestricted : a -> Unrestricted a newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> Unrestricted a) -> Unrestricted a -- You'll need this if you actually make use of the outer linear multiplicity -- in the function argument to newArray -- which is also why newArray returns Unrestricted useUnrestricted : (1 _ : Unrestricted a) -> (a -> b) -> b useUnrestricted (MkUnrestricted x) f = f x This is e.g. how Linear Haskell does it. The unrestricted multiplicity of the argument to `MkUnrestricted` prevents the bug here by only allowing you to output non-linear things (so it rejects wrapping the linear input in `MkUnrestricted`; you have to first convert it via a terminal operation into something else). The entire `Data.Linear.Array` seems to be in need of a once-over unless I'm misunderstanding something. EDIT: Never mind, reading too quickly, I see the mread now that has the signature I'd imagine it should.