haskell - 如何在 haskell 中组合 'freer' 效果?

标签 haskell effect-systems

我正在尝试将一个简单的解释器从基于转换器的 monad 堆栈重写为基于 freer 的效果,但是我遇到了将我的意图传达给 GHC 类型系统的困难。

我只使用 StateFresh目前的效果。我正在使用两种状态,我的效果运行器如下所示:

runErlish g ls = run . runGlobal g . runGensym 0 . runLexicals ls
  where runGlobal    = flip runState
        runGensym    = flip runFresh'
        runLexicals  = flip runState

最重要的是,我用这种类型定义了一个函数 FindMacro:
findMacro :: Members [State (Global v w), State [Scope v w]] r
             => Arr r Text (Maybe (Macro (Term v w) v w))

到目前为止,所有这些都运行良好。当我尝试写 macroexpand2 时出现问题(好吧,macroexpand1,但我正在简化它,因此问题更容易理解):
macroexpand2 s =
  do m <- findMacro s
     return $ case m of
       Just j -> True
       Nothing -> False

这会产生以下错误:
Could not deduce (Data.Open.Union.Member'
                    (State [Scope v0 w0])
                    r
                    (Data.Open.Union.FindElem (State [Scope v0 w0]) r))
from the context (Data.Open.Union.Member'
                    (State [Scope v w])
                    r
                    (Data.Open.Union.FindElem (State [Scope v w]) r),
                  Data.Open.Union.Member'
                    (State (Global v w))
                    r
                    (Data.Open.Union.FindElem (State (Global v w)) r))
  bound by the inferred type for `macroexpand2':
             (Data.Open.Union.Member'
                (State [Scope v w])
                r
                (Data.Open.Union.FindElem (State [Scope v w]) r),
              Data.Open.Union.Member'
                (State (Global v w))
                r
                (Data.Open.Union.FindElem (State (Global v w)) r)) =>
             Text -> Eff r Bool
  at /tmp/flycheck408QZt/Erlish.hs:(79,1)-(83,23)
The type variables `v0', `w0' are ambiguous
When checking that `macroexpand2' has the inferred type
  macroexpand2 :: forall (r :: [* -> *]) v (w :: [* -> *]).
                  (Data.Open.Union.Member'
                     (State [Scope v w])
                     r
                     (Data.Open.Union.FindElem (State [Scope v w]) r),
                   Data.Open.Union.Member'
                     (State (Global v w))
                     r
                     (Data.Open.Union.FindElem (State (Global v w)) r)) =>
                  Text -> Eff r Bool
Probable cause: the inferred type is ambiguous

好的,我可以添加一个 Members类型的注释:
macroexpand2 :: Members [State (Global v w), State [Scope  v w]] r
                => Text -> Eff r Bool

现在我明白了:
Overlapping instances for Member (State [Scope v0 w0]) r
  arising from a use of `findMacro'
Matching instances:
  instance Data.Open.Union.Member'
             t r (Data.Open.Union.FindElem t r) =>
           Member t r
    -- Defined in `Data.Open.Union'
There exists a (perhaps superclass) match:
  from the context (Members
                      '[State (Global v w), State [Scope v w]] r)
    bound by the type signature for
               macroexpand2 :: Members
                                 '[State (Global v w), State [Scope v w]] r =>
                               Text -> Eff r Bool
    at /tmp/flycheck408QnV/Erlish.hs:(79,17)-(80,37)
(The choice depends on the instantiation of `r, v0, w0'
 To pick the first instance above, use IncoherentInstances
 when compiling the other instance declarations)
In a stmt of a 'do' block: m <- findMacro s
In the expression:
  do { m <- findMacro s;
       return
       $ case m of {
           Just j -> True
           Nothing -> False } }
In an equation for `macroexpand2':
    macroexpand2 s
      = do { m <- findMacro s;
             return
             $ case m of {
                 Just j -> True
             Nothing -> False } }

有人建议我在 irc 上尝试 forall r v w.这没有什么区别。出于好奇,我尝试使用 IncoherentInstances在编译这段代码时(我不喜欢检查 freer 和 play 的分支),看看它是否会给我一个关于发生了什么的线索。它没:
Could not deduce (Data.Open.Union.Member'
                    (State [Scope v0 w0])
                    r
                    (Data.Open.Union.FindElem (State [Scope v0 w0]) r))
  arising from a use of `findMacro'
