从类型级列表中创建值列表

Question

我有这样的类型级列表

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

我正在尝试使用现有的TList生成新的TList.这个想法是有一个功能

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

其中't'是一些能够构造'gx'类型值的函数,其中'x'是列表'ixs'中的一种类型.

所以给定

data Foo x

和(某种)

generate :: forall x . Bar x

我可以得到这样的东西

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

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

我试图实现一些东西(https://gist.github.com/lolepezy/30820595afd9217083c5ca629e350b55),但它不会合理地检查(合理).

那我该怎么办呢？

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.这是rank-2多态类型实现的:

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

这需要RankNTypes语言扩展.

现在调用者只能传递参数类型为多态的函数g.所以传球Just False将不再有效,但传球Nothing会没问题.

这些情况的定义原则上是可以的,但你实际上可以删除OVERLAPSpragma甚至代理参数,因为没有任何重叠,并且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实例:

• 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)