创建一个从类型级列表

Question

值的列表我有这样

data TList (ixs :: [*]) (f :: * -> *) where 
    TNil :: TList '[] f 
    (:-:) :: f ix -> TList ixs f -> TList (ix ': ixs) f 

一个类型级列表，我想使用一个现有的生成一个新的从TList。 的想法是有一个函数

genTList :: TList ixs f -> t -> TList ixs g 

其中“T”是一些功能能够构造类型的值“G X”其中“x”是一个类型形成该列表“IXS”。

因此，鉴于

data Foo x 

和（某种）

generate :: forall x . Bar x 

我能得到这样的事情

genTList (Foo Int :-: Foo String) generate = Bar :-: Bar 

所以基本上在每一个项目的 'x'类型列表我想要一个类型'Bar x' 并且还使用无参数const构造它的值因为我知道 'Bar x'没有构造函数参数。

我试图实现一些东西（https://gist.github.com/lolepezy/30820595afd9217083c5ca629e350b55），但它不会typecheck（合理）。

那么我该如何处理这个问题呢？

Answer 1

您定义

class TListGen ixs (g :: * -> *) where 
    genTList :: Proxy ixs -> g ix -> TList ixs g 

但是这意味着该函数的调用者可以选择什么来实例化所有类型的变量，所以还特别如何实例ix。

因此，例如，

genTList (Proxy :: Proxy '[Int, String]) (Just False) 

将是这个函数的类型调用正确，选择g是Maybe和ix是Bool。但这不可能是正确的。我们需要传递一个足够多态的东西，它至少适用于类型级列表中出现的所有元素，或者更好，可用于ix的任何可能选择。这是一个等级2多态类型所实现的：

class TListGen ixs (g :: * -> *) where 
    genTList :: Proxy ixs -> (forall ix . g ix) -> TList ixs g 

这需要RankNTypes语言扩展。

现在调用者只能传递参数类型为g的多态的函数。所以通过Just False将不再工作，但通过Nothing会没事的。

这些案例的定义原则上可以，但实际上您可以删除OVERLAPS附注，甚至是代理参数，因为没有任何重叠，并且可以从结果类型推断出ixs，因为它作为参数出现到TList数据类型：

class TListGen ixs (g :: * -> *) where 
    genTList :: (forall ix . g ix) -> TList ixs g 

instance TListGen '[] g where 
    genTList _ = TNil 

instance TListGen ixs g => TListGen (ix ': ixs) g where 
    genTList g = g :-: genTList g 

现在我们可以尝试使用它：

GHCi> genTList Nothing :: TList '[ Int, String ] Maybe 

不幸的是，这将导致一个错误，因为没有Show instan CE：

• No instance for (Show (TList '[Int, String] Maybe)) 
    arising from a use of ‘print’ 
• In a stmt of an interactive GHCi command: print it 

定义Show实例TList是可能的，但有点棘手。

我不知道这是否是主要的锻炼，但如果你确定只重用代码，那么这一切都是在generics-sop封装。

你TList被称为NP（与论点翻转顺序为），你的genTList被称为pure_NP，所以你可以写

GHCi> import Generics.SOP.NP 
GHCi> pure_NP Nothing :: NP Maybe '[ Int, String ] 
Nothing :* (Nothing :* Nil)