haskell – 在类型列表上映射依赖类型

我认为从简单的代码中理解我的问题相当简单,但另一方面,我不确定答案！直觉上,我想要做的是给出一个类型列表[*]和一些依赖类型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了,因为我在子发行版上强制所需的类型类.

最终编辑

所以有几种方法可以解决这个问题. TypeList是最常用的.我的问题不仅仅是在这一点上回答.

为什么要将分发产品列入清单？将普通元组(两种类型的产品)代替：*：？

{-# 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：*