Environmental Dependencies as Coeffects
summary
Claim: environmental dependencies become coeffects modeled as indexed comonads and encoded with type-level monoids. Implementation: a Haskell prototype uses heavy GHC extensions and dependent-style naturals to enforce, for example, a moving-average needing 12 previous values and a bounded-resource scenario (six MRI machines) as a goal. Works for dataflow and implicit-parameter (co‑reader) examples; fails for bounded reuse of IO actions without linear types and a distributive law. Prototype lives on the listed GitHub; linear-Haskell branch is partial.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:48Motivation Examples
- 2:44Coeffects
- 4:25Formalities
- 6:03Pure Functions
- 6:42Monadic Action
- 10:14Index Monoise
- 12:14Coeffect Type Class
- 12:51Constraints
- 16:50Data Flow
- 19:04Bounded Reuse
- 21:37Extend
- 24:48Linear Haskell
- 28:25Linear Granular
- 29:33Implicit Parameters
- 32:32Further Directions
- 33:44Questions
related talks
23mSecurity Reasoning via Substructural Dependency Tracking
22mGiving Semantics to Program-Counter Labels via Secure Effects
32mSubstructural Information Flow via Polymorphism
25mCapabilities, Effects, Ownership, and Behaviors
20mInternalizing Indistinguishability with Dependent Types
22mCompilers should get over themselves and respect semantic dependencies!
36mObject Capabilities
19mScalable Language Agnostic Taint Tracking using Explicit Data Dependencies