Idris 2: Quantitative Type Theory in Practice

Re:Idris 2: Quantitative Type Theory in Practice by phlip9 on Monday January 24, 2022 @12:29PM (#30060866)

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/...). 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)

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).

[ Parent | on HN ]

Re:Idris 2: Quantitative Type Theory in Practice by dwohnitmok on Monday January 24, 2022 @05:43PM (#30065127)

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.

[ Parent | on HN ]