Skip to content

Instantly share code, notes, and snippets.

@AndreasPK
Created July 29, 2021 13:23
Show Gist options
  • Save AndreasPK/06bd02f2772cb950af123ab786c98db7 to your computer and use it in GitHub Desktop.
Save AndreasPK/06bd02f2772cb950af123ab786c98db7 to your computer and use it in GitHub Desktop.
GADT map stuff
data Side = LeftSide | RightSide
data GEither c a b where
GLeft :: a -> GEither 'LeftSide a b
GRight :: b -> GEither 'RightSide a b
data LVal = LVal Int
data RVal = RVal Int
data LeftRightMap where
MkMap :: IntMap (GEither LeftSide LVal RVal) -> IntMap (GEither RightSide LVal RVal) -> LeftRightMap
mapBoth :: LeftRightMap -> (forall side. (GEither side LVal RVal) -> (GEither side LVal RVal)) -> LeftRightMap
mapBoth (MkMap lmap rmap) f =
MkMap (fmap f lmap) (fmap f rmap)
mapLeft :: LeftRightMap -> (forall side. (GEither LeftSide LVal RVal) -> (GEither LeftSide LVal RVal)) -> LeftRightMap
mapLeft (MkMap lmap rmap) f =
MkMap (fmap f lmap) rmap
fleft :: (GEither LeftSide LVal RVal) -> (GEither LeftSide LVal RVal)
fleft (GLeft (LVal x)) = GLeft $ LVal $ x + 1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment