Skip to content

Commit

Permalink
Support good type inference with unique parametrized effects
Browse files Browse the repository at this point in the history
  • Loading branch information
arybczak committed Nov 4, 2024
1 parent a70cf0c commit 19dc8c8
Show file tree
Hide file tree
Showing 7 changed files with 96 additions and 13 deletions.
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
60 changes: 59 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,15 @@ module Effectful.Internal.Effect
, type (++)
, KnownEffects(..)

-- * Re-exports
-- * The effects
, type (<:>)
, The1
, The2
, The3
, The4
, The5

-- * Re-exports
, Type
) where

Expand Down Expand Up @@ -148,3 +157,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 = The5 e a1 a2 a3 a4 a5 es
e a1 a2 a3 a4 <:> es = The4 e a1 a2 a3 a4 es
e a1 a2 a3 <:> es = The3 e a1 a2 a3 es
e a1 a2 <:> es = The2 e a1 a2 es
e a1 <:> es = The1 e a1 es

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

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

class e a1 a2 a3 :> es => The3
(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 => The4
(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 => The5
(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 @@ -4,7 +4,9 @@
-- effects via Template Haskell.
module Effectful.TH
( makeEffect
, makeTheEffect
, makeEffect_
, makeTheEffect_
) where

import Control.Monad
Expand Down Expand Up @@ -57,7 +59,10 @@ 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

makeTheEffect :: Name -> Q [Dec]
makeTheEffect = 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 +77,21 @@ makeEffect = makeEffectImpl True
--
-- /Note:/ function signatures must be added /after/ the call to 'makeEffect_'.
makeEffect_ :: Name -> Q [Dec]
makeEffect_ = makeEffectImpl False
makeEffect_ = makeEffectImpl ''(:>) False

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

makeEffectImpl :: Bool -> Name -> Q [Dec]
makeEffectImpl makeSig effName = do
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
makeTheEffect ''Test1

data Test2 a b :: Effect where
Test2 :: Test2 a b m (a, b)
AmbTest :: Test2 a b m ()
makeTheEffect ''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

0 comments on commit 19dc8c8

Please sign in to comment.