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

Question

我认为我的问题通过简单的代码很容易理解，但另一方面，我不确定答案!直观地说，我想要做的是给定一个类型 [*] 和一些依赖类型 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(法线和指数都描述 double 型)，选择一个分布只是为了修复类型似乎很愚蠢。我真正想定义的是定义一个简单的异构列表

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 是最通用的。在这一点上，我的问题不仅仅是回答。

Answer 1

这是 DataKinds 的解决方案.我们需要更多的扩展，FlexibleContexts和 FlexibleInstances .

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

我们将继续使用您的 Distribution类作为依赖类型的示例

class Distribution m where
    type SampleSpace m :: *

借用 the TypeMap example you found ， 我们会有

type family   TypeMap (f :: * -> *) (xs :: [*]) :: [*]
type instance TypeMap t             '[]         =  '[]
type instance TypeMap t             (x ': xs)   =  t x ': TypeMap t xs

在类型列表中，我们希望能够 TypeMap SampleSpace .不幸的是，我们不能部分应用类型族中的类型，因此我们将专门化 TypeMap为 SampleSpace .这里的想法是 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 的异构列表派生实例s。注意 ': 右边的类型用途 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