我认为我的问题从简单的代码中很容易理解，但另一方面，我不确定答案！直观地说，我想做的是给出一个类型 [*] 和一些依赖类型 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（正态和指数都描述了双精度），因此选择一个分布来修复类型似乎很愚蠢。我真正想定义的是定义一个简单的异构列表
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 以某种方式转换为我想要的样本空间列表。当然，最后一点代码不起作用，我不知道如何修复它。干杯！
编辑
就像我所提出的解决方案问题的一个坚实的例子一样，假设我有这样的类
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'
组树和列表之间的区别在于，元组树是岩浆状的（有一个二元运算符），而列表是幺半群的（有一个二元运算符，一个恒等式，运算符是关联的）。因此，没有单一的，挑出的DNil是身份，类型不会迫使我们放弃(NormalDistribution :*: ExponentialDistribution) :*: BinaryDistribution和NormalDistribution :*: (ExponentialDistribution :*: BinaryDistribution)之间的区别。
编辑
下面的代码使类型列表具有关联运算符 TypeListConcat 和标识 TypeListNil 。除了提供的两种类型之外，没有什么可以保证不会有其他TypeList实例。我无法让TypeOperators语法适用于我想要的一切。
{-# LANGUAGE TypeFamilies,MultiParamTypeClasses,FlexibleInstances,TypeOperators #-}
-- Lists of types
-- The class of things where the end of them can be replaced with something
-- The extra parameter t combined with FlexibleInstances lets us get away with essentially
-- type TypeListConcat :: * -> *
-- And instances with a free variable for the first argument
class TypeList l a where
type TypeListConcat l a :: *
typeListConcat :: l -> a -> TypeListConcat l a
-- An identity for a list of types. Nothing guarantees it is unique
data TypeListNil = TypeListNil
deriving (Show)
instance TypeList TypeListNil a where
type TypeListConcat TypeListNil a = a
typeListConcat TypeListNil a = a
-- Cons for a list of types, nothing guarantees it is unique.
data (:::) h t = (:::) h t
deriving (Show)
infixr 5 :::
instance (TypeList t a) => TypeList (h ::: t) a where
type TypeListConcat (h ::: t) a = h ::: (TypeListConcat t a)
typeListConcat (h ::: t) a = h ::: (typeListConcat t a)
-- A Distribution instance for lists of types
class Distribution m where
type SampleSpace m :: *
instance Distribution TypeListNil where
type SampleSpace TypeListNil = TypeListNil
instance (Distribution m1, Distribution m2) => Distribution (m1 ::: m2) where
type SampleSpace (m1 ::: m2) = SampleSpace m1 ::: SampleSpace m2
-- Some types and values to play with
data NormalDistribution = NormalDistributionWhatever
instance Distribution NormalDistribution where
type SampleSpace NormalDistribution = Doubles
data ExponentialDistribution = ExponentialDistributionWhatever
instance Distribution ExponentialDistribution where
type SampleSpace ExponentialDistribution = Doubles
data BinaryDistribution = BinaryDistributionWhatever
instance Distribution BinaryDistribution where
type SampleSpace BinaryDistribution = Bools
data Doubles = DoublesSampleSpaceWhatever
deriving (Show)
data Bools = BoolSampleSpaceWhatever
deriving (Show)
-- Play with them
example1 :: TypeListConcat (Doubles ::: TypeListNil) (Doubles ::: Bools ::: TypeListNil)
example1 = (DoublesSampleSpaceWhatever ::: TypeListNil) `typeListConcat` (DoublesSampleSpaceWhatever ::: BoolSampleSpaceWhatever ::: TypeListNil)
example2 :: TypeListConcat (Doubles ::: Doubles ::: TypeListNil) (Bools ::: TypeListNil)
example2 = example2
example3 :: Doubles ::: Doubles ::: Bools ::: TypeListNil
example3 = example1
example4 :: SampleSpace (NormalDistribution ::: ExponentialDistribution ::: BinaryDistribution ::: TypeListNil)
example4 = example3
main = print example4
编辑 - 使用 TypeList s 的代码
下面是一些类似于您在编辑中添加的代码的代码。我不知道Rand应该是什么，所以我编造了别的东西。
-- Distributions with sampling
class Distribution m => Generative m where
generate :: m -> StdGen -> (SampleSpace m, StdGen)
instance Generative TypeListNil where
generate TypeListNil g = (TypeListNil, g)
instance (Generative m1, Generative m2) => Generative (m1 ::: m2) where
generate (m ::: ms) g =
let
(x, g') = generate m g
(xs, g'') = generate ms g'
in (x ::: xs, g'')
-- Distributions with modes
class Distribution m => Modal m where
modes :: m -> [SampleSpace m]
instance Modal TypeListNil where
modes TypeListNil = [TypeListNil]
instance (Modal m1, Modal m2) => Modal (m1 ::: m2) where
modes (m ::: ms) = [ x ::: xs | x <- modes m, xs <- modes ms]
这是
DataKinds的解决方案。我们将需要更多的扩展，FlexibleContexts和FlexibleInstances。
{-# LANGUAGE TypeOperators,DataKinds,GADTs,TypeFamilies,FlexibleInstances,FlexibleContexts #-}
我们将继续使用您的Distribution类作为依赖类型的示例
class Distribution m where
type SampleSpace m :: *
借用您找到的TypeMap示例，我们将有
type family TypeMap (f :: * -> *) (xs :: [*]) :: [*]
type instance TypeMap t '[] = '[]
type instance TypeMap t (x ': xs) = t x ': TypeMap t xs
在类型列表中，我们希望能够TypeMap SampleSpace .遗憾的是，我们无法部分应用类型族中的类型，因此我们将专门针对SampleSpace TypeMap。这里的想法是SampleSpaces = TypeMap SampleSpace
type family SampleSpaces (xs :: [*]) :: [*]
type instance SampleSpaces '[] = '[]
type instance SampleSpaces (x ': xs) = SampleSpace x ': SampleSpaces xs
我们将继续使用您的HList，但为其添加一个Show实例：
data HList (xs :: [*]) where
Nil :: HList '[]
(:+:) :: x -> HList xs -> HList (x ': xs)
infixr 5 :+:
instance (Show x, Show (HList xs)) => Show (HList (x ': xs)) where
showsPrec p (x :+: xs) = showParen (p > plus_prec) $
showsPrec (plus_prec+1) x .
showString " :+: " .
showsPrec (plus_prec) xs
where plus_prec = 5
instance Show (HList '[]) where
show _ = "Nil"
现在我们都准备好为异构Distribution列表派生实例。 请注意':右侧的类型如何使用我们上面定义的SampleSpaces。
instance (Distribution m, Distribution (HList ms)) => Distribution (HList (m ': ms)) where
type SampleSpace (HList (m ': ms)) = HList (SampleSpace m ': SampleSpaces ms)
instance Distribution (HList '[]) where
type SampleSpace (HList '[]) = HList '[]
现在我们可以玩弄它，看看一堆类型是等效的
-- Some types and values to play with
data NormalDistribution = NormalDistributionWhatever
instance Distribution NormalDistribution where
type SampleSpace NormalDistribution = Doubles
data ExponentialDistribution = ExponentialDistributionWhatever
instance Distribution ExponentialDistribution where
type SampleSpace ExponentialDistribution = Doubles
data BinaryDistribution = BinaryDistributionWhatever
instance Distribution BinaryDistribution where
type SampleSpace BinaryDistribution = Bools
data Doubles = DoublesSampleSpaceWhatever
deriving (Show)
data Bools = BoolSampleSpaceWhatever
deriving (Show)
-- Play with them
example1 :: HList [Doubles, Doubles, Bools]
example1 = DoublesSampleSpaceWhatever :+: DoublesSampleSpaceWhatever :+: BoolSampleSpaceWhatever :+: Nil
example2 :: SampleSpace (HList [NormalDistribution, ExponentialDistribution, BinaryDistribution])
example2 = example1
example3 :: SampleSpace (HList [ExponentialDistribution, NormalDistribution, BinaryDistribution])
example3 = example2
main = print example3