Skip to content

Instantly share code, notes, and snippets.

@sjoerdvisscher

sjoerdvisscher/LinearClearBits.hs

Created December 25, 2025 15:45
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save sjoerdvisscher/68819f7fd2b2fe14133b49b7b76ab413 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save sjoerdvisscher/68819f7fd2b2fe14133b49b7b76ab413 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. sjoerdvisscher created this gist Dec 25, 2025.
    19 changes: 19 additions & 0 deletions LinearClearBits.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,19 @@
    {-# LANGUAGE GHC2024, LinearTypes #-}
    module LinearClearBits where

    data With3 a b c where
    With3 :: x %1 -> (x %1 -> a) -> (x %1 -> b) -> (x %1 -> c) -> With3 a b c

    w1 :: With3 a b c %1 -> a
    w1 (With3 x f _ _) = f x

    w2 :: With3 a b c %1 -> b
    w2 (With3 x _ g _) = g x

    w3 :: With3 a b c %1 -> c
    w3 (With3 x _ _ h) = h x

    data Bin = Bin { caseBin :: forall r. With3 (Bin %1 -> r) (Bin %1 -> r) r %1 -> r }

    clearBitsBin :: Bin %1 -> Bin
    clearBitsBin (Bin b) = Bin (\w -> b (With3 w (\w' p -> w1 w' (clearBitsBin p)) (\w' p -> w1 w' (clearBitsBin p)) (\w' -> w3 w')))