Since Haskell has linear types so we can track resources, why can't we disable the GC like in ATS?

Learn
12

No, you shouldn’t need pragmas. As the abstract says:

Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell.

Linear types permeate all the way into Core, so optimizations should preserve them, although I believe that is not yet checked at the moment. @romes is working on that. But any problems with that should be seen as bugs in GHC, not as problems with linear constraints.

Also, the second argument of swap is not a good example because that’s just an integer which may be shared without causing any problems. It is the third argument as which is the mutable array that would cause problems if it were shared improperly.

Edit: nevermind, I misread your post. The linear constraints will be desugared to an evidence passing style which works similarly to the state monad:

swap i w as
      ⋮
swap i x as

Desugars to something like this:

let s1 = swap s0 i w as in
      ⋮
let s2 = swap s1 i x as in

And that could get inlined like this:

   let s3 = (let
     !Ur ai = get s0 i as
     !Ur aw = get s0 w as
     !s1 = set s0 i aw as
     !s2 = set s1 w ai as
   in s2) in
      ⋮
   let s6 = (let
     !Ur ai = get s3 i as
     !Ur ax = get s3 x as 
     !s4 = set s3 i ax as
     !s5 = set s4 x ai as
   in s5) in

So there are no duplicate subexpressions.

2 Likes