Set Monad (WIP)

Main.purs

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)