Make linear+session types real

[rrnewton]

This will be a major step up in assurance for the compiler internals. The core cursorizing transform is really so complicated and error prone that it warrants it.

I won't describe the technique here. Read the paper for more details..

P.S. Note that if this were implemented in a type-indexed, Accelerate style, we could consider doing it at the host type-system level, and thus verifying that our compiler passes correctly handle cursors for all inputs. That's a lot of work, though. It would probably happen in an inverted version of the technique described in the ghostbuster paper. You would need to go to an indexed representation, do the verified transform, and then drop back down. Either that or refactor the whole compiler. But we have generally felt that that provides too high a cost/benefit ratio. Perhaps there are lighter weight (static) verification techniques... In the meantime, the more dynamic testing approach in this issue should do quite well.

[rrnewton]

Important point -- will this just be for L2, or also for L3 / Target language?

[vollmerm]

It makes sense to extend the existing typechecker for L2 first. We could also add a typechecker for L3, potentially, but some of the information we need for checking might be gone by then.

[vollmerm]

@rrnewton: I ended up giving up on doing inference in the type checker, but it's probably possible to do.

Instead I modified RouteEnds and Cursorize to add Has(...) types, and it seems to work on simple tests.

For example, this is the "Node" case from sum-tree:

("Node",
 ["cursIn24"],
 LetE ("x3",
       PackedTy "CURSOR_TY"
                ()
                (HasCur [PackedTy "Tree" () NoneCur,
                         PackedTy "Tree" () NoneCur]),
       VarE "cursIn24")
      (LetE ("hoistapp17",
             ProdTy [PackedTy "CURSOR_TY"
                              ()
                              (HasCur [PackedTy "Tree"
                                                ()
                                                NoneCur]),
                     IntTy],
             AppE "sum_tree" (VarE "x3"))
            (LetE ("end_x3",
                   PackedTy "CURSOR_TY"
                            ()
                            (HasCur [PackedTy "Tree"
                                              ()
                                              NoneCur]),
                   ProjE 0 (VarE "hoistapp17"))
                  (LetE ("y4",
                         PackedTy "CURSOR_TY"
                                  ()
                                  (HasCur [PackedTy "Tree"
                                                    ()
                                                    NoneCur]),
                         VarE "end_x3")
                        (LetE ("fltPrm5",
                               IntTy,
                               ProjE 1
                                     (VarE "hoistapp17"))
                              (LetE ("hoistapp19",
                                     ProdTy [PackedTy "CURSOR_TY"
                                                      ()
                                                      (HasCur []),
                                             IntTy],
                                     AppE "sum_tree"
                                          (VarE "y4"))
                                    (LetE ("fltPrm6",
                                           IntTy,
                                           ProjE 1
                                                 (VarE "hoistapp19"))
                                          (LetE ("end_y4",
                                                 PackedTy "CURSOR_TY"
                                                          ()
                                                          (HasCur []),
                                                 ProjE 0
                                                       (VarE "hoistapp19"))
                                                (LetE ("fltPrd23",
                                                       IntTy,
                                                       PrimAppE AddP
                                                                [VarE "fltPrm5",
                                                                 VarE "fltPrm6"])
                                                      (MkProdE [VarE "end_y4",
                                                                VarE "fltPrd23"]))))))))))

As an example, the type PackedTy "CURSOR_TY" () (HasCur [PackedTy "Tree" () NoneCur, PackedTy "Tree" () NoneCur]) means a cursor that still "has" two trees. You can read off from the types how the two trees are consumed, ending up with a cursor with only Has(), which is returned.

Currently the actual type checker just ignores these types.

Next up is adding the Needs(...) types, which I think might be more difficult.

[rrnewton]

Ah, I see this is a third parameter of the PackedTy. That seems reasonable.

But right now there are really two different normal forms:

• PackedTy "CURSOR_TY" _ (HasCur _)
• PackedTy other_string _ NoneCur

As a refactor I think it would make since to go ahead and get rid of the (temporary) pattern synonym business for CursorTy and instead make CursorTy a disjoint type from PackedTy (even in L1.. it can just be unused, a violation of the nanopass principle, yes). After that refactor happens, then only the CursorTy constructor will need to track Has/Needs information, right @vollmerm ? (And only one or the other, which makes it a write pointer or a read pointer...)

[vollmerm]

We changed direction and this is no longer going to be implemented.

[rrnewton]

Yeah, I agree that this is obsolete. Thanks for triaging. In the new system, @vollmerm's L2 typechecker already ensures that locations are already written once. It would probably be overkill to try to ensure that cursors are used linearly once we get to L3.

The place linearity may eventually come back is in the front end language (L0). If we use the Linear Haskell design in the front end, GHC will actually be checking the linearity. This would be in service of fusion (@laithsakka), which takes multiple distinct forms:

• In out of place tree transforms A->B->C: If the tree traversals are linearly typed, that guarantees that fusion is safe, shifting burden from the program analysis to the type system.
• On an out-of-place-transform A->B or A->A: The final deforestation would be to convert to an in-place traversal via mutation of the input tree. Linearity of the source program guarantees that the input may be destroyed.
  • Implementing in-place traversal can use various representations in the compiler, it can look like executing new data-constructors, but just-freed old memory (a la clean), or it can use explicit mutation on the cells that make up the tree.
  • Re: explicit mutation, Once we have such linear types, they could be exposed in the front-end to expose mutable data structures and allow writing of in-place traversals directly.