15

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

我目前只使用StateandFresh效果。我正在使用两种状态,我的效果跑步者看起来像这样:

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在编译这段代码时尝试使用(我不想检查一个更自由的分支并玩),看看它是否会给我一个关于发生了什么的线索。它没有:

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 内部结构的理解用尽的地方,我有疑问:

  1. 为什么会有重叠实例?我不明白这是从哪里来的。
  2. IncoherentInstances实际上做了什么?自动选择听起来很可能会导致难以调试的错误。
  3. 我如何在另一个函数中实际使用 findMacro?

干杯!

4

1 回答 1

18

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

{-# 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

我将尝试解释一般问题并提供最少的代码说明。可以在此处找到该代码的独立版本。

在最基本的级别(忽略优化表示),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是一个来自函子列表联合的自由单子。Union fs a表现得像一个 n-ary 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效果为例。首先,我们需要有一个Functorfor 的实例Union fs,因为Eff只有一个Monadif 的实例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)

这里只有两个基本缺失的东西。

第一个是 monad 实例,Eff它允许我们使用do-notation 代替Freeand Pure,还允许我们使用许多多态 monadic 函数。我们将在这里跳过它,因为它很容易编写。

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

我们需要一个Member f fs可以将 -s 注入f a-s的类,Union fs af它是 .s 的一个元素时fs。从历史上看,人们以两种方式实施它。

首先,直接使用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)

其次,间接地,通过首先使用类型族计算fin的索引,然后在-s 计算索引的指导下使用非重叠类来实现。这通常被认为更好,因为人们倾向于不喜欢重叠的实例。fsinjf

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这是有效的,因为or中没有类型变量[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]减少。

现在,经过这么大的弯路,我将在您的帖子末尾解决您的问题。

  1. Overlapping instances并不表示任何可能的解决方案,只是一个类型错误工件。我需要更多的代码上下文来确定它是如何产生的,但我确信它不相关,因为一旦Lookup卡住,情况就会变得毫无希望。

  2. IncoherentInstances也无关紧要,也无济于事。Lookup我们需要一个具体的效果位置索引才能为程序生成代码,如果卡住了我们不能凭空捏造一个索引。

  3. 问题findMacro在于它对State状态内的类型变量有影响。每当您想使用findMacro时,您必须确保 和 的和v参数w是已知的具体类型。您可以通过类型注释来做到这一点,或者更方便的是您可以使用, 并编写来指定and 。如果你有一个多态函数,你需要为该函数启用、绑定和使用注解,并在使用时编写。您还需要启用多态或ScopeGlobalTypeApplicationsfindMacro @Int @Intv = Intw = IntfindMacroScopedTypeVariablesvwforall v w.findMacro @v @w{-# language AllowAmbiguousTypes #-}vw(正如评论中指出的那样)。我认为尽管在 GHC 8 中启用它是一个合理的扩展,与TypeApplications.


附录:

但是,幸运的是,GHC 8 的新功能让我们修复了类型推断以获得可扩展的效果,我们可以推断出所有mtl可以推断的东西,也可以推断出一些mtl无法处理的东西。新的类型推断对于效果的顺序也是不变的。

我在这里有一个最小的实现以及一些示例。但是,它还没有在我知道的任何效果库中使用。我可能会写一篇关于它的文章,并做一个拉取请求以便将它添加到freer.

于 2016-08-17T14:16:44.250 回答