創建一個從類型級列表

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)