Skip to content

Instantly share code, notes, and snippets.

@ymdfield
Last active August 1, 2025 09:46
Show Gist options
  • Select an option

  • Save ymdfield/53c1739266a82c21e3fc4e21298970f2 to your computer and use it in GitHub Desktop.

Select an option

Save ymdfield/53c1739266a82c21e3fc4e21298970f2 to your computer and use it in GitHub Desktop.

Most Haskell effect libraries including Heftia use integer IDs for so‑called "effect tags" to identify which effect to handle. Concretely, this ID is the index of that effect in a type‑level list representing the effect set. For example, in the set

{Reader[String], Reader[Double], Reader[Char]}

the tag ID of Reader[Char] is 2.

Effect handling matches on these tag IDs at runtime to determine which effect to interpret. The tag IDs themselves, however, are computed at compile time via type‑level computation. That means, to intercept a suspended effect's handling, the compiler must already know that the effect is present in the list.

Right now, modifyZero has the type

A < S => A < S

but whether Reader[Int] is included in S can never be known at compile time, given only the knowledge confined to the scope of the modifyZero definition. Therefore, modifyZero can't tamper with the interpretation of Reader[Int], and it's impossible to implement something like calling Reader.run(0) internally while still having the type A < S => A < S. From the standpoint of parametricity, this is desirable: by looking at the type, you know what cannot happen, giving you guarantees and predictability of behavior.

To enable the desired functionality, a type constraint asserting that Reader[Int] ∈ S must be introduced. With such a constraint in place, modifyZero can be implemented. Below is an example written in Heftia.

#!/usr/bin/env -S cabal run -v1
{- cabal:
build-depends: base, heftia-effects ^>= 0.7, data-effects-core
ghc-options: -Wall
-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Control.Monad.Hefty
import Control.Monad.Hefty.Reader
import Data.Effect.OpenUnion

modifyZero :: Ask Int :> es => Eff es a -> Eff es a
modifyZero = runAsk 0 . pull

pull :: forall e es a. e :> es => Eff es a -> Eff (e : es) a
pull = interposeFor @e (weakenFor labelMembership) send . raise

main :: IO ()
main = print $ runPure $ runAsk 42 $ modifyZero ask

-- > main
-- 0

Here, the pull function is a technique for emulating the behavior of Kyo‑style effect sets. For details, see: https://github.com/sayo-hs/kontrolle/blob/8fa41192202b25a92706d28df28725ad9aab4c6d/src/Control/Effect/Simple.hs

If the constraint Ask Int :> es is absent, modifyZero can do virtually nothing internally; at best it could run the action multiple times. That illustrates just how strong the guarantees provided by parametricity are. Consequently, even if something like Reader.run is included in its body, it cannot interfere with the Reader effect in the es set, and the result remains 42.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment