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

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 (Normals和指数都描述双数)，选择一个发行版来修复这个类型似乎很愚蠢。我真正想要定义的是定义一个简单的异构列表

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)

尽管它似乎应该键入check，但如下所示

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

为什么要把发行版的产品从列表中去掉？一个普通的元组(两种类型的产品)能代替:*:吗？

{-# 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] 

Answer 2

下面是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的异构列表的实例了，注意':右侧的类型是如何使用SampleSpaces的，我们在上面定义了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