haskell - 递归类型族

Question

我正在尝试一个mtl-style 类，它允许我将Pipe组合提升到外部 monad 上。为此，我必须定义类型的哪两个变量是Pipe组合的域和共域。

我尝试使用关联类型族方法，但无济于事：

{-# LANGUAGE TypeFamilies #-}

import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data Pipe a b m r = Pipe { unPipe :: FreeT (PipeF a b) m r }

class MonadPipe m where
    type C a b (m :: * -> *) :: * -> *
    idT :: C a a m r
    (<-<) :: C b c m r -> C a b m r -> C a c m r

instance (Monad m) => MonadPipe (Pipe i o m) where
    type C a b (Pipe i o m) = Pipe a b m
    idT = Pipe idP
    (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2)

instance (MonadPipe m) => MonadPipe (StateT s m) where
    type C a b (StateT s m) = StateT s (C a b m)
    idT = StateT $ \s -> idT
    (StateT f1) <-< (StateT f2) = StateT $ \s -> f1 s <-< f2 s

但是，上面的代码不进行类型检查。GHC 给出以下错误：

family.hs:23:15:
    Could not deduce (C a a m ~ C a0 a0 m0)
    from the context (MonadPipe m)
      bound by the instance declaration at family.hs:21:14-52
    NB: `C' is a type function, and may not be injective
    Expected type: C a a (StateT s m) r
      Actual type: StateT s (C a0 a0 m0) r
    In the expression: StateT $ \ s -> idT
    In an equation for `idT': idT = StateT $ \ s -> idT
    In the instance declaration for `MonadPipe (StateT s m)'

family.hs:24:10:
    Could not deduce (C b c m ~ C b0 c0 m1)
    from the context (MonadPipe m)
      bound by the instance declaration at family.hs:21:14-52
    NB: `C' is a type function, and may not be injective
    Expected type: C b c (StateT s m) r
      Actual type: StateT s (C b0 c0 m1) r
    In the pattern: StateT f1
    In an equation for `<-<':
        (StateT f1) <-< (StateT f2) = StateT $ \ s -> f1 s <-< f2 s
    In the instance declaration for `MonadPipe (StateT s m)'

<<Two other errors for 'C a b m' and 'C a c m'>>

我很难理解为什么类型不会统一，特别是对于idT定义，因为我希望内部idT被普遍量化，a所以它会匹配外部。

所以我的问题是这是否可以用类型族来实现，如果不能用类型族来实现，它怎么能实现？

Answer 1

默认情况下，类型推断是一种猜谜游戏。Haskell 的表面语法使得明确哪些类型应该实例化 a 变得相当尴尬forall，即使您知道自己想要什么。这是 Damas-Milner 完整性的美好旧时光的遗产，当时有趣到需要显式键入的想法被简单地禁止了。

假设我们可以使用 Agda 样式的符号在模式和表达式中显式地显示类型应用程序，f {a = x}选择性地访问. 您的af

idT = StateT $ \ s -> idT

应该是指

idT {a = a}{m = m} = StateT $ \ s -> idT {a = a}{m = m}

所以左边有类型C a a (StateT s m) r，右边有类型StateT s (C a a m) r，在类型家族的定义上是相等的，欢乐辐射世界。但这不是你写的意思。调用多态事物的“变量规则”要求每个forall都用一个新的存在类型变量实例化，然后通过统一解决。所以你的代码意味着什么

idT {a = a}{m = m} = StateT $ \ s -> idT {a = a'}{m = m'}
  -- for a suitably chosen a', m'

在计算类型族之后，可用的约束是

C a a m ~ C a' a' m'

但这并没有简化，也不应该简化，因为没有理由假设C是单射的。令人抓狂的是，机器比你更关心找到最通用解决方案的可能性。您已经想到了一个合适的解决方案，但问题是在默认假设是猜测时实现通信。

有许多策略可以帮助您摆脱困境。一种是改用数据族。Pro：内射性没问题。缺点：构造函数。（警告，以下未经检验的猜测。）

class MonadPipe m where
  data C a b (m :: * -> *) r
  idT :: C a a m r
  (<-<) :: C b c m r -> C a b m r -> C a c m r

instance (MonadPipe m) => MonadPipe (StateT s m) where
  data C a b (StateT s m) r = StateTPipe (StateT s (C a b m) r)
  idT = StateTPipe . StateT $ \ s -> idT
  StateTPipe (StateT f) <-< StateTPipe (StateT g) =
    StateTPipe . StateT $ \ s - f s <-< g s

另一个缺点是生成的数据系列不是自动单子的，也不是很容易解包或以统一的方式使其成为单子。

我正在考虑为这些东西尝试一种模式，让你保留你的类型系列，但为它定义一个新类型包装器

newtype WrapC a b m r = WrapC {unwrapC :: C a b m r}

然后WrapC在操作的类型中使用以使类型检查器保持在正确的轨道上。我不知道这是否是一个好策略，但我计划在这些日子里找出答案。

更直接的策略是使用代理、幻象类型和作用域类型变量（尽管本示例不需要它们）。（再次，猜测警告。）

data Proxy (a :: *) = Poxy
data ProxyF (a :: * -> *) = PoxyF

class MonadPipe m where
  data C a b (m :: * -> *) r
  idT :: (Proxy a, ProxyF m) -> C a a m r
  ...

instance (MonadPipe m) => MonadPipe (StateT s m) where
  data C a b (StateT s m) r = StateTPipe (StateT s (C a b m) r)
  idT pp = StateTPipe . StateT $ \ s -> idT pp

这只是使类型应用程序显式化的一种糟糕方式。请注意，有些人使用a它自己而不是作为参数Proxy a传递undefined，因此无法在类型中将代理标记为这样，并且依赖于不会意外评估它。最近的进展PolyKinds可能至少意味着我们只能拥有一种多态幻象代理类型。至关重要的是，Proxy类型构造函数是单射的，所以我的代码实际上是在说“这里和那里的参数相同”。

但有时我希望我可以在源代码中降到 System FC 级别，或者以其他方式表达明确的手动覆盖以进行类型推断。这样的事情在依赖类型社区中是相当标准的，没有人会想象机器可以在没有任何推动的情况下解决所有问题，或者隐藏的参数没有任何值得检查的信息。一个函数的隐藏参数可以在使用站点被抑制，但需要在定义中明确表示，这是很常见的。Haskell 的现状是基于一种文化假设，即“类型推断就足够了”，这种假设已经偏离了一代人的轨道，但仍然以某种方式持续存在。

Answer 2

编辑了三遍：数据系列版本见底部。并将 GADT 版本更改为删除 m。

让我猜猜：剩菜？

让我先介绍一下类型错误，即解决方案。

The class defines :
type C a0 b0 m  where a0 and b0 are fresh.
idT :: C a a m r, where a and r are fresh. 

The idT in the (Pipe i o m0) instance is okay by what I think is the logic:
LHS is idT :: C a0 a0 (Pipe i o m0) r0 which becomes Pipe a0 a0 m0 r0
RHS is Pipe idP :: Pipe a1 a1 m1 r1 starts fresh
And then these unify
because Pipe is a data constructor.

The idT in the MonadPipe m0 => (StateT s0 m0) instance:
LHS is idT :: C a0 a0 (StateT s0 m0) which becomes StateT s0 (C a0 a0 m0)
RHS is StateT (\s -> idT) :: StateT s1 m1 r1
Some unification seems to happen...
RHS is StateT (\s -> idT) :: StateT s1 (C a0 a0 m0) r1
  where expression idT :: MonadPipe m1 => (C a2 a2 m2) r2 starts fresh
        context of idT :: (C a0 a0 m0) (a1, s1)
And then (C a0 a0 m0) does not unify with (C a1 a2 m2)
because C is a type constructor.

newtype如果类型族成为数据族，您之前制作 Category 实例的方法可能在这里有效。

编辑：您更改参数的顺序和 newtype StateT 来解决它：

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}

