haskell - 递归类型族

Question

我正在试验 mtl - 允许我提升 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 的表面语法使得明确说明哪些类型应该实例化 forall 变得相当尴尬。 ，即使你知道你想要什么。这是 Damas-Milner 完整性的美好旧时光的遗产，当时有趣到需要显式键入的想法被简单地禁止了。

假设我们可以使用 Agda 风格的 f {a = x} 在模式和表达式中显式地显示类型应用程序。表示法，选择性地访问与 a 对应的类型参数在 f 的类型签名中.您的

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

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

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

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 的现状是基于一种文化假设，即“类型推断就足够了”，这种假设已经偏离了一代人的轨道，但仍然以某种方式持续存在。