from the context (Members
                    '[State (Global v w), State [Scope v w]] r)
  bound by the type signature for
             macroexpand2 :: Members
                               '[State (Global v w), State [Scope v w]] r =>
                             Text -> Eff r Bool
  at /tmp/flycheck408eru/Erlish.hs:(79,17)-(80,37)
The type variables `v0', `w0' are ambiguous
Relevant bindings include
  macroexpand2 :: Text -> Eff r Bool
    (bound at /tmp/flycheck408eru/Erlish.hs:81:1)
Note: there are several potential instances:
  instance (r ~ (t' : r'), Data.Open.Union.Member' t r' n) =>
           Data.Open.Union.Member' t r ('Data.Open.Union.S n)
    -- Defined in `Data.Open.Union'
  instance (r ~ (t : r')) =>
           Data.Open.Union.Member' t r 'Data.Open.Union.Z
    -- Defined in `Data.Open.Union'
In a stmt of a 'do' block: m <- findMacro s
In the expression:
  do { m <- findMacro s;
       return
       $ case m of {
           Just j -> True
           Nothing -> False } }
In an equation for `macroexpand2':
    macroexpand2 s
      = do { m <- findMacro s;
             return
             $ case m of {
                 Just j -> True
                 Nothing -> False } }

所以,这是我对 freer 内部结构的理解用完的地方,我有问题:
  • 为什么会出现重叠实例?我不明白这是从哪里来的。
  • IncoherentInstances 实际上是做什么的?自动选择听起来很可能会导致难以调试的错误。
  • 我如何在另一个函数中实际使用 findMacro?

  • 干杯!

    最佳答案

    可扩展效果的类型推断在历史上一直很糟糕。让我们看一些例子:

    {-# language TypeApplications #-}
    
    -- mtl
    import qualified Control.Monad.State as M
    
    -- freer
    import qualified Control.Monad.Freer as F
    import qualified Control.Monad.Freer.State as F
    
    -- mtl works as usual
    test1 = M.runState M.get 0
    
    -- this doesn't check
    test2 = F.run $ F.runState F.get 0  
    
    -- this doesn't check either, although we have a known
    -- monomorphic state type
    test3 = F.run $ F.runState F.get True
    
    -- this finally checks
    test4 = F.run $ F.runState (F.get @Bool) True
    
    -- (the same without TypeApplication)
    test5 = F.run $ F.runState (F.get :: F.Eff '[F.State Bool] Bool) True
    

    我将尝试解释一般问题并提供最少的代码说明。代码的独立版本可以是 found here .

    在最基本的层面上(不考虑优化的表示),Eff定义如下:
    {-# language
      GADTs, DataKinds, TypeOperators, RankNTypes, ScopedTypeVariables,
      TypeFamilies, DeriveFunctor, EmptyCase, TypeApplications,
      UndecidableInstances, StandaloneDeriving, ConstraintKinds,
      MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
      AllowAmbiguousTypes, PolyKinds
      #-}
    
    import Control.Monad
    
    data Union (fs :: [* -> *]) (a :: *) where
      Here  :: f a -> Union (f ': fs) a
      There :: Union fs a -> Union (f ': fs) a
    
    data Eff (fs :: [* -> *]) (a :: *) =
      Pure a | Free (Union fs (Eff fs a))
    
    deriving instance Functor (Union fs) => Functor (Eff fs)  
    

    换句话说,Eff是一个来自仿函数列表的联合的自由 monad。 Union fs a表现得像一个 n 元 Coproduct .二进制 Coproduct就像 Either对于两个仿函数:
    data Coproduct f g a = InL (f a) | InR (g a)
    

    相比之下,Union fs a让我们从仿函数列表中选择一个仿函数:
    type MyUnion = Union [[], Maybe, (,) Bool] Int
    
    -- choose the first functor, which is []
    myUnion1 :: MyUnion
    myUnion1 = Here [0..10]
    
    -- choose the second one, which is Maybe
    myUnion2 :: MyUnion
    myUnion2 = There (Here (Just 0))
    
    -- choose the third one
    myUnion3 :: MyUnion
    myUnion3 = There (There (Here (False, 0)))
    

    让我们实现 State效果为例。首先,我们需要有一个 Functor Union fs 的实例, 自 Eff只有一个 Monad实例如果 Functor (Union fs) .
    Functor (Union '[])很简单,因为空联合没有值:
    instance Functor (Union '[]) where
      fmap f fs = case fs of {} -- using EmptyCase
    

    否则,我们在联合前添加一个仿函数:
    instance (Functor f, Functor (Union fs)) => Functor (Union (f ': fs)) where
      fmap f (Here fa) = Here (fmap f fa)
      fmap f (There u) = There (fmap f u)
    

    现在State定义和运行者:
    run :: Eff '[] a -> a
    run (Pure a) = a
    
    data State s k = Get (s -> k) | Put s k deriving Functor
    
    runState :: forall s fs a. Functor (Union fs) => Eff (State s ': fs) a -> s -> Eff fs (a, s)
    runState (Pure a)                 s = Pure (a, s)
    runState (Free (Here (Get k)))    s = runState (k s) s
    runState (Free (Here (Put s' k))) s = runState k s'
    runState (Free (There u))         s = Free (fmap (`runState` s) u)
    

    我们已经可以开始编写和运行我们的 Eff程序,虽然我们缺乏所有的糖和便利:
    action1 :: Eff '[State Int] Int
    action1 =
      Free $ Here $ Get $ \s ->
      Free $ Here $ Put (s + 10) $
      Pure s
    
    -- multiple state
    action2 :: Eff '[State Int, State Bool] ()
    action2 =
      Free $ Here $ Get $ \n ->            -- pick the first effect
      Free $ There $ Here $ Get $ \b ->    -- pick the second effect
      Free $ There $ Here $ Put (n < 10) $ -- the second again
      Pure ()
    

    现在:
    > run $ runState action1 0
    (0,10)
    > run $ (`runState` False) $ (`runState` 0) action2
    (((),0),True)
    

    这里只有两个必不可少的东西。

    第一个是 Eff 的 monad 实例这让我们可以使用 do - 符号代替 FreePure ,并且还让我们使用许多多态一元函数。我们将在这里跳过它,因为它写起来很简单。

    第二个是从效果列表中选择效果的推理/重载。以前我们需要写Here x为了选择第一个效果,There (Here x)选择第二个,依此类推。相反,我们想在效果列表中编写多态的代码,所以我们必须指定的是一些效果是列表的一个元素,并且一些隐藏的类型类魔法将插入适当数量的 There -s。

    我们需要一个 Member f fs可以注入(inject)的类 f a -s 进入 Union fs a -s 当 ffs 的一个元素.从历史上看,人们以两种方式实现它。

    一、直接与OverlappingInstances :
    class Member (f :: * ->  *) (fs :: [* -> *]) where
      inj :: f a -> Union fs a
    
    instance Member f (f ': fs) where
      inj = Here
    
    instance {-# overlaps #-} Member f fs => Member f (g ': fs) where
      inj = There . inj
    
    -- it works
    injTest1 :: Union [[], Maybe, (,) Bool] Int
    injTest1 = inj [0]
    
    injTest2 :: Union [[], Maybe, (,) Bool] Int
    injTest2 = inj (Just 0)
    

    其次,间接地,通过首先计算f的索引在 fs使用类型系列,然后实现 inj具有非重叠类,由 f 指导-s 计算索引。这通常被认为更好,因为人们往往不喜欢重叠的实例。
    data Nat = Z | S Nat
    
    type family Lookup f fs where
      Lookup f (f ': fs) = Z
      Lookup f (g ': fs) = S (Lookup f fs)
    
    class Member' (n :: Nat) (f :: * -> *) (fs :: [* -> *]) where
      inj' :: f a -> Union fs a
    
    instance fs ~ (f ': gs) => Member' Z f fs where
      inj' = Here
    
    instance (Member' n f gs, fs ~ (g ': gs)) => Member' (S n) f fs where
      inj' = There . inj' @n
    
    type Member f fs = Member' (Lookup f fs) f fs
    
    inj :: forall fs f a. Member f fs => f a -> Union fs a
    inj = inj' @(Lookup f fs)
    
    -- yay
    injTest1 :: Union [[], Maybe, (,) Bool] Int
    injTest1 = inj [0]
    
    freer库使用第二种解决方案,而 extensible-effects第一个用于 7.8 之前的 GHC 版本,第二个用于较新的 GHC-s。

    无论如何,两种解决方案都具有相同的推理限制,即我们几乎总是可以Lookup只有具体的单态类型,而不是包含类型变量的类型。 ghci 中的示例:
    > :kind! Lookup Maybe [Maybe, []]
    Lookup Maybe [Maybe, []] :: Nat
    = 'Z
    

    这是有效的,因为在 Maybe 中都没有类型变量或 [Maybe, []] .
    > :kind! forall a. Lookup (Either a) [Either Int, Maybe]
    forall a. Lookup (Either a) [Either Int, Maybe] :: Nat
    = Lookup (Either a) '[Either Int, Maybe]
    

    这个卡住了,因为 a类型变量块减少。
    > :kind! forall a. Lookup (Maybe a) '[Maybe a]
    forall a. Lookup (Maybe a) '[Maybe a] :: Nat
    = Z
    

    这是有效的,因为我们对任意类型变量的唯一了解是它们等于自身,并且 a等于 a .

    通常,类型族缩减会卡在变量上,因为约束求解可能会在以后将它们细化为不同的类型,因此 GHC 无法对它们做出任何假设(除了等于它们自己)。基本上相同的问题出现在 OverlappingInstances 上。实现(尽管没有任何类型系列)。

    让我们重温 freer鉴于此。
    import Control.Monad.Freer
    import Control.Monad.Freer.State
    
    test1 = run $ runState get 0 -- error
    

    GHC 知道我们有一个单一效果的堆栈,因为 run工作于 Eff '[] a .它也知道那个效果一定是State s .但是当我们写 get ,GHC只知道它有一个State t一些新鲜的效果t变量,以及 Num t必须保持,所以当它试图计算 freer 时相当于 Lookup (State t) '[State s] ,它会卡在类型变量上,并且任何进一步的实例解析都会在卡住的类型系列表达式上绊倒。另一个例子:
    foo = run $ runState get False -- error
    

    这也失败了,因为 GHC 需要计算 Lookup (State s) '[State Bool] ,虽然我们知道状态必须是 Bool ,这仍然因为 s 卡住了多变的。
    foo = run $ runState (modify not) False -- this works
    

    这是有效的,因为状态类型为 modify not可以解析到Bool , 和 Lookup (State Bool) '[State Bool]减少。

    现在,经过这么大的弯路,我将在您的帖子末尾回答您的问题。
  • Overlapping instances不表示任何可能的解决方案,只是一个类型错误工件。我需要更多的代码上下文来确定它究竟是如何产生的,但我确定它不相关,因为一旦 Lookup卡住了,案子就无望了。
  • IncoherentInstances也无关紧要,也无济于事。我们需要一个具体的效果位置索引才能为程序生成代码,如果Lookup我们不能凭空拉出一个索引。卡住。
  • findMacro 的问题是它有State状态内的类型变量的影响。每当您想使用 findMacro你必须确保 vw Scope 的参数和 Global是已知的具体类型。您可以通过类型注释来做到这一点,或者更方便的是您可以使用 TypeApplications ,然后写 findMacro @Int @Int用于指定 v = Intw = Int .如果您有 findMacro在多态函数中,您需要启用 ScopedTypeVariables , 绑定(bind) vw使用 forall v w.该函数的注解,然后写 findMacro @v @w当你使用它时。您还需要启用 {-# language AllowAmbiguousTypes #-}用于多晶vw (如评论中所指出的)。我认为虽然在 GHC 8 中启用它是一个合理的扩展,连同 TypeApplications .


  • 附录:

    然而,幸运的是,新的 GHC 8 功能让我们修复了可扩展效果的类型推断,我们可以推断出一切mtl可以,还有一些东西mtl处理不了。新的类型推断对于效果的排序也是不变的。

    我有一个 minimal implementation here以及一些例子。但是,它尚未在我所知道的任何效果库中使用。我可能会写一篇关于它的文章,并做一个拉取请求以将它添加到 freer .

    关于haskell - 如何在 haskell 中组合 'freer' 效果?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/38993017/

    相关文章:

    haskell - 如何用writeFile将每个[String]写入haskell中的文件?

    haskell - 如何在应用类型默认规则的 ghci 中打印多态函数(或值)的类型?

    haskell - "const id"的行为

    haskell - 当 Exc 是成员时 Control.Eff 的 MonadPlus 实例

    haskell - 如何产生无限二叉树?

    list - 如何将函数应用于 haskell 中的列表?