Skip to content

Instantly share code, notes, and snippets.

@JadenGeller
Last active October 30, 2019 21:47
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save JadenGeller/d63165a774187d955f2836c3596590dd to your computer and use it in GitHub Desktop.
Save JadenGeller/d63165a774187d955f2836c3596590dd to your computer and use it in GitHub Desktop.
Correct-by-composition set operations that cannot branch on ordering
{-# LANGUAGE FlexibleInstances, UndecidableInstances, LambdaCase, DeriveFunctor, MonadComprehensions #-}
import qualified Prelude
import Prelude (Show, Num, Functor, Bool(..), not, Int, Maybe(..), Either(..), Eq, (==), (.), ($), const, otherwise)
import Control.Monad (MonadPlus, guard, when, unless, (>>=), fmap, mzero, mplus, return)
import qualified Data.Foldable
import Data.Foldable (Foldable)
import Data.Maybe (maybe, isJust)
import Data.Functor.Foldable (Fix)
class (MonadPlus s) => Set s where
null :: s a -> Bool
class (Set b) => Bag b where
count :: b a -> Int
instance (Foldable s, MonadPlus s) => Set s where
null = Data.Foldable.null
instance (Foldable s, MonadPlus s) => Bag s where
count = Data.Foldable.length
or :: (Set s) => s Bool -> Bool
or = not . null . (>>= guard)
and :: (Set s) => s Bool -> Bool
and = not . or . fmap not
any :: (Set s) => (a -> Bool) -> s a -> Bool
any pred = or . fmap pred
all :: (Set s) => (a -> Bool) -> s a -> Bool
all pred = and . fmap pred
(+) :: (Set s) => s a -> s a -> s a
xs + ys = xs `mplus` ys
(-) :: (Set s, Eq a) => s a -> s a -> s a
xs - ys = do x <- xs
guard . not $ any (== x) ys
return x
catMaybes :: (Set s) => s (Maybe a) -> s a
catMaybes xs = [x | Just x <- xs]
-- How can we show the type system we're not dropping anything when we catMaybes?
sequence :: (Set s) => s (Maybe a) -> Maybe (s a)
sequence xs = if (all isJust xs) then Just (catMaybes xs) else Nothing
--sequence :: (Set s) => s (Maybe a) -> Maybe (s a)
--sequence xs = if (all isJust xs) then Just (catMaybes xs) else Nothing
lefts :: (Set s) => s (Either a b) -> s a
lefts xs = [x | Left x <- xs]
rights :: (Set s) => s (Either a b) -> s b
rights xs = [x | Right x <- xs]
partitionEithers :: (Set s) => s (Either a b) -> (s a, s b)
partitionEithers xs = (lefts xs, rights xs)
data Nat = Zero | Succ Nat
deriving Show
isZero :: Nat -> Bool
isZero Zero = True
isZero (Succ _) = False
pred :: Nat -> Maybe Nat
pred Zero = Nothing
pred (Succ n) = Just n
min :: (Set r) => r Nat -> Maybe Nat
min ns | null ns = Nothing
min ns | any isZero ns = Just Zero
| otherwise = (fmap Succ . min . catMaybes. fmap pred) ns
-- We use catMaybes remove the Just, but we're guarenteed that there are no Nothing
-- Could the type system handle this?
max :: (Set r) => r Nat -> Maybe Nat
max ns | null ns = Nothing
max ns | all isZero ns = Just Zero
| otherwise = (fmap Succ . max . catMaybes . fmap pred) ns
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment