限制含半幺羣類型值組成

Question

我有一個是Monoid一個實例，這樣我可以得到很好的值組成的數據類型：

data R a = R String (Maybe (String → a)) 

instance Monoid (R a) where 
    mempty = R "" Nothing 
    R s f `mappend` R t g = R (s ++ t) (case g of Just _ → g; Nothing → f) 

接下來，我不希望所有R a值彼此組合，它在我的領域沒有意義。所以，筆者爲大家介紹假體類型t：

{-# LANGUAGE DataKinds, KindSignatures #-} 

data K = T1 | T2 
data R (t ∷ K) a = R String (Maybe (String → a)) 

instance Monoid (R t a) where … 

所以我 「限制」 值：

v1 ∷ R T1 Int 
v2 ∷ R T2 Int 
-- v1 <> v2 => type error 

和 「無限制」：

v ∷ R t Int 
-- v <> v1 => ok 
-- v <> v2 => ok 

但現在我有一個問題。當談到v30，例如：

• 我將有巨大的 數據 樣的聲明（data K = T1 | … | T30）。我可以通過使用類型級別自然解決以獲得無限的幻像類型源（治癒比疾病更糟糕，不是嗎？）
• 我應該記住哪個幻像類型用於在依賴項中編寫類型簽名時使用的值代碼（確實是惱人）

是否有更容易的方法來限制組成？

Answer 1

尋找的ConstrainedMonoid

我來到了一個非常類似的問題最近，我終於解決了這個帖子的末尾描述的方式（不涉及獨異，但使用的類型的謂詞）。但是，我接受了挑戰，並試圖編寫一個ConstrainedMonoid課程。

這裏的想法：

class ConstrainedMonoid m where 
    type Compatible m (t1 :: k) (t2 :: k) :: Constraint 
    type TAppend m (t1 :: k) (t2 :: k) :: k 
    type TZero m :: k 

    memptyC :: m (TZero m) 
    mappendC :: (Compatible m t t') => m t -> m t' -> m (TAppend m t t') 

好了，還有的小例子，這實際上不添加任何新的東西（我換R S型參數）：

data K = T0 | T1 | T2 | T3 | T4 
data R a (t :: K) = R String (Maybe (String -> a)) 

instance ConstrainedMonoid (R a) where 
    type Compatible (R a) T1 T1 =() 
    type Compatible (R a) T2 T2 =() 
    type Compatible (R a) T3 T3 =() 
    type Compatible (R a) T4 T4 =() 
    type Compatible (R a) T0 y =() 
    type Compatible (R a) x T0 =() 

    type TAppend (R a) T0 y = y 
    type TAppend (R a) x T0 = x 
    type TAppend (R a) T1 T1 = T1 
    type TAppend (R a) T2 T2 = T2 
    type TAppend (R a) T3 T3 = T3 
    type TAppend (R a) T4 T4 = T4 
    type TZero (R a) = T0 

    memptyC = R "" Nothing 
    R s f `mappendC` R t g = R (s ++ t) (g `mplus` f) 

這種不幸發生很多冗餘類型實例（OverlappingInstances似乎不適用於類型族），但我認爲它在類型級別和值級別上滿足幺半羣法則。

但是，它並沒有關閉。它更像是一組不同的monoid，索引K。如果這就是你想要的，那就夠了。

如果您想了解更多

讓我們來看看不同的變體：

data B (t :: K) = B String deriving Show 

instance ConstrainedMonoid B where 
    type Compatible B T1 T1 =() 
    type Compatible B T2 T2 =() 
    type Compatible B T3 T3 =() 
    type Compatible B T4 T4 =() 

    type TAppend B x y = T1 
    type TZero B = T3 

    memptyC = B "" 
    (B x) `mappendC` (B y) = B (x ++ y) 

這可能是這是有道理的在您的域名的情況下 - 但是，它不是一個獨異了。如果您嘗試製作其中一個，它將與上述實例相同，只是使用不同的TZero。我其實只是在這裏猜測，但我的直覺告訴我，唯一有效的幺半羣實例就像R a;只有不同的單位值。否則，你會最終得到一些不必要的聯想（可能與終端對象，我認爲），這是而不是在組合下關閉。如果你想限制組成等於K s，你將失去單位價值。

一個更好的辦法（恕我直言）

以下是我真正解決我的問題（我根本就沒想到類羣的當年，因爲他們沒有任何意義，無論如何）。該解決方案主要剝掉以外的所有Compatible「約束製片人」，這是留給作謂語兩類：使用像

foo :: (Matching a b) => B a -> B b -> B Int 

type family Matching (t1 :: K) (t2 :: K) :: Constraint 
type instance Matching T1 T1 =() 
type instance Matching T2 T1 =() 
type instance Matching T1 T2 =() 
type instance Matching T4 T4 =() 

這使您完全控制您的兼容性的定義，以及你想要什麼類型的作品（不一定是monoidal），而且更一般。它可以擴展到無限種，太：

-- pseudo code, but you get what I mean 
type instance NatMatching m n = (IsEven m, m > n) 

---

回答你的最後兩點：

• 是的，你有你的那種定義足夠多的類型。但我認爲他們應該自我解釋。你也可以將它們分組，或者定義一個遞歸類型。

• 您主要必須在兩處提醒索引類型的含義：約束的定義以及工廠方法（mkB1 :: String -> B T1）。但我認爲這不應該成爲問題，如果類型命名的好。 （它可以是非常多餘的，雖然 - 我還沒有找到一種方法，以避免可能仍然會TH工作。）

難道這是更容易？

什麼其實我希望能夠寫出如下：

type family Matching (t1 :: K) (t2 :: K) :: Constraint 
type instance Matching T1 y =() 
type instance Matching x T1 =() 
type instance Matching x y = (x ~ y) 

我擔心這有嚴重的理由不被允許的;然而，也許，它只是沒有實施...

編輯：現在，我們有closed type families，正是這樣做。