Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support good type inference with unique parametrized effects #268

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion effectful-core/effectful-core.cabal
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
cabal-version: 3.0
build-type: Simple
name: effectful-core
version: 2.5.0.0
version: 2.5.1.0
license: BSD-3-Clause
license-file: LICENSE
category: Control
Expand Down
1 change: 1 addition & 0 deletions effectful-core/src/Effectful.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ module Effectful
, Dispatch(..)
, DispatchOf
, (:>)
, type (<:>)
, (:>>)

-- * Running the 'Eff' monad
Expand Down
55 changes: 54 additions & 1 deletion effectful-core/src/Effectful/Internal/Effect.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK not-home #-}
-- | Type-safe indexing for 'Effectful.Internal.Monad.Env'.
Expand All @@ -16,7 +17,10 @@ module Effectful.Internal.Effect
, type (++)
, KnownEffects(..)

-- * Re-exports
-- * Unique parametrized effects
, type (<:>)

-- * Re-exports
, Type
) where

Expand Down Expand Up @@ -148,3 +152,52 @@ instance KnownEffects es => KnownEffects (e : es) where

instance KnownEffects '[] where
knownEffectsLength = 0

----------------------------------------

type family (e :: Effect) <:> (es :: [Effect]) :: Constraint where
e a1 a2 a3 a4 a5 <:> es = Has5UniqueParams e a1 a2 a3 a4 a5 es
e a1 a2 a3 a4 <:> es = Has4UniqueParams e a1 a2 a3 a4 es
e a1 a2 a3 <:> es = Has3UniqueParams e a1 a2 a3 es
e a1 a2 <:> es = Has2UniqueParams e a1 a2 es
e a1 <:> es = HasUniqueParam e a1 es

class e a1 :> es => HasUniqueParam
(e :: k1 -> Effect)
(a1 :: k1)
(es :: [Effect])
| e es -> a1

class e a1 a2 :> es => Has2UniqueParams
(e :: k1 -> k2 -> Effect)
(a1 :: k1)
(a2 :: k2)
(es :: [Effect])
| e es -> a1 a2

class e a1 a2 a3 :> es => Has3UniqueParams
(e :: k1 -> k2 -> k3 -> Effect)
(a1 :: k1)
(a2 :: k2)
(a3 :: k3)
(es :: [Effect])
| e es -> a1 a2 a3

class e a1 a2 a3 a4 :> es => Has4UniqueParams
(e :: k1 -> k2 -> k3 -> k4 -> Effect)
(a1 :: k1)
(a2 :: k2)
(a3 :: k3)
(a4 :: k4)
(es :: [Effect])
| e es -> a1 a2 a3 a4

class e a1 a2 a3 a4 a5 :> es => Has5UniqueParams
(e :: k1 -> k2 -> k3 -> k4 -> k5 -> Effect)
(a1 :: k1)
(a2 :: k2)
(a3 :: k3)
(a4 :: k4)
(a5 :: k5)
(es :: [Effect])
| e es -> a1 a2 a3 a4 a5
2 changes: 1 addition & 1 deletion effectful-th/effectful-th.cabal
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
cabal-version: 3.0
build-type: Simple
name: effectful-th
version: 1.0.0.3
version: 1.0.1.0
license: BSD-3-Clause
license-file: LICENSE
category: Control
Expand Down
24 changes: 16 additions & 8 deletions effectful-th/src/Effectful/TH.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
module Effectful.TH
( makeEffect
, makeEffect_
, makeUniqueEffect
, makeUniqueEffect_
) where

import Control.Monad
Expand Down Expand Up @@ -57,7 +59,7 @@ import Effectful.Dispatch.Dynamic
-- If the constructor declaration has Haddock, then this is reused for the
-- sending functions, otherwise a simple placeholder is used.
makeEffect :: Name -> Q [Dec]
makeEffect = makeEffectImpl True
makeEffect = makeEffectImpl ''(:>) True

