Created
October 7, 2021 19:47
-
-
Save jmatsushita/f3126befb0a0a8676067b9b91259aeca to your computer and use it in GitHub Desktop.
purescript-set-monad
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Data.Set.Monad where | |
import Prelude | |
import Data.Set as S | |
import Data.Foldable | |
import Data.Tuple.Nested | |
import Unsafe.Coerce | |
-- 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 (Ord a => S.Set a) | |
| Return (a) | |
| Bind (forall b. (Set b) /\ (b -> Set a)) | |
| Zero | |
| Plus (Set a) (Set a) | |
run :: forall a. (Ord a) => Set a -> S.Set a | |
run (Prim s) = s | |
run (Return a) = S.singleton a | |
run (Zero) = S.empty | |
run (Plus ma mb) = run ma `S.union` run mb | |
run (Bind (Prim s /\ f)) = foldl S.union S.empty (S.map (run <<< f) s) | |
run (Bind (Return a /\ f)) = run (f a) | |
run (Bind (Zero /\ _)) = S.empty | |
run (Bind (Plus (Prim s) ma /\ f)) = run (Bind (unsafeCoerce $ Prim (s `S.union` run ma) /\ f)) | |
run (Bind (Plus ma (Prim s) /\ f)) = run (Bind (unsafeCoerce $ Prim (run ma `S.union` s) /\ f)) | |
run (Bind (Plus (Return a) ma /\ f)) = run (Plus (f a) (Bind (unsafeCoerce $ ma /\ f))) | |
run (Bind (Plus ma (Return a) /\ f)) = run (Plus (Bind (unsafeCoerce $ ma /\ f)) (f a)) | |
run (Bind (Plus Zero ma /\ f )) = run (Bind (unsafeCoerce $ ma /\ f)) | |
run (Bind (Plus ma Zero /\ f )) = run (Bind (unsafeCoerce $ ma /\ f)) | |
run (Bind (Plus (Plus ma mb) mc /\ f)) = run (Bind (unsafeCoerce $ Plus ma (Plus mb mc) /\ f )) | |
run (Bind (Plus ma mb /\ f)) = run (Plus (Bind (unsafeCoerce $ ma /\ f)) (Bind (unsafeCoerce $ mb /\ f))) | |
run (Bind (Bind (ma /\ f) /\ g)) = run (Bind (unsafeCoerce $ ma /\ (\a -> Bind (unsafeCoerce $ (f a) /\ g)))) | |
-- Compiling Data.Set.Monad | |
-- Error found: | |
-- in module Data.Set.Monad | |
-- at src/Data/Set/Monad.purs:29:12 - 29:23 (line 29, column 12 - line 29, column 23) | |
-- Could not match constrained type | |
-- Ord b1 => Tuple (Set b1) (b1 -> Set a0) | |
-- with type | |
-- Tuple t2 t3 | |
-- while trying to match type Ord b1 => Tuple (Set b1) (b1 -> Set a0) | |
-- with type Tuple t2 t3 | |
-- while checking that expression case $0 of | |
-- (Prim s) -> s | |
-- (Return a) -> singleton a | |
-- Zero -> empty | |
-- (Plus ma mb) -> (union (...)) (run mb) | |
-- (Bind (Tuple (Prim s) f)) -> ((...) empty) ((...) s) | |
-- (Bind (Tuple (Return a) f)) -> run (f a) | |
-- (Bind (Tuple Zero _)) -> empty | |
-- (Bind (Tuple (Plus (Prim s) ma) f)) -> run (Bind (...)) | |
-- (Bind (Tuple (Plus ma (Prim s)) f)) -> run (Bind (...)) | |
-- (Bind (Tuple (Plus (Return a) ma) f)) -> run ((...) (...)) | |
-- (Bind (Tuple (Plus ma (Return a)) f)) -> run ((...) (...)) | |
-- (Bind (Tuple (Plus Zero ma) f)) -> run (Bind (...)) | |
-- (Bind (Tuple (Plus ma Zero) f)) -> run (Bind (...)) | |
-- (Bind (Tuple (Plus (Plus ma mb) mc) f)) -> run (Bind (...)) | |
-- (Bind (Tuple (Plus ma mb) f)) -> run ((...) (...)) | |
-- (Bind (Tuple (Bind (Tuple ma f)) g)) -> run (Bind (...)) | |
-- has type Set a0 | |
-- in binding group run | |
-- where a0 is a rigid type variable | |
-- bound at (line 0, column 0 - line 0, column 0) | |
-- b1 is a rigid type variable | |
-- bound at (line 20, column 13 - line 20, column 55) | |
-- t2 is an unknown type | |
-- t3 is an unknown type | |
-- See https://github.com/purescript/documentation/blob/master/errors/ConstrainedTypeUnified.md for more information, | |
-- or to contribute content related to this error. | |
-- [error] Failed to build. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment