我认为从简单的代码中理解我的问题相当简单,但另一方面,我不确定答案!直觉上,我想要做的是给出一个类型列表[*]和一些依赖类型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
现在这一切都相当不错,除了PSampleSpace的类型将导致一些问题.特别是,如果我们想直接构建PSampleSpace,例如
ss = True :+: 3.0 :+: SNil
我们必须明确地给它一组分布,它们产生它或者遇到单态限制.此外,由于两个发行版当然可以共享一个SampleSpace(normals和Exponentials都描述双打),因此选择一个发行版来修复类型似乎很愚蠢.我真正想要定义的是定义一个简单的异构列表
data HList (xs :: [*]) where Nil :: HList ('[]) (:+:) :: x -> (HList xs) -> HList (x ': xs)
写点东西
instance distribution (Pdistribution (m ': ms)) where type SampleSpace (Pdistribution (m ': ms)) = HList (SampleSpace m ': mxs)
其中mxs已经以某种方式转换为我想要的SampleSpaces列表.当然,最后一点代码不起作用,我不知道如何解决它.干杯!
编辑
class distribution m => Generative m where generate :: m -> Rand (SampleSpace m)
即使它似乎应该键入检查,以下
instance Generative (HList '[]) where generate Nil = return Nil instance (Generative m,Generative (HList ms)) => Generative (HList (m ': ms)) where generate (m :+: ms) = do x <- generate m (x :+:) <$> generate ms
才不是. GHC抱怨它
Could not deduce (SampleSpace (HList xs) ~ HList (SampleSpaces xs))
现在我可以使用我的Pdistribution GADT了,因为我在子发行版上强制所需的类型类.
最终编辑
解决方法
为什么要将分发产品列入清单?将普通元组(两种类型的产品)代替:*:?
{-# LANGUAGE TypeOperators,TypeFamilies #-} class distribution m where type SampleSpace m :: * data (:+:) a b = ProductSampleSpaceWhatever deriving (Show) instance (distribution m1,distribution m2) => distribution (m1,m2) where type SampleSpace (m1,m2) = SampleSpace m1 :+: SampleSpace m2 data normaldistribution = normaldistributionWhatever instance distribution normaldistribution where type SampleSpace normaldistribution = Doubles data Exponentialdistribution = ExponentialdistributionWhatever instance distribution Exponentialdistribution where type SampleSpace Exponentialdistribution = Doubles data Doubles = DoublesSampleSpaceWhatever example :: SampleSpace (normaldistribution,Exponentialdistribution) example = ProductSampleSpaceWhatever example' :: Doubles :+: Doubles example' = example -- Just to prove it works: main = print example'
元组树和列表之间的区别在于元组的树是类似岩浆的(有一个二元运算符),而列表是类似于monoid的(有一个二元运算符,一个标识,运算符是关联的).所以没有单一的,选择的DNil是身份,而且类型不会强迫我们抛弃(normaldistribution:*:Exponentialdistribution)之间的区别:*:Binarydistribution和normaldistribution:*