递归类型系列

Question

我正在尝试一个mtl允许我Pipe在外部monad 上提升构图的类式.为此,我必须定义该类型的哪两个变量是Pipe组合的域和codomain .

我尝试使用相关的类型系列方法,但无济于事:

{-# 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是单射的.令人抓狂的是,机器比你更关心找到最通用解决方案的可能性.您已经有了一个合适的解决方案,但问题是当默认假设是猜测时实现通信.

有许多策略可以帮助您解决这个问题.一种是使用数据系列.亲:注意力没问题.Con:结构.(警告,未经测试的猜测如下.)

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

另一个问题是结果数据族不是自动monadic,也不是很容易打开它或以统一的方式使其monadic.

我正在考虑为你保留类型族的这些东西尝试一个模式,但为它定义一个newtype包装器

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类型构造函数是单射的,所以我的代码实际上是在说"与此相同的参数".

但有时我希望我可以在源代码中降低到系统FC级别,或者以其他方式表达类型推断的明确手动覆盖.在依赖类型的社区中,这样的事情是非常标准的,没有人会想象机器可以在没有轻推的情况下解决所有问题,或者隐藏的参数没有值得检查的信息.很常见的是,函数的隐藏参数可以在使用站点被抑制,但需要在定义中明确.Haskell目前的情况是基于一种文化假设,即"类型推断就足够了",这种假设在一代人的时间里已经脱轨,但仍然存在.

Answer 2

编辑三次：请参阅底部的数据系列版本。并将 GADT 版本更改为 drop 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如果类型系列变成数据系列，您之前创建类别实例的方法可能在这里起作用。

编辑：您改变参数的顺序和新类型 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))