import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data Pipe m a b r = Pipe { unPipe :: FreeT (PipeF a b) m r }

newtype StatePipe s mp a b r = SP (StateT s (mp a b) r)

class MonadPipe mp where
    idT :: mp a a r
    (<-<) :: mp b c r -> mp a b r -> mp a c r

instance (Monad m) => MonadPipe (Pipe m) where
    idT = Pipe idP
    (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2)

instance (MonadPipe mp) => MonadPipe (StatePipe s mp) where
     idT = SP . StateT $ \s -> idT
     (SP (StateT f1)) <-< (SP (StateT f2)) = SP . StateT $ \s -> f1 s <-< f2 s

虽然 MonadTrans 现在可能很伤心。另一种方法通过使用 GADT 来保持参数顺序，也许可以更清楚地表达您要构建的内容：

{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleInstances #-}
import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data Pipe s a b m r where
  FPipe :: { unPipe :: FreeT (PipeF a b) m r } -> Pipe () a b m r
  LPipe :: StateT s1 (Pipe s2 a b m) r -> Pipe (s1,s2) a b m r

class MonadPipe s where
    idT :: Monad m => Pipe s a a m r
    (<-<) :: Monad m => Pipe s b c m r -> Pipe s a b m r -> Pipe s a c m r

instance MonadPipe () where
    idT  = FPipe idP
    (FPipe p1) <-< (FPipe p2) = FPipe (p1 <+< p2)

instance MonadPipe s2 => MonadPipe (s1,s2) where
    idT  = LPipe (StateT $ \s -> idT)
    (LPipe (StateT f1)) <-< (LPipe (StateT f2)) = 
       LPipe (StateT $ \s1 -> (f1 s1 <-< f2 s1))

我可以把它翻译成一个更好的数据系列吗？

{-# LANGUAGE TypeFamilies #-}
import Control.Monad.Trans.Free
import Control.Monad.Trans.State
import Control.Pipe hiding (Pipe)

data family GPipe s :: * -> * -> (* -> *) -> * -> *
newtype instance GPipe () a b m r = Pipe { unPipe :: FreeT (PipeF a b) m r }
newtype instance GPipe (s1,s2) a b m r = LPipe ( StateT s1 (GPipe s2 a b m) r )

class MonadPipe s where
  idT :: Monad m => GPipe s a a m r
  (<-<) :: Monad m => GPipe s b c m r -> GPipe s a b m r -> GPipe s a c m r

instance MonadPipe () where
  idT = Pipe idP
  (Pipe p1) <-< (Pipe p2) = Pipe (p1 <+< p2)

instance MonadPipe s2 => MonadPipe (s1,s2) where
  idT = LPipe (StateT (\s -> idT))
  (LPipe (StateT f1)) <-< (LPipe (StateT f2)) = LPipe (StateT (\s -> f1 s <-< f2 s))