Skip to content

Instantly share code, notes, and snippets.

@jmatsushita
Created October 14, 2021 19:32
Show Gist options
  • Save jmatsushita/049426e4a71ec6751644a35cdd9a91f1 to your computer and use it in GitHub Desktop.
Save jmatsushita/049426e4a71ec6751644a35cdd9a91f1 to your computer and use it in GitHub Desktop.
Set Monad (WIP)
module Main where
import Data.Foldable
import Prelude
import Data.Set as S
-- data Set a where
-- Prim :: (Ord a) => S.Set a -> Set a
-- Return :: a -> Set a
-- Bind :: Set a -> (a -> Set b) -> Set b
-- Zero :: Set a
-- Plus :: Set a -> Set a -> Set a
-- https://hgiasac.github.io/posts/2018-12-18-PureScript-GADTs-Alternatives---Recap.html
data Set a
= Prim (forall r. (Ord a => S.Set a -> r) -> r)
| Return (a)
| Bind (forall r. (forall b. Set b -> (b -> Set a) -> r) -> r)
| Zero
| Plus (Set a) (Set a)
run :: forall a. (Ord a) => Set a -> S.Set a
run (Prim s) = s identity
run (Return a) = S.singleton a
run (Zero) = S.empty
run (Plus ma mb) = run ma `S.union` run mb
run (Bind e) = e go
where
go (Prim s) f = foldl S.union S.empty (S.map (run <<< f) $ s identity)
go (Return a) f = run (f a)
go Zero _ = S.empty
go (Plus (Prim s) ma) f = run $ bind (prim ((s identity) `S.union` (run ma))) f
go (Plus ma (Prim s)) f = run $ bind (prim (run ma `S.union` s identity)) f
go (Plus (Return a) ma) f = run (Plus (f a) (bind ma f))
go (Plus ma (Return a)) f = run (Plus (bind ma f) (f a))
go (Plus Zero ma) f = run (bind ma f)
go (Plus ma Zero) f = run (bind ma f)
go (Plus (Plus ma mb) mc) f = run (bind (Plus ma (Plus mb mc)) f)
go (Plus ma mb) f = run (Plus (bind ma f) (bind mb f))
go (Bind e') g = e' go'
where
go' ma f = run (bind ma (\a -> bind (f a) g))
prim :: forall a. Ord a => S.Set a -> Set a
prim s = Prim (_ $ s)
bind :: forall a b. Set b -> (b -> Set a) -> Set a
bind s f = Bind (\x -> x s f)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment