類型級列表

Question

多態構造我有一個類型級列表L，並正嘗試寫一個多態MKL，可以使用如下：

{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, 
    UndecidableInstances, AllowAmbiguousTypes, TypeSynonymInstances, 
    FlexibleInstances, ScopedTypeVariables #-} 

data T = Foo | Bar 
    deriving (Show, Eq) 

data L (ts :: [T]) = L [T] 
    deriving (Show, Eq) 

demo1 :: L '[Foo] 
demo1 = mkL 

demo2 :: L '[Foo, Bar] 
demo2 = mkL 

我demo1的輕鬆工作就夠了，但由於某種原因，遞歸案件正在擊敗我。

class MkL p where 
    mkL :: p 
instance MkL (L '[]) where 
    mkL = L [] 
instance MkL (L '[Foo]) where 
    mkL = L [Foo] 
instance MkL (L '[Bar]) where 
    mkL = L [Bar] 
instance MkL (L (l1 ': l2 ': ls)) where 
    mkL = 
     let (L [l1]) = undefined -- FIXME 
      (L [l2]) = undefined 
      (L rest) = undefined 
     in L (l1 : l2 : rest) 

如果我MKL更換FIXME，我得到：

No instance for (MkL (L t0)) arising from a use of ‘mkL’ 
The type variable ‘t0’ is ambiguous 
Note: there are several potential instances: 
    instance MkL (L (l1 : l2 : ls)) -- Defined at Target.hs:19:10 
    instance MkL (L '['Bar]) -- Defined at Target.hs:17:10 
    instance MkL (L '['Foo]) -- Defined at Target.hs:15:10 
    ...plus one other 
In the expression: mkL 
In a pattern binding: (L [l1]) = mkL 

那麼，有沒有什麼辦法來實現這一點？

Answer 1

您必須根據列表的遞歸結構在列表上編寫遞歸函數。一個列表或者是[]或_ : _：

instance MkL (L '[]) where 
    mkL = L [] 

instance MkL (L xs) => MkL (L ('Foo ': xs)) where 
    mkL = let L xs = mkL :: L xs in L (Foo : xs) 

instance MkL (L xs) => MkL (L ('Bar ': xs)) where 
    mkL = let L xs = mkL :: L xs in L (Bar : xs) 

但要注意的是，你的L類型可能不是你想要的。就編譯器而言，值水平[T]與類型水平[T]之間沒有關係。這是完全正確的：

instance MkL (L xs) where 
    mkL = L [] 

要保存類型級別列表的價值水平表示，你必須這樣做

data family SingT (x :: k) 

data instance SingT (x :: [k]) where 
    Nil :: SingT '[] 
    Cons :: SingT x -> SingT xs -> SingT (x ': xs) 

data instance SingT (x :: T) where 
    SFoo :: SingT 'Foo 
    SBar :: SingT 'Bar 

class Sing a where 
    sing :: SingT a 

instance Sing 'Foo where sing = SFoo 
instance Sing 'Bar where sing = SBar 
instance (Sing x, Sing xs) => Sing (x ': xs) where sing = Cons sing sing 
instance Sing '[] where sing = Nil 

然後你有sing :: SingT '[ 'Foo, 'Bar ]等，這類型僅由居住Cons SFoo (Cons SBar Nil)。有一些軟件包，例如singletons，它可以部分自動化定義這種類型的過程。

Answer 2

您必須考慮三種情況：空列表，頭部爲Foo的列表以及頭部爲Bar的列表。翻譯成實例：

instance MkL (L '[]) where 
    mkL = L [] 

instance MkL (L ts) => MkL (L (Foo ': ts)) where 
    mkL = case mkL :: L ts of L ts -> L (Foo : ts) 

instance MkL (L ts) => MkL (L (Bar ': ts)) where 
    mkL = case mkL :: L ts of L ts -> L (Bar : ts) 

沒有必要在這裏考慮n + 2長的名單，一些n，因爲我認爲我們想有實例爲所有ts :: [T]，以及空和(:)構造覆蓋所有。

---

在不同的音符，有一個existing library覆蓋這種使用情況下，它的安全，通常更強大。它使我們能夠生成（通過模板哈斯克爾，但也可以用手寫）類型級數據（稱爲「單例」）的價值級代表或類型級價值級函數的代表，併爲我們提供了大量工具與他們合作。

例如：

{-# LANGUAGE TemplateHaskell #-} -- on the top of the others 

import Data.Singletons.TH 

$(singletons [d| data T = Foo | Bar |]) 

這定義（除其他外）的SFoo :: Sing Foo和SBar :: Sing Bar構造，其中Sing是一個數據族和Sing x正好包含代表一些x類型的值電平。對於每個Sing x只有一個值（這就是爲什麼它是單例），因此可以明確地從它的單例中確定一個類型。

sFoo :: Sing Foo 
sFoo = SFoo 

sBar :: Sing Bar 
sBar = SBar 

demo1 :: Sing '[Foo] 
demo1 = sing 

demo2 :: Sing '[Foo, Bar] 
demo2 = sing 

sing類似於你Mk類，但它工作在許多不同的種類。

這裏，demo1等於SCons SFoo SNil，其中SCons和SNil是表示類型級列表中的單例構造函數。如果我們不想用，雖然單身的工作，我們可以擦除型指數，並與普通的舊數據工作：

demo1' :: [T] 
demo1' = fromSing demo1 

現在demo1等於[Foo]，所以fromSing的S -prefixed單身轉換回簡單的交涉。

與單身人士一起工作的最大好處是他們完美地反映了類型，所以它不可能「作弊」;相比之下，我們可以在運行時使任意值L ts不符合幻像類型索引。簡而言之，在L ts該索引只是一個幻像類型，但在Sing ts中，該索引正好反映在構造函數中。