{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreigrm6ypufwr6i57drv4g3xwckaa5gqzcf2id3lr7s7rmk2q2cx37m",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mluljpbliwt2"
  },
  "path": "/t/ann-linear-locks-locking-primitives-free-of-deadlocks/14112#post_2",
  "publishedAt": "2026-05-15T04:50:35.000Z",
  "site": "https://discourse.haskell.org",
  "textContent": "This is a cool idea, but I don’t think it really requires `LinearTypes`. Sketch:\n\n\n    -- Compile-time proof tokens.\n    type (<) :: k -> k -> ZeroBitType\n\n    (~) :: l < m -> m < n -> l < n\n\n    -- Newtype over IO, annotated by \"lock level\" and \"acquisition level\".\n    type Scoped :: k -> k -> Type -> Type\n\n    run :: (forall k (l :: k). Scoped l l b) -> IO b\n\n    fork :: Scoped l a () -> Scoped l a ThreadId\n\n    -- Newtype over MVar, annotated by level.\n    type Lock :: k -> Type -> Type\n\n    -- Create a new lock level and corresponding lock.\n    new\n      :: b\n      -> (forall m. l < m -> Lock m b -> Scoped m a r)\n      -> Scoped l a r\n\n    -- Given that the acquisition level is less than the level of the lock,\n    -- acquire it in a scope of the corresponding acquisition level.\n    with\n      :: a < m\n      -> Lock m b\n      -> (b -> Scoped l m (b, r))\n      -> Scoped l a r\n",
  "title": "[ANN] linear-locks: locking primitives free of deadlocks"
}