Skip to content

Commit

Permalink
Now with an EverythingIsApplied constraint
Browse files Browse the repository at this point in the history
To help with silently not overriding anything
  • Loading branch information
reactormonk committed Jun 6, 2018
1 parent 075c8eb commit fc2ec64
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 23 deletions.
25 changes: 6 additions & 19 deletions src/HedgehogExample.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,30 +9,20 @@ import V2
import Data.Diverse

newtype Name = Name Text
newtype Address = Address Text
newtype Email = Email Text

data Person = Person
{ _name :: Name
, _address :: Address
, _email :: Email
}

data Company = Company
{ _employees :: [Person]
, _ceo :: Person }
}

instance MonadGen m => DefaultRecipe Identity (m Name) where
type DefaultRecipeDeps Identity (m Name) = '[]
def = pureRecipe $ do
name <- text (linear 3 20) unicode
pure $ Name name

instance MonadGen m => DefaultRecipe Identity (m Address) where
type DefaultRecipeDeps Identity (m Address) = '[]
def = pureRecipe $ do
name <- text (linear 3 20) unicode
pure $ Address name
def = pureRecipe $ Name <$> text (linear 3 20) unicode

instance MonadGen m => DefaultRecipe Identity (m Email) where
type DefaultRecipeDeps Identity (m Email) = '[]
Expand All @@ -42,28 +32,25 @@ instance MonadGen m => DefaultRecipe Identity (m Email) where
pure $ Email $ (user <> "@" <> host)

instance MonadGen m => DefaultRecipe Identity (m Person) where
type DefaultRecipeDeps Identity (m Person) = '[m Name, m Address, m Email]
type DefaultRecipeDeps Identity (m Person) = '[m Name, m Email]
def = Recipe $ \deps -> pure $ do
name <- grab deps
address <- grab deps
email <- grab deps
pure $ Person name address email
pure $ Person name email

instance MonadGen m => DefaultRecipe Identity (m Company) where
type DefaultRecipeDeps Identity (m Company) = '[m Person]
def = Recipe $ \deps -> pure $ do
ceo <- grab deps
employees <- Gen.list (linear 3 10) (grab deps)
pure $ Company employees ceo
pure $ Company employees

regularGen :: MonadGen m => m Company
regularGen = runIdentity $ finish nil

largeCompanyGen' :: forall (m :: * -> *). MonadGen m => Recipe Identity (m Company) '[m Person]
largeCompanyGen' = Recipe $ \deps -> pure $ do
ceo <- grab deps
employees <- Gen.list (linear 100 1000) (grab deps)
pure $ Company employees ceo
pure $ Company employees

largeCompanyGen :: forall m. MonadGen m => (m Company)
largeCompanyGen = runIdentity $ finish (largeCompanyGen' @m ./ nil) -- TODO why is this annotation required?
Expand Down
4 changes: 4 additions & 0 deletions src/Tests.hs
Original file line number Diff line number Diff line change
Expand Up @@ -50,3 +50,7 @@ c5 = finish nil

rc5 :: Identity M5
rc5 = finish (r5 ./ nil)

-- Should fail with "not everything is applied"
-- rc4fail :: Identity M4
-- rc4fail = finish (r5 ./ nil)
21 changes: 17 additions & 4 deletions src/V2.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ import qualified Data.Sequence as S
import Data.Diverse.Many.Internal (Many(..))
import Unsafe.Coerce
import Numbers
-- import GHC.TypeLits as Lits
import GHC.TypeLits as Lits

pureRecipe :: Applicative effect => target -> Recipe effect target '[]
pureRecipe target = Recipe $ \_ -> pure target
Expand Down Expand Up @@ -120,13 +120,28 @@ instance forall effect target book state.
(s2r, deps) :: (Many state, Many (RecipeDeps effect target book)) <- s2
(res s2r deps) :: effect (Many state, target)

finish :: forall target (effect:: * -> *) (book :: [*]) (store :: [*]).
type family Contains (target :: *) (store :: [*]) :: Bool where
Contains target (target ': t) = True
Contains target (h ': t) = Contains target t
Contains target '[] = False

type family EverythingIsAppliedTypeError (bool :: Bool) (s :: Type) (b :: [Type]) :: Constraint where
EverythingIsAppliedTypeError True s b = ()
EverythingIsAppliedTypeError False s b = TypeError ('Text "The type " ':<>: ShowType s ':<>: 'Text " is not overriding anything in " ':<>: ShowType b)

type family EverythingIsApplied (effect :: * -> *) target (book :: [*]) (store :: [*]) :: Constraint where
EverythingIsApplied effect target ((Recipe effect head _) ': tBook) store = (EverythingIsAppliedTypeError (Contains head store) head store, EverythingIsApplied effect target tBook store)
EverythingIsApplied effect target (head ': tBook) store = TypeError ('Text "The type " ':<>: ShowType head ':<>: 'Text " is not a Recipe")
EverythingIsApplied effect target '[] store = ()

finish :: forall (effect :: * -> *) target (book :: [*]) (store :: [*]).
( store ~ (LiftMaybe (Nub (RecipeDepsRec effect target book (RecipeDeps effect target book))))
, ToS (ListLen (EmptyStore effect target book))
, HasRecipe effect target book
, Monad effect
, (SubSelect effect book (RecipeDeps effect target book) store)
, (UniqueMember (Maybe target) store)
, EverythingIsApplied effect target book (Nub (RecipeDepsRec effect target book (RecipeDeps effect target book)))
) =>
Many book -> effect target
finish book = do
Expand All @@ -136,8 +151,6 @@ finish book = do
(_, target) <- cook book store (Proxy @target)
pure target

-- test

class DefaultRecipe (effect :: * -> *) target where
type DefaultRecipeDeps effect target :: [*]
def :: Recipe effect target (DefaultRecipeDeps effect target)
Expand Down

0 comments on commit fc2ec64

Please sign in to comment.