-- | Like 'makeEffect', but doesn't generate type signatures. This is useful
-- when you want to attach Haddock documentation to function signatures:
Expand All @@ -72,18 +74,24 @@ makeEffect = makeEffectImpl True
--
-- /Note:/ function signatures must be added /after/ the call to 'makeEffect_'.
makeEffect_ :: Name -> Q [Dec]
makeEffect_ = makeEffectImpl False
makeEffect_ = makeEffectImpl ''(:>) False

makeEffectImpl :: Bool -> Name -> Q [Dec]
makeEffectImpl makeSig effName = do
makeUniqueEffect :: Name -> Q [Dec]
makeUniqueEffect = makeEffectImpl ''(<:>) True

makeUniqueEffect_ :: Name -> Q [Dec]
makeUniqueEffect_ = makeEffectImpl ''(<:>) False

makeEffectImpl :: Name -> Bool -> Name -> Q [Dec]
makeEffectImpl memberOp makeSig effName = do
checkRequiredExtensions
info <- reifyDatatype effName
dispatch <- do
e <- getEff (ConT $ datatypeName info) (const WildCardT <$> datatypeInstTypes info)
let dispatchE = ConT ''DispatchOf `AppT` e
dynamic = PromotedT 'Dynamic
pure . TySynInstD $ TySynEqn Nothing dispatchE dynamic
ops <- traverse (makeCon makeSig) (constructorName <$> datatypeCons info)
ops <- traverse (makeCon memberOp makeSig) (constructorName <$> datatypeCons info)
pure $ dispatch : concat (reverse ops)
where
getEff :: Type -> [Type] -> Q Type
Expand All @@ -109,8 +117,8 @@ makeEffectImpl makeSig effName = do
_ -> pure ()

-- | Generate a single definition of an effect operation.
makeCon :: Bool -> Name -> Q [Dec]
makeCon makeSig name = do
makeCon :: Name -> Bool -> Name -> Q [Dec]
makeCon memberOp makeSig name = do
fixity <- reifyFixity name
typ <- reify name >>= \case
DataConI _ typ _ -> pure typ
Expand Down Expand Up @@ -194,7 +202,7 @@ makeCon makeSig name = do
else VarE 'send `AppE` effOp
#endif
let fnSig = ForallT actionVars
(ConT ''HasCallStack : UInfixT effTy ''(:>) esVar : actionCtx)
(ConT ''HasCallStack : UInfixT effTy memberOp esVar : actionCtx)
(makeTyp esVar substM resTy actionParams)

let mkDec fix =
Expand Down
16 changes: 16 additions & 0 deletions effectful-th/tests/ThTests.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
module Main where

import Data.Kind (Type)
import Data.String
import GHC.TypeLits

import Effectful
Expand All @@ -12,6 +13,21 @@ import Effectful.TH
main :: IO ()
main = pure () -- only compilation tests

data Test1 a :: Effect where
Test1 :: Test1 a m a
makeUniqueEffect ''Test1

data Test2 a b :: Effect where
Test2 :: Test2 a b m (a, b)
AmbTest :: Test2 a b m ()
makeUniqueEffect ''Test2

test :: (Num n, IsString s, Test1 n <:> es, Test2 s Char <:> es) => Eff es ()
test = do
_ <- test1
_ <- test2
ambTest

data SimpleADT (m :: Type -> Type) (a :: Type)
= SimpleADTC1 Int
| SimpleADTC2 String
Expand Down
4 changes: 2 additions & 2 deletions effectful/effectful.cabal
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
cabal-version: 3.0
build-type: Simple
name: effectful
version: 2.5.0.0
version: 2.5.1.0
license: BSD-3-Clause
license-file: LICENSE
category: Control
Expand Down Expand Up @@ -74,7 +74,7 @@ library
, async >= 2.2.2
, bytestring >= 0.10
, directory >= 1.3.2
, effectful-core >= 2.5.0.0 && < 2.5.1.0
, effectful-core >= 2.5.1.0 && < 2.5.2.0
, process >= 1.6.9
, strict-mutable-base >= 1.1.0.0
, time >= 1.9.2
Expand Down
Loading