A fundamental property when reasoning about randomized programs is \emph{probabilistic independence}, which states that two random quantities are entirely uncorrelated. By viewing independence as a probabilistic version of separation, recent works have developed separation logics capturing independence for probabilistic imperative programs. However, it is not clear how to capture independence in functional, higher-order programs.

In this work, we propose two higher-order languages that can reason about sharing and separation in effectful programs. Our first language $\lambda^1_{INI}$ has a linear type system and probabilistic semantics, where the two product types capture independent and possibly-dependent pairs. Our second language $\lambda^2_{INI}$ is a two-level, stratified language, inspired by Benton’s linear-non-linear (LNL) calculus. We motivate this language with a probabilistic model, but we also provide a general categorical semantics and exhibit a range of concrete models beyond probabilistic programming.