GHC: không thể suy ra thông số kiểu phantom

Question

Vì vậy, tôi đang cố gắng tạo loại cho các bộ dữ liệu có độ dài thay đổi, về cơ bản là phiên bản đẹp hơn của Either a (Either (a,b) (Either (a,b,c) ...)) và 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 

Tuy nhiên, trình biên dịch dường như không thể suy ra các tham số kiểu bóng ma của prepend hoặc append trong các trường hợp đệ quy:

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

Có bất cứ điều gì tôi có thể làm gì để giúp trình biên dịch làm cho suy luận này?

Answer 1

Phần quan trọng của thông báo lỗi ở đây là:

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

này có nghĩa là gì? Điều đó có nghĩa là có thể có nhiều instance Prependable sao cho số type Prepend ... = a của bạn, để nếu bạn suy ra một số Prepend thành a, bạn không nhất thiết phải biết nó thuộc về trường hợp nào.

Bạn có thể giải quyết điều này bằng cách sử dụng data types in type families, trong đó có lợi thế mà bạn không đối phó với các chức năng loại, đó là surjective nhưng thể được đơn ánh, và thay vào đó với kiểu "quan hệ", đó là song ánh (Vì vậy, mỗi Loại Prepend chỉ có thể thuộc về một loại gia đình và mỗi loại gia đình có loại Prepend riêng biệt).

(Nếu bạn muốn tôi chỉ cho một giải pháp với các kiểu dữ liệu trong các gia đình loại, để lại nhận xét! Về cơ bản, chỉ cần sử dụng một data Prepend thay vì type Prepend)

Answer 2

Các giải pháp tôi đưa ra là để thêm một đối số giả để buộc prepend và append tới tham số phantom:

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