GHC：未能推斷幻像類型參數

Question

所以我試圖爲可變長度元組創建一個類型，基本上是Either a (Either (a,b) (Either (a,b,c) ...))和Either (Either (Either ... (x,y,z)) (y,z)) z的更漂亮的版本。

{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-} 
module Temp where 

-- type level addition 
data Unit 
data Succ n 

class Summable n m where 
    type Sum n m :: * 

instance Summable Unit m where 
    type Sum Unit m = Succ m 

instance Summable n m => Summable (Succ n) m where 
    type Sum (Succ n) m = Succ (Sum n m) 

-- variable length tuple, left-to-right 
data a :+ b = a :+ Maybe b 
infixr 5 :+ 

class Prependable t r s where 
    type Prepend t r s :: * 
    prepend :: r -> Maybe s -> Prepend t r s 

instance Prependable Unit x y where 
    type Prepend Unit x y = x :+ y 
    prepend = (:+) 

instance Prependable n x y => Prependable (Succ n) (w :+ x) y where 
    type Prepend (Succ n) (w :+ x) y = w :+ Prepend n x y 
    prepend (w :+ Nothing) _ = w :+ Nothing 
    prepend (w :+ Just x) y = w :+ Just (prepend x y) 

-- variable length tuple, right-to-left 
data a :- b = Maybe a :- b 
infixl 5 :- 

class Appendable t r s where 
    type Append t r s :: * 
    append :: Maybe r -> s -> Append t r s 

instance Appendable Unit x y where 
    type Append Unit x y = x :- y 
    append = (:-) 

instance Appendable n x y => Appendable (Succ n) x (y :- z) where 
    type Append (Succ n) x (y :- z) = Append n x y :- z 
    append _ (Nothing :- z) = Nothing :- z 
    append x (Just y :- z) = Just (append x y) :- z 

然而，編譯器似乎無法推斷遞歸案件的prepend或append幻象類型參數：

Temp.hs:32:40: 
    Could not deduce (Prepend t1 x y ~ Prepend n x y) 
    from the context (Prependable n x y) 
     bound by the instance declaration at Temp.hs:29:10-61 
    NB: `Prepend' is a type function, and may not be injective 
    In the return type of a call of `prepend' 
    In the first argument of `Just', namely `(prepend x y)' 
    In the second argument of `(:+)', namely `Just (prepend x y)' 

Temp.hs:49:34: 
    Could not deduce (Append t0 x y ~ Append n x y) 
    from the context (Appendable n x y) 
     bound by the instance declaration at Temp.hs:46:10-59 
    NB: `Append' is a type function, and may not be injective 
    In the return type of a call of `append' 
    In the first argument of `Just', namely `(append x y)' 
    In the first argument of `(:-)', namely `Just (append x y)' 

有什麼我可以做些什麼來幫助編譯器進行此推斷？

Answer 1

這裏的錯誤消息的重要組成部分是：

NB: `Prepend' is a type function, and may not be injective 

這是什麼意思？這意味着可能有多個instance Prependable，因此它們的type Prepend ... = a，因此如果您推斷某些Prepend爲a，則不一定知道它屬於哪個實例。

您可以通過使用data types in type families，其中有你不型的功能，這是滿射，但可能是射，而是用型「關係」，這是雙射處理的優勢，解決這個問題（所以每Prepend類型只能屬於一個類型系列，而每個類型系列都有不同的類型）。

（如果你要我表現出與類型家庭的數據類型的解決方案，發表評論！基本上，只要使用的type Prependdata Prepend代替）

Answer 2

我想出瞭解決的辦法是增加一個僞參數綁prepend和append的幻影參數：

-- as above, except... 

unsucc :: Succ n -> n 
unsucc _ = undefined 

class Prependable t r s where 
    type Prepend t r s :: * 
    prepend :: t -> r -> Maybe s -> Prepend t r s 

instance Prependable Unit x y where 
    type Prepend Unit x y = x :+ y 
    prepend _ = (:+) 

instance Prependable n x y => Prependable (Succ n) (w :+ x) y where 
    type Prepend (Succ n) (w :+ x) y = w :+ Prepend n x y 
    prepend _ (w :+ Nothing) _ = w :+ Nothing 
    prepend t (w :+ Just x) y = w :+ Just (prepend (unsucc t) x y) 

class Appendable t r s where 
    type Append t r s :: * 
    append :: t -> Maybe r -> s -> Append t r s 

instance Appendable Unit x y where 
    type Append Unit x y = x :- y 
    append _ = (:-) 

instance Appendable n x y => Appendable (Succ n) x (y :- z) where 
    type Append (Succ n) x (y :- z) = Append n x y :- z 
    append _ _ (Nothing :- z) = Nothing :- z 
    append t x (Just y :- z) = Just (append (unsucc t) x y) :- z