उपयोगकर्ता द्वारा परिभाषित एक डेटाटाइप से मेल खाने वाले पैटर्न में शामिल कैस्ट को समझना

Question

तो, मैं हास्केल में DataKinds और TypeFamilies के साथ खेल रहा था और उत्पन्न कोर जीएचसी को देखना शुरू कर दिया था।

यहाँ मेरे सवाल प्रेरित करने के लिए एक छोटे से testcase है:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 

module TestCase where 

data Ty = TyBool | TyInt 

type family InterpTy (t :: Ty) :: * 
type instance InterpTy TyBool = Bool 
type instance InterpTy TyInt = Int 

data Expr (a :: Ty) where 
    I :: Int -> Expr TyInt 
    B :: Bool -> Expr TyBool 

eval :: Expr a -> InterpTy a 
eval (I i) = i 
eval (B b) = b 

के eval समारोह

TestCase.eval = 
    \ (@ (a_aKM :: TestCase.Ty)) (ds_dL3 :: TestCase.Expr a_aKM) -> 
    case ds_dL3 of _ [Occ=Dead] { 
     TestCase.I dt_dLh i_as6 -> 
     i_as6 
     `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0]) 
       ; (TestCase.InterpTy (Sym dt_dLh))_R 
       :: GHC.Types.Int ~# TestCase.InterpTy a_aKM); 
     TestCase.B dt_dLc b_as7 -> 
     b_as7 
     `cast` (Sub (Sym TestCase.TFCo:R:InterpTyTyBool[0]) 
       ; (TestCase.InterpTy (Sym dt_dLc))_R 
       :: GHC.Types.Bool ~# TestCase.InterpTy a_aKM) 
    } 

जाहिर है हम के बारे में जानकारी रखने की आवश्यकता नहीं के लिए उत्पन्न कोर पर एक नज़र डालते हैं क्या a विशिष्ट शाखा में हो सकता है। अगर मैं डेटाकाइंड पर अनुक्रमणित नहीं करता हूं और टाइपफमिलियों का उपयोग नहीं करता तो कलाकार को समझना बहुत आसान होता है।

Main.eval = 
    \ (@ a_a1hg) (ds_d1sQ :: Main.Simpl a_a1hg) -> 
    case ds_d1sQ of _ [Occ=Dead] { 
     Main.I' dt_d1to i_aFa -> 
     i_aFa 
     `cast` (Sub (Sym dt_d1to) :: GHC.Integer.Type.Integer ~# a_a1hg); 
     Main.B' dt_d1tk b_aFb -> 
     b_aFb `cast` (Sub (Sym dt_d1tk) :: GHC.Types.Bool ~# a_a1hg) 
    } 

यह मैं पूरी तरह से अच्छी तरह से समझ सकते हैं, इस भाग कि मुझे क्या TypeFamilies उदाहरण में परेशानी पैदा करती है:

वह कुछ इस तरह होगा

(Sub (Sym TestCase.TFCo:R:InterpTyTyInt[0]) 
     ; (TestCase.InterpTy (Sym dt_dLh))_R 
     :: GHC.Types.Int ~# TestCase.InterpTy a_aKM); 

दूसरी पंक्ति क्या वास्तव में भ्रमित है मुझे। अर्धविराम क्या कर रहा है? ऐसा लगता है कि यहां कुछ जगह है या क्या मुझे कुछ याद आ रहा है? वहाँ एक जगह है जहाँ मैं इस पर पढ़ सकते हैं है, (मैं खुशी कागजात ले अगर आप एक सिफारिश कर सकते हैं)

सधन्यवाद

raichoo

Answer 1

अर्धविराम coercions के transitivity के लिए वाक्य रचना है।

सिस्टम एफसी के बारे में नवीनतम (सितम्बर 2014 को) कागज ICFP 2014

विशेष रूप से से "Safe Zero-Cost Coercions in Haskell" है, कि कागज के 3 चित्र में हम coercions की वाक्य रचना को देखते हैं। "γ₁; γ₂" जबरन पारगमनशीलता है। यदि γ₁ एक जबरदस्ती है कि गवाह है कि "τ₁ ~ τ₂" और γ₂ एक जबरदस्ती है कि गवाह है कि τ₂ ~ τ₃ फिर "γ₁; γ₂" एक जबरदस्ती है कि गवाह τ₁ ~ τ₃।

उदाहरण में, जब आप eval (I i) = i बारे में क्या संकलक दाहिने हाथ की ओर देखता प्रकार Int के एक मूल्य है, और क्या यह (समारोह की वापसी प्रकार से) की जरूरत है InterpTy a के बारे में कुछ है। तो अब इसे एक सबूत बनाने की जरूरत है कि Int ~ InterpTy a।

अनौपचारिक रूप से, (दाईं से बाईं ओर पढ़ने और भूमिकाओं अनदेखी - विवरण जिनमें से जुड़ा हुआ कागज को देखने के लिए):

1. GADT पैटर्न मैच हम सीखते हैं कि "a ~ Int"
(कि dt_dLh है) कर रहा से
2. इसलिए हम Int ~ a "प्राप्त करने के लिए Sym लागू करते हैं।
3. फिर "InterpTy Int ~ InterpTy a" पाने के लिए InterpTy परिवार लागू (यह/अनुरूपता का एक उदाहरण है /)
4. फिर हम रचना है कि संक्रामक के साथ "Sym InterpTyTyInt" (जो है जो यह बताता है स्वयंसिद्ध के फ़्लिप संस्करण है कि "InterpTy TyInt ~ Int") हम जिस दबाव के बाद हैं उसके बाद: "Int ~ InterpTy a"