小编ale*_*404的帖子

所以我理解了Rank2Types,但是当我尝试以下内容时

{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}

import Data.Machine

f :: IO (Process a a)
f = return . auto $ id

GHC咳嗽出来

Couldn't match type `MachineT m0 (Is a0) a0'
              with `forall (m :: * -> *). Monad m => MachineT m (Is a) a'
Expected type: IO (Process a a)
  Actual type: IO (MachineT m0 (Is a0) a0)
In the expression: return . auto $ id
In an equation for `f': f = return . auto $ id
Failed, …

我认为从简单的代码中理解我的问题相当简单,但另一方面,我不确定答案!直觉上,我想要做的是给出一个类型列表[*]和一些依赖类型Foo,生成类型[Foo*].也就是说,我想在基类型上"映射"依赖类型.

首先,我正在使用以下扩展

{-# LANGUAGE TypeOperators,DataKinds,GADTs,TypeFamilies #-}

假设我们有一些依赖类型

class Distribution m where
    type SampleSpace m :: *

它表征了一些概率分布的样本空间.如果我们想要在可能异构的值上定义产品分布,我们可能会写类似的东西

data PDistribution (ms :: [*]) where
    DNil :: PDistribution ('[])
    (:*:) :: Distribution m => m -> (PDistribution ms) -> PDistribution (m ': ms)

并补充它

data PSampleSpace (m :: [*]) where
    SSNil :: PSampleSpace ('[])
    (:+:) :: Distribution m => SampleSpace m -> (PSampleSpace ms) -> PSampleSpace (m ': ms)

这样我们就可以定义了

instance Distribution (PDistribution ms) where
    type SampleSpace (PDistribution ms) = PSampleSpace ms …