inverting एक प्रकार परिवार

Question

मैं एक "रैखिक" प्रकार परिवार मिल गया है, प्रपत्र

type family Foo a 
type instance Foo T1 = T2 
type instance Foo T2 = T3 
... 
type instance Foo T9 = T10 

मेरी particualr उपयोग-मामले में की यानी, यह बहुत सुविधाजनक परिभाषित करने के लिए है "रिवर्स" परिवार FooRev और उसके बाद बाधा (FooRev (Foo x) ~ x) लागू:

type family FooRev a 
type instance FooRev T10 = T9 
type instance FooRev T9 = T8 
... 
type instance FooRev T2 = T1 

रिवर्स परिवार GHC कई प्रकार है कि अन्यथा गैर injectivity के कारण अस्पष्ट होगा अनुमान लगाने के लिए अनुमति देता है। यह अनिवार्य रूप से वही विचार है जिसे प्रस्तावित किया गया था here। यह समाधान बहुत अच्छी तरह से काम करता है, लेकिन यह सभी मामलों को सूचीबद्ध करके "रिवर्स" प्रकार परिवार को परिभाषित करने के लिए परेशान, प्रोग्रामिक और त्रुटि-प्रवण है। क्या Foo जैसे रैखिक परिवार के विपरीत को परिभाषित करने का एक और सामान्य तरीका है?

Answer 1

मैंने @ ची के विचार को देने का फैसला किया, और अंत में मैं कुछ आसान के साथ आया।

{-# LANGUAGE TypeOperators, DataKinds, TypeFamilies #-} 

type family NextElt (a :: *) (xs :: [*]) where 
    NextElt a (a ': b ': cs) = b 
    NextElt a (b ': c ': cs) = NextElt a (c ': cs) 

type family PrevElt (a :: *) (xs :: [*]) :: * where 
    PrevElt a (b ': a ': xs) = b 
    PrevElt a (b ': c ': xs) = PrevElt a (c ': xs) 

data T1 
data T2 
data T3 
type TSeq = '[T1, T2, T3] 

type NextRp a = NextElt a TSeq 
type PrevRp a = PrevElt a TSeq 

प्रकार के रेखीय क्रम प्रतिनिधित्व करने के लिए एक प्रकार सूची का उपयोग करते हुए मुझे प्रत्येक प्रकार दो बार लिख (जो प्रकार परिवार उदाहरणों या एक वर्ग के उदाहरणों का प्रयोग करते आवश्यक है) के बिना रिश्ते को व्यक्त करने की अनुमति देता है। उपरोक्त प्रकार के परिवार पिछले या अगले तत्व वाली सूची में किसी तत्व की खोज के लिए स्लाइडिंग-विंडो दृष्टिकोण का उपयोग करते हैं। इन प्रकार के परिवार सामान्य हैं (और Data.Type.Equality का उपयोग कर गैर-* प्रकारों के लिए काम करने के लिए बढ़ाया जा सकता है।)

Answer 2

मुझे लगता है कि FunctionalDependencies अपने मामले के लिए सबसे अच्छा समाधान किया जाना चाहिए:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} 

class Foo a b | a -> b, b -> a 
instance Foo T1 T2 
instance Foo T2 T3 
... 

अब प्रत्येक b एक a से अनुमान लगाया जा सकता है और इसके विपरीत।