11 Natural Transformation (การแปลงแบบธรรมชาติ) (Sketch)
เราได้พูดเกี่ยวกับfunctorในฐานะการแปรงระหว่างcategoryต่างๆที่คงไว้ด้วยโครงสร้าง
functorทำการ”ฝัง”categoryตัวหนึ่งในอีกตัวหนึ่ง มันอาจจะรวบสิ่งต่างๆหลายๆอันไปเป็นสิ่งเดียว แต่มันไม่เคยที่จะทำลายการเชื่อมต่อกัน หนึ่งในวิธีคิดเกี่ยวกับมันคือการที่ว่า ในการมีfunctorเรากำลังขึ้นรูป(model)categoryหนึ่งข้างในอีกอันหนึ่ง categoryเริ่มต้นมีหน้าที่เป็นแม่แบบ(model)สำหรับโครงสร้างที่เป็นส่วนหนึ่งของcategoryที่เป็นเป้าหมาย
ได้มีหลายวิธีของการฝังcategoryหนึ่งในอีกตัวหนึ่ง ในบางครั้งพวกมันนั้นเท่ากับในบางครั้งพวกมันนั้นก็แตกต่าง เราอาจจะรวบcategoryเริ่มต้นไปเป็นวัตถุเดี่ยว อีกคนอาจจะโยงทุกๆวัตถุไปยังวัตถุที่ต่างกันและทุกๆmorphismไปยังmorphismที่ต่างกัน ในแม่แบบที่เหมือนกันอาจจะถูกทำให้เป็นจริง(realized)ในหลายๆรูปแบบและวิธี การแปลงแบบธรรมชาติ(Natural transformation)ช่วยเราในการเปรียบเทียบการทำให้เป็นจริงเหล่านี้ พวกมันคือการโยงระหว่างfunctor (การโยงที่พิเศษที่อนุรักษ์ความเป็นfunctorของมัน)
ลองพิจารณาfunctorสองตัว\(F\)และ\(G\)ระหว่างcategory\(\textbf{C}\)และ\(\textbf{D}\) ถ้าคุณให้ความสำคัญกับแต่วัตถุหนึ่ง\(a\)ใน\(\textbf{C}\) มันก็จะถูกโยงไปยังสองสัตถุอย่าง\(Fa\)และ\(Ga\) การโยงระหว่างfunctorควรที่จะโยง\(Fa\)ไปยัง\(Ga\)
สังเกตว่า\(Fa\)และ\(Ga\)คือวัตถุในcategory\(\textbf{D}\)เดียวกัน การโยงระหว่างวัตถุในcategoryเดียวกันไม่ควรที่จะขัดกับ(คุณสมบัติของ)categoryนั้น เราไม่ต้องการที่จะสร้างการเชื่อมต่อใหม่ๆระหว่างวัตถุ ดังนั้นมันจึงเป็นธรรมชาติที่จะใช้การเชื่อมต่อที่มีอยู่แล้วนั้นก็คือmorphism การแปลงแบบธรรมชาติคือการเลือกmorphismเหล่านี้ สำหรับทุกๆวัตถุ\(a\)มันเลือกmorphismอันหนึ่งจาก\(Fa\)ไปยัง\(Ga\) ถ้าเราเรียกการแปลงแบบธรรมชาติว่า\(\alpha\) morphismตัวนี้จะถูกเรียกว่าส่วนประกอบ(component)ของ\(\alpha\)ที่\(a\)หรือ\(\alpha_a\)
\[ \alpha_a :: Fa\rightarrow Ga \]
จงจำไว้ว่า\(a\)คือวัตถุใน\(\textbf{C}\)ในขณะที่\(\alpha_a\)คือmorphismใน\(\textbf{D}\)
แน่นอนว่ามันเป็นแค่ส่วนหนึ่งของเรื่องทั้งหมด เพราะว่าfunctorไม่แต่โยงวัตถุแต่พวกมันยังโยงmorphismด้วย มันกลับเป็นว่าการโยงของmorphismนั้นคงที่ ภายใต้การแปลงแบบธรรมชาติใดๆตามระหว่าง\(F\)และ\(G\) \(Ff\)ต้องถูกแปลงไปเป็น\(Gf\) มากกว่านั้นคือการโยงของmorphismโดยfunctorทั้งสอง ได้จำกัดตัวเลือกที่เรามีในการนิยามการแปลงแบบธรรมชาติในแบบที่ที่เข้ากันกับการโยงได้ ลองพิจารณาmorphism\(f\)ระหว่างสองวัตถุอย่าง\(a\)และ\(b\)ใน\(\textbf{C}\) มันโยงmorphism\(Ff\)และ\(Gf\)ทั้งสองใน\(\textbf{D}\)
การแปลงแบบธรรมชาติ\(\alpha\)ได้ให้morphismเพิ่มขึ้นมาสองตัว ที่ทำให้diagramใน\(\textbf{D}\)สมบูรณ์
\[ \begin{aligned} &\alpha_a :: Fa\rightarrow Ga \\ &\alpha_b :: Fb\rightarrow Gb \end{aligned} \]
ในที่นี้เรามีวิธีการสองแบบในการเดินจาก\(Fa\)ไปยัง\(Gb\) ในการที่จะทำให้แน่ใจว่าพวกมันนั้นเท่ากัน เราต้องกำหนดเงื่อนไขความเป็นธรรมชาติให้เป็นจริงในทุกๆ\(f\)
\[ Gf\circ\alpha_a = \alpha_b\circ Ff \]
เงื่อนไขความเป็นธรรมชาติเป็นความต้องการที่ค่อนข้างเข้มงวด ตัวอย่างเช่นถ้าmorphism\(Ff\)นั้นสามารถที่จะinvertได้ ความเป็นธรรมชาติก็จะกำหนด\(\alpha_b\) ในแบบของ\(\alpha_a\) หรือก็คือมันtransport\(\alpha_a\)เทียบกับ\(f\)
\[ \alpha_b = (Gf)\circ\alpha_a\circ(Ff)^{-1} \]
ถ้ามันมีมากกว่าmorphismที่สามารถinvertได้ระหว่างวัตถุทั้งสอง การtransportเหล่านี้ต้องตรงกัน แต่โดยทั่วไปmorphismนั้นไม่สามารถทีถูกinvertได้ แต่คุณสามารถที่จะเห็นว่าการมีอยู่ของการแปลงแบบธรรมชาติระหว่างสองfunctorนั้นอยากที่จะถูกรับประกันว่ามีอยู่ ดังนั้นความหายากหรือความหลากหลายของfunctorที่มีความสัมพันธ์โดยการแปลงแบบธรรมชาติ อาจจะบอกคุณได้มากเกี่ยวกับโครงสร้างของcategoryที่ๆพวกมันทำงานอยู่ เราจะเห็นตัวอย่างของสิ่งนี้ในการที่เราพูดเกี่ยวกับlimitและlemmaของYoneda
ถ้าเรามองการแปลงแบบธรรมชาติในแบบของแต่ละตัวประกอบ เราอาจจะพูดได้ว่ามันโยงวัตถุไปยังmorphism เพราะว่าเงื่อนไขความเป็นธรรมชาติ เราสามารถที่จะพูดได้ว่ามันโยงmorphismไปยังสี่เหลี่ยมของการcommute ได้มีสี่เหลี่ยมของการcommuteที่เป็นธรรมชาติใน\(\textbf{D}\)สำหรับทุกๆmorphismใน\(\textbf{C}\)
คุณสมบัตินี้ของการแปลงแบบธรรมชาตินั้นมีประโยชน์ในการสร้างแบบcategoryที่มีความหลากหลาย โดยมักจะประกอบด้วยcommutative diagram ด้วยการเลือกfunctorอย่างรอบคอบ หลากหลายเงื่อนไขของความcommutativeเหล่านี้อาจจะถูกแปลงไปเป็นเงื่อนไขความเป็นธรรมชาติ เราจะเห็นตัวอย่างของสิ่งเหล่านี้ในตอนที่เราไปยังlimit colimitและadjunction
สุดท้ายแล้วการแปลงแบบธรรมชาติอาจจะถูกใช้ในการนิยามisomorphismระหว่างfunctor การบอกว่าfunctorทั้งสองนั้นisomorphicแบบธรรมชาตินั้นแทบจะเหมือนการบอกว่ามันนั้นเท่ากัน isomorphicแบบธรรมชาติ ที่ถูกนิยามในฐานะการแปลงแบบธรรมชาติที่ส่วนประกอบทั้งหมดเป็นisomorphism (morphismที่invertได้)
11.1 FunctionแบบPolymorphic
เราได้พูดเกี่ยวกับหน้าที่ของfunctor(หรือโดยเฉพาะendofunctor)ในการเขียนโปรแกรม โดยที่มันคู่กับconstructorของtypeที่โยงtypeต่างๆไปยังtypeต่างๆ พวกมันก็ยังโยงfunctionต่างๆไปยังfunctionต่างๆและการโยงนี้ถูกเขียนโดยfunction higher order ที่ชื่อว่าfmap
(หรือtransform
,then
และสิ่งที่คล้ายๆกันในC++)
ในการสร้างการแปลงแบบธรรมชาติ เราเริ่มด้วยวัตถุอย่างtypea
โดยfunctorF
ตัวหนึ่งที่โยงมันไปยังtype\(Fa\) และfunctorอีกตัวหนึ่งG
ที่โยงไปยัง\(Ga\)ส่วนประกอบของการแปลงแบบธรรมชาติalpha
ที่a
คือfunctionจาก\(Fa\)ไปยัง\(Ga\) หรือในHaskellเทียม
alpha_a :: F a -> G a
การแปลงแบบธรรมชาติคือfunctionแบบpolymorphic ที่นิยามสำหรับทุกtypea
alpha :: forall a . F a -> G a
forall a
นั้นที่ไม่บังคับในHaskell(และในความจริงแล้วมีความจำเป็นที่ต้องเปิดส่วนขยายของภาษาอย่างExplicitForAll
) โดยทั่วๆไปแล้วคุณอาจจะต้องเขียนมันในรูปแแบบนี้
alpha :: F a -> G a
ต้องจำไว้ว่ามันคือชุดของfunctionที่ถูกparameterizedโดยa
นี่คืออีกตัวอย่างหนึ่งของความกระชับของsyntaxของHaskell เพราะในการสร้างที่คล้ายกันในC++ก็จะมีความเยิ่นเย้อมากกว่า
template<class A> G<A> alpha(F<A>);
สิ่งที่แตกต่างอย่างลึกซึ้งระหว่างfunctionแบบpolymorphicของHaskellและfunctioแบบgenericของC++ ถูกแสดงให้เห็นในแบบที่functionต่างๆเหล่านี้นั้นถูกเขียนและตรวจสอบของtype ในHaskell functionแบบpolymorphicต้องถูกนิยามให้เหมือนกันหมดสำหรับทุกtype สูตรๆหนึ่งต้องทำงานได้ในทุกๆtype สิ่งนี้สามารถถูกเรียกว่าความเป็นpolymorphicแบบparametric
ในอีกด้านหนึ่งC++รองรับความเป็นpolymorphicเฉพาะกิจที่มีอยู่แล้ว ที่หมายความว่าtemplateไม่ต้องถูกนิยามแบบสมบูรณ์สำหรับทุกๆtype templateจะสามารถใช้ได้สำหรับtypeที่ให้มาหรือไม่นั้นจะถูกตัดสินใจในเวลาที่ถูกสร้าง โดยที่typeที่เป็นรูปธรรมนั้นจะแทนที่parameterของtype การตรวจสอบtypeนั้นก็จะถูกยืดเวลาออกไป โดยที่มักจะนำไปสู่ข้อความerrorที่ไม่สามารถเข้าใจได้ ที่เป็นสิ่งที่อย่างน่าเสียดาย
ในC++ได้มีกลไกสำหรับfunctionในการoverloadingและการทำให้templateมีความเฉพาะเจาะจง โดยที่อนุญาติในมีนิยามที่แตกต่างกันของfunctionเดียวกันสำหรับtypeที่แตกต่างกัน ในHaskellความเป็นfunctionนี้นั้นถูกให้โดยtype classsesและtype families
ความเป็นpolymorphicแบบparametricของHaskellมีผลที่ตามมาที่คาดไม่ถึง คือว่าในทุกๆfunctionแบบpolymorphicของtypeอย่าง
alpha :: F a -> G a
โดยที่F
และG
คือfunctor ได้บรรลุเงื่อนไขของความเป็นธรรมชาติโดยอัตโนมัติ ที่นี่มันคือสมการในแบบcategory(ที่\(f\)คือfunction\(f::a\rightarrow b\))
\[ Gf\circ\alpha_a = \alpha_b\circ Ff \]
ในHaskell การกระทำของfunctorG
บนmorphismf
นั้นถูกเขียนโดยfmap
ผมจะเขียนมันในHaskell-เทียมที่มีtype annotationsอย่าง
. alpha_a = alpha_b . fmap_F f fmap_G f
เพราะว่าการอนุมานของtype annotationsนั้นไม่จำเป็นและสมการเหล่านี้เป็นสิ่งที่ถูกต้อง
fmap f . alpha = alpha . fmap f
นี่ยังไม่ใช่Haskellจริงๆ(ความเท่ากันของfunctionไม่สามารถถูกเขียนในโค้ด) แต่มันคือความเท่ากันที่สามารถถูกใช้โดยโปรแกรมเมอร์ในการให้เหตุผลทางสมการ หรือใช้โดยcomplierในการเพิ่มประสิทธิภาพ
เหตุผลที่ว่าทำไมเงื่อนไขของความเป็นธรรมชาติถูกบรรลุอย่างอัตโนมัติในHaskell นั้นต้องมาคู่กับ”การได้ทฤษฎีบทโดยไม่ต้องทำอะไร” ความเป็นpolymorphicแบบparametricที่ถูกใช้ในการนิยามการแปลงแบบธรรมชาติในHaskell ได้กำหนดให้มีข้อจำกัดที่แข็งแรงบนการเขียน(ที่ก็คือการที่มีหนึ่งสูตรสำหรับtypeทุกประเภท) ข้อจำกัดเหล่านี้แปรไปยังทฤษฎีบทของความเท่ากันระหว่างfunctionเหล่านี้ ในกรณีของfunctionที่แปลงfunctorต่างๆ ทฤษฎีบทที่ได้มาโดยไม่ต้องทำอะไรนั้นคือเงื่อนไขของความเป็นธรรมชาติ1
หนึ่งในวิธีการคิดเกี่ยวกับfunctorในHaskellที่ผมกล่าวถึงก่อนหน้านี้ คือการพิจารณาพวกมันให้เป็นcontainerแบบทั่วไป เราสามารถที่จะใช้การเปรียบเทียบอย่างนี้ต่อและลองพิจารณาการแปลงแบบธรรมชาติให้เป็น วิธีการในการบรรจุช้ำของสิ่งที่อยู่ข้างในของcontainerหนึ่งไปยังอีกcontainerหนึ่ง
เงื่อนไขทางธรรมชาติกลายมาเป็นสมการที่ว่ามันไม่จำเป็นว่าเราจะแปรสิ่งที่อยู่ภายในก่อน ที่ก็คือผ่านการใช้งานของfmap
และการบรรจุช้ำต่อจากนี้ หรือบรรจุช้ำก่อนและทำการเปลี่ยนแปลงสิ่งที่อยู่ข้างในcontainerใหม่ด้วยfmap
ของมันเอง สองการกระทำแบบนี้ ในการบรรจุช้ำและการfmap
นั้นorthogonalกัน(ไม่มีความเกี่ยวข้องกัน) “หนึ่งในนั้นขยับใข่ อีกตัวทำการต้มมัน” (One moves the eggs, the other boils them)
เรามาดูตัวอย่างต่างๆของการแปลงแบบธรรมชาติในHaskell สิ่งแรกคือระหว่างfunctorของlistและfunctorMaybe
มันreturnกลับมาเป็นหัวของlistในตอนที่listนั้นไม่ได้ว่าง
safeHead :: [a] -> Maybe a
= Nothing
safeHead [] :xs) = Just x safeHead (x
มันคือfunctionที่polymorphicในa
เพราะมันใช้ได้สำหรับtypea
ใดๆก็ตามโดยไม่มีข้อจำกัด ดังนั้นมันคือตัวอย่างของpolymorphismแบบparametric ที่ก็คือการแปลงแบบธรรมชาติระหว่างfunctorทั้งสอง การที่จะทำให้เราเชื่อมั่น เรามาพิสูจน์ความเป็นเงื่อนไขของความเป็นธรรมชาติ
fmap f . safeHead = safeHead . fmap f
เรามีอยู่สองกรณีในการพิจารณาlistว่าง
fmap f (safeHead []) = fmap f Nothing = Nothing
fmap f []) = safeHead [] = Nothing safeHead (
และlistที่ไม่ว่าง
fmap f (safeHead (x:xs)) = fmap f (Just x) = Just (f x)
fmap f (x:xs)) = safeHead (f x : fmap f xs) = Just (f x) safeHead (
ผมได้ใช้การเขียนfmap
สำหรับlistต่างๆเหล่านี้
fmap f [] = []
fmap f (x:xs) = f x : fmap f xs
และสำหรับMaybe
fmap f Nothing = Nothing
fmap f (Just x) = Just (f x)
กรณีที่น่าสนใจคือในตอนที่หนึ่งในfunctorคือfunctorConst
แบบ’ง่ายๆ’ การแปลงแบบธรรมชาติมาจากหรือไปยังfunctorConst
ดูเหมือนแค่functionที่เป็นpolymorphicในtypeของการreturn หรือtypeของargumentของมัน
ตัวอย่างเช่นlength
สามารถถูกคิดในฐานะแปลงแบบธรรมชาติสำหรับfunctorของlistคือConst Int
functorอย่างๆ
length :: [a] -> Const Int a
length [] = Const 0
length (x:xs) = Const (1 + unConst (length xs))
ในที่นี้unConst
ถูกใช้ในการดึงconstructorของConst
unConst :: Const c a -> c
Const x) = x unConst (
แน่นอนว่าในทางปฏิบัติlength
ถูกนิยามว่า
length :: [a] -> Int
ที่ช่อนความจริงที่ว่ามันคือแปลงแบบธรรมชาติได้อย่างมีประสิทธิภาพ
การหาfunctionที่polymorphicแบบparametricจากfunctorConst
นั้นอาจจะยากกว่านิดหนึ่ง เนื่อว่ามันอาจจะจำเป็นต้องมีการสร้างของค่าจากการที่ไม่มีอะไรเลย สิ่งที่เราสามารถทำได้คือ
scam :: Const Int a -> Maybe a
Const x) = Nothing scam (
functorที่มีความทั่วไปอีกอย่างหนึ่งที่เราได้เห็นแล้วและที่จะมีบทบาทในlemmaของYoneda คือfunctorReader
ที่ผมจะเขียนนิยามของมันใหม่ในฐานะnewtype
ว่า
newtype Reader e a = Reader (e -> a)
มันถูกparameterizedโดยสองtypeแต่ก็มีความเป็นfunctor(แบบcovariant)แค่ในตัวที่สอง
instance Functor (Reader e) where
fmap f (Reader g) = Reader (\x -> f (g x))
ในทุกๆtypee
คุณสามารถที่จะนิยามชุดของการแปลงแบบธรรมชาติจากReader e
ไปยังfunctorf
อื่นๆ เราจะเห็นหลังจากนี้ว่าสมาชิกของชุดนี้นั้น ตรงแบบหนึ่งต่อหนึ่งกับสมาชิกของf e
(lemmaของYoneda)
ตัวอย่างเช่นลองพิจารณาunit typeค่อนข้างทั่วๆไป()
กับสมาชิกเดี่ยว()
functorReader ()
นั้นนำtypea
ใดๆก็ตามและโยงมันไปยังtypeแบบfunction() -> a
สิ่งนี้คือfunctionที่เลือกสมาชิกหนึ่งในa
มา มาลองพิจารณาการแปลงแบบธรรมชาติจากfunctorนี้ไปยังMaybe
functor
alpha :: Reader () a -> Maybe a
ได้มีแค่สองตัวอย่างdumb
และobvious
Reader _) = Nothing dumb (
และ
Reader g) = Just (g ()) obvious (
(สิ่งที่คุณสามารถทำได้กับg
คือการใช้มันกับค่าunit()
)
และแน่นอนว่าในการคาดเดาของlemmaของYoneda สิ่งเหล่านี้คู่กับสมาชิกทั้งสองของtypeMaybe ()
ที่ก็คือNothing
และJust ()
เราจะกลับมาที่lemmaของYonedaหลังจากนี้ นี่เป็นแค่น้ำจิ้ม
11.2 ข้ามพ้นความเป็นธรรมชาติ
Functionแบบpolymorphicและparametricระหว่างfunctorทั้งสอง(รวมไปถึงกรณีที่สุดโต่งของfunctorConst
) นั้นจะเป็นการแปลงแบบธรรมชาติเสมอ และเนื่องด้วยtypeแบบข้อมูลแบบพีชคณิตและมาตรฐานนั้นคือfunctor functionแบบpolymorphicระหว่างtypeพวกนี้คือการแปลงแบบธรรมชาติ
เราได้มีtypeแบบfunctionต่างๆอยู่แล้วและสิ่งเหล่านี้นั้นมีความเป็นfunctorในtypeของการreturnของมัน เราสามารถใช้มันในการสร้างfunctorต่างๆ(เหมือนกับfunctorReader
) และนิยามการแปลงแบบธรรมชาติที่เป็นfunctionแบบhigher-order
แต่ว่าtypeแบบfunctionนั้นไม่เป็นcovariantในtypeของargument พวกมันเป็นแบบcontravariant แน่นอนว่าfunctorแบบcontravariantนั้นเท่ากันกับfunctorแบบcovariantจากcategoryตรงข้าม functionแบบpolymorphicระหว่างfunctorแบบcontravariantนั้นก็ยังคือการแปลงแบบธรรมชาติในความหมายทางcategory ยกเว้นว่าพวกมันทำงานบนfunctorจากcategoryตรงข้ามไปยังtypeของHaskell
คุณอาจจะจำได้ว่าตัวอย่างของfunctorแบบcontravariantที่เราได้เห็นมาก่อนหน้านี้คือ
newtype Op r a = Op (a -> r)
functorนี้นั้นเป็นแบบcontravariantในa
instance Contravariant (Op r) where
Op g) = Op (g . f) contramap f (
เราสามารถที่จะเขียนfunctionแบบpolymorphicจากอย่างOp Bool
ไปยัง Op String
ว่า
Op f) = Op (\x -> if f x then "T" else "F") predToStr (
แต่เนื่องด้วยfunctorทั้งสองนั้นไม่ได้เป็นcovariant นี่จึงไม่ใช่การแปลงแบบธรรมชาติใน\(\textbf{Hask}\) แต่เพราะว่าพวกมันนั้นเป็นcontravariantทั้งคู่ พวกมันบรรลุเงื่อนไขของความเป็นธรรมชาติแบบ”ตรงข้าม”
. predToStr = predToStr . contramap f contramap f
สังเกตว่าfunctionf
ต้องไปยังทิศทางตรงข้ามของสิ่งที่เราได้ใช้กับfmap
ก็เพราะว่าsigntureของcontramap
คือ
contramap :: (b -> a) -> (Op Bool a -> Op Bool b)
แล้วเป็นไปได้ไหมที่จะมีconstructorของtypeที่ไม่ใช่functorไม่ว่าจะเป็นcovariantหรือ contravariant? นี่คือตัวอย่างหนึ่ง
-> a a
สิ่งนี้ไม่ใช่functorเพราะว่าtypea
เดียวกันถูกใช้ทั้งในตำแหน่งด้านลบ(contravariant)และด้านบวก(covariant) ดังนั้นfunctionที่มีsignatureแบบนี้
-> a) -> f a (a
ที่f
คือfunctorใดๆก็ตามไม่สามารถที่จะเป็นการแปลงแบบธรรมชาติ น่าสนใจที่ว่าได้มีการgeneralizeของการแปลงแบบธรรมชาติ ที่ถูกเรียกว่าการแปลงแบบธรรมชาติคู่(dinatural transformations)ที่จะทำงานกับกรณีต่างๆแบบนี้ เราจะมาดูสิ่งๆแบบนี้ในตอนที่เราพูดเกี่่ยวกับends
11.3 CategoryของFunctor
ในที่นี้เรามีการโยงระหว่างfunctorต่างๆ(นั้นก็คือการแปลงแบบธรรมชาติ)มันเป็นธรรมชาติในการที่ถามว่าfuntorสามารถก่อให้เกิดcategoryได้หรือเปล่า และแน่นอนว่ามันทำได้ ได้มีcategoryของfunctorหนึ่งสำหรับแต่ละคู่ของcategories\(\textbf{C}\)และ\(\textbf{D}\) วัตถุในcategoryนี้คือfunctorจาก\(\textbf{C}\)ไปยัง\(\textbf{D}\)และmorphismคือการแปลงแบบธรรมชาติ
เราต้องนิยามการประกอบกันของการแปลงแบบธรรมชาติทั้งสองแต่นั้นมันค่อนข้างง่าย ส่วนประกอบของการแปลงแบบธรรมชาติคือmorphismและเราก็รู้วิธีการประกอบmorphisms
ถ้าเรานำการแปลงแบบธรรมชาติ\(\alpha\)จากfunctor\(F\)ไปยัง\(G\)แล้ว ส่วนประกอบของมันที่วัตถุ\(a\)ในบางmorphism
\[ \alpha_a::Fa\rightarrow Ga \]
เราต้องการที่จะประกอบ\(\alpha\)ด้วย\(\beta\)ที่ก็คือการแปลงแบบธรรมชาติจากfunctor\(G\)ไปยัง\(H\) โดยที่ส่วนประกอบของ\(\beta\)ที่\(a\)คือmorphism
\[ \beta_a :: Ga\rightarrow Ha \]
Morphismเหล่านี้นั้นประกอบได้และการประกอบของมันคือmorphismอีกอันหนึ่ง
\[ \beta_a\circ\alpha_a :: Fa\rightarrow Ha \]
เราจะใช้morphismนี้ในฐานะส่วนประกอบของการแปลงแบบธรรมชาติ\(\beta\cdot\alpha\)ที่คือการประกอบกันของการแปลงแบบธรรมชาติ\(\beta\)หลัง\(\alpha\)ทั้งสอง
\[ (\beta\cdot\alpha)_a = \beta_a\circ\alpha_a \]
การจ้อง(ที่นาน)ไปยังdiagramได้ทำให้เรามั่นใจว่าผลของการประกอบนี้คือการแปลงแบบธรรมชาติจาก\(F\)ไปยัง\(H\)
\[ Hf\circ(\beta\cdot\alpha)_a = (\beta\cdot\alpha)_b\circ Ff \]
การประกอบกันของการแปลงแบบธรรมชาติต่างๆนั้นมีคุณสมบัติการเปลี่ยนหมู่ เพราะว่าการประกอบกันของพวกมันที่ก็คือmorphismทั่วๆไป ดังนั้นจึงมีคุณสมบัติการเปลี่ยนหมู่ในส่วนของการประกอบกันของพวกมัน
สุดท้ายแล้วสำหรับfunctor\(F\)ได้มีการแปลงแบบธรรมชาติที่เป็นidentity\(1_F\) ที่ส่วนประกอบของมันคือmorphismแบบidentity
\[ \operatorname{id}_{Fa}::Fa\rightarrow Fa \]
แน่นอนว่าดังนั้นfunctorsที่สร้างจึงเป็นcategory
ของให้ผมได้พูดเกี่ยวกับเกี่ยวกับnotationสักนิดหนึ่ง ผมได้ใช้จุดสำหรับประเภทของการประกอบของการแปลงแบบธรรมชาติที่ผมได้อธิบายไปก่อนหน้านี้ ที่ก็ตามมาจากSaunders Mac Lane ปัญหาคือว่าการประกอบของการแปลงแบบธรรมชาติมีอยู่สองวิธี โดยสิ่งก่อนหน้านี้จะถูกเรียกว่าเรียกว่าการประกอบกันในแนวตั้ง เพราะว่าfunctorนั้นมักจะช้อนกันในdiagramที่ทำการอธิบายมัน การประกอบกันในแนวตั้งนั้นมีความสำคัญในการนิยามcategoryของfunctor ผมจะอธิบายการประกอบกันในแนวนอนในอีกไม่ช้า
categoryของfunctorระหว่างcategory \(\textbf{C}\)และ\(\textbf{D}\) นั้นถูกเขียนไว้ว่า\(\textbf{Fun}(\textbf{C}, \textbf{D})\)หรือ\([\textbf{C},\textbf{D}]\) หรือในบางครั้งในฐานะ\(\textbf{D}^\textbf{C}\) ในการเขียนอย่างสุดท้ายบอกเราว่าcategoryของfunctor ตัวมันเองอาจจะถูกมองเป็นวัตถุแบบfunction(ก็คือexponential) ในอีกcategoryหนึ่ง นี่เป็นจริงหรือเปล่า?
เรามาดูที่ลำดับชั้นของความabstractionที่เราได้สร้างมาจนถึงจุดนี้ เราเรื่มจากcategoryที่คือกลุ่มของวัตถุและmorphism categoryมันเอง(หรือถ้าให้พูดอย่างถูกต้อง categoryขนาดเล็กที่วัตถุก่อเป็นset)เป็นวัตถุในcategoryที่สูงกว่า\(\textbf{Cat}\) moprhismsในcategoryนั้นคือfunctor hom-setใน\(\textbf{Cat}\)คือsetของfunctor ตัวอย่างเช่น\(\textbf{Cat}(\textbf{C}, \textbf{D})\)คือsetของfunctor ระหว่างcategoryสองตัวอย่าง\(\textbf{C}\)และ\(\textbf{D}\)
cateogryของfunctor\([\textbf{C},\textbf{D}]\)นั้นก็เป็นsetของfunctorระหว่างcategoryทั้งสอง (บวกกับการแปลงแบบธรรมชาติในฐานะmorphism) วัตถุต่างๆของมันนั้นเหมือนกับสมาชิกของ\(\textbf{Cat}(\textbf{C},\textbf{D})\) มากไปกว่านั้นcategoryของfunctor ในการที่เป็นcategoryต้องเป็นวัตถุของ\(\textbf{Cat}\) (ดังนั้นcategoryของfunctorระหว่างcategoryขนาดเล็กสองตัวก็มีขนาดเล็กเอง) เรามีความสัมพันธ์ระหว่างHom-setและวัตถุในcategoryเดียวกัน สถานการณ์นี้นั้นเหมือนกับวัตถุexpoenentialที่เราได้เห็นได้เห็นในส่วนก่อนหน้า เรามาดูในวิธีการที่เราสร้างมันใน\(\textbf{Cat}\)
คุณอาจจะจำได้ในการที่จะสร้างexponential เราต้องการที่จะนิยามproduct ใน\(\textbf{Cat}\)ที่เป็นสิ่งที่ค่อนข้างง่ายเพราะว่าcategoryขนาดเล็กเป็นsetของวัตถุ และเรารู้วิธีการในการนิยามproductแบบCartesianของset ดังนั้นวัตถุในcategoryแบบproduct\(\textbf{C}\times\textbf{D}\)คือแค่คู่ของวัตถุ\((c,d)\)ที่ตัวหนึ่งมาจาก\(\textbf{C}\)และอีกตัวมาจาก\(\textbf{D}\) ในทางเดียวกันmorphismระหว่างสองคู่\((c,d)\)และ\((c',d')\)คือคู่ของmorphism\((f,g)\)ที่\(f::c\rightarrow c'\)และ\(g::d\rightarrow d'\) คู่เหล่านี้ของmorphismประกอบกันในแต่ละส่วนประกอบ และมันก็จะมีคู่ที่เป็นidentityที่ก็คือmorphismแบบidentityของคู่นั้น โดยสรุปแล้ว\(\textbf{Cat}\)คือcategoryแบบCartesian closedอย่างเต็มที่ที่ ที่ได้มีวัตถุexponential\(\textbf{D}^\textbf{C}\)ในทุกๆคู่ของcategory และโดย”วัตถุ“ใน\(\textbf{Cat}\)ผมหมายถึงcategory ดังนั้น\(\textbf{D}^\textbf{C}\)คือcategoryที่ที่เราสามารถเห็นเป็นcategoryของfunctorระหว่าง\(\textbf{C}\)และ\(\textbf{D}\)
11.4 2-Category
ในการที่เราได้เข้าใจcategoryของfunctor เรามาดูอย่างใกล้ๆที่\(\textbf{Cat}\) โดยนิยามแล้วHom-setใดๆก็ตามใน\(\textbf{Cat}\)คือsetของfunctor ก่อนหน้านี้บอกเราว่าfunctorระหว่างสองวัตถุมีโครงสร้างที่หรูหรากว่าแค่set พวกมันก่อให้เกิดcategoryที่คู่กับการแปลงแบบธรรมชาติที่กระทำในฐานะmorphism เนื่องด้วยว่าfunctorนั้นถูกพิจารณาเป็นmorphismใน\(\textbf{Cat}\) การแปลงแบบธรรมชาติจึงเป็นmorphismระหว่างmorphism
โครงสร้างที่หรูหรากว่านี้คือตัวอย่างของ2-category ที่คือการgeneralizeของcategoryที่นอกเหนือจากวัตถุและmorphism (ที่อาจจะถูกเรียกว่า1-morphismในบริบทนี้) ได้มี2-morphismที่ก็คือmorphismระหว่างmorphismด้วย
ในกรณีนี้ของ\(\textbf{Cat}\)ที่มองในฐานะ2-categoryเราก็จะมี
- วัตถุ: category(ขนาดเล็ก)
- 1-morphism: functorระหว่างcategory
- 2-morphism: การแปลงแบบธรรมชาติระหว่างfunctor
แทนที่จะHom-setระหว่างcategoryทั้งสอง\(\textbf{C}\)และ\(\textbf{D}\) เรามีhom-categoryที่ก็คือcategoryของfunctor\(\textbf{D}^\textbf{C}\) เราได้มีการประกอบfunctorแบบทั่วๆไปที่คือfunctor\(F\)จาก\(\textbf{D}^\textbf{C}\)ประกอบกับfunctor\(G\)จาก\(\textbf{E}^\textbf{D}\) เพิ่อที่จะได้\(G\circ F\)จาก\(\textbf{E}^\textbf{C}\) แต่เราก็มีการประกอบกับข้างในของแต่ละHom-category ที่คือการประกอบแนวตั้งของการแปลงแบบธรรมชาติหรือ2-morphismระหว่างfunctor
ด้วยการที่มีสองประเภทของการประกอบกันใน2-categoryเราก็จะมีคำถาม แล้วพวกมันมีปฏิสัมพันธ์อย่างไร
เรามาเลือกสองfunctorหรือ1-morphismใน\(\textbf{Cat}\)
\[ \begin{gather*} F :: \textbf{C} \to \textbf{D} \\ G :: \textbf{D} \to \textbf{E} \end{gather*} \]
และการประกอบของมัน
\[ G\circ F::\textbf{C}\rightarrow \textbf{E} \]
สมมุติว่าเรามีการแปลงแบบธรรมชาติ\(\alpha\)และ\(\beta\)ที่กระทำ ตามลำดับบนfunctor\(F\)และ\(G\)
\[ \begin{gather*} \alpha :: F \to F' \\ \beta :: G \to G' \end{gather*} \]
สังเกตว่าเราไม่สามารถใช้การประกอบกันแบบแนวตั้งกับคู่ๆนี้ก็เพราะว่า เป้าหมายของ\(\alpha\)นั้นแตกต่างจากจุดเริ่มต้นของ\(\beta\) ใ นความจริงแล้วพวกมันคือสมาชิกของcategoryของfunctorที่แตกต่างกัน อย่าง\(\textbf{D}^\textbf{C}\)และ\(\textbf{E}^\textbf{D}\) แต่เราสามารถที่จะใช้การประกอบกันของfunctor \(F'\)และ\(G'\)เพราะว่าเป้าหมายของ\(F'\)นั้นคือที่เริ่มต้นของ\(G'\) ที่คือcategory\(\textbf{D}\) อะไรคือความสัมพันธ์ระหว่างfunctor \(G'\circ F'\)และ\(G\circ F\)ละ?
การที่เรามี\(\alpha\)และ\(\beta\)อยู่พร้อม เราสามารถนิยามการแปลงแบบธรรมชาติจาก\(G'\circ F'\)ไปยัง\(G\circ F\)ได้อย่างไร? ให้ผมได้ร่างการสร้างนี้
เหมือนทั่วไปๆ เราเริ่มจากวัตถุ\(a\)ใน\(\textbf{C}\) ที่imageของมันแยกออกไปเป็นสองวัตถุใน\(\textbf{D}\) ที่คือ\(Fa'\)และ\(F'a\) ก็มีmorphismที่เป็นส่วนประกอบของ\(\alpha\)ในการเชื่อมระหว่างวัตถุทั้งสองอย่าง
\[ \alpha_a :: Fa\rightarrow F'a \]
เราไปจาก\(\textbf{D}\)ไปยัง\(\textbf{E}\)วัตถุเหล่านี้แยกไปต่อไปเป็นสี่วัตถุอย่าง \(G (F a)\), \(G'(F a)\), \(G (F'a)\), \(G'(F'a)\) เราก็มีmorphismสี่ตัวที่ก่อเป็นสี่เหลี่ยม สองmorphismจากทั้งหมดคือส่วนประกอบของการแปลงแบบธรรมชาติ\(\beta\)
\[ \begin{gather*} \beta_{F a} :: G (F a) \to G'(F a) \\ \beta_{F'a} :: G (F'a) \to G'(F'a) \end{gather*} \]
อีกสองตัวคือimageของ\(\alpha_a\)ภายใต้functorทั้งสอง(functorจะทำการโยงmorphismต่างๆ)
\[ \begin{gather*} G \alpha_a :: G (F a) \to G (F'a) \\ G'\alpha_a :: G'(F a) \to G'(F'a) \end{gather*} \]
นั้นก็มีmorphismหลายตัว เป้าหมายของเราคือการหาmorphismที่ไปจาก\(G(Fa)\)ไปยัง\(G'(F'a)\) ส่วนประกอบที่มีคุณสมปัติสำหรับการแปลงแบบธรรมชาติที่เชื่อมทั้งสองfunctor\(G \circ F\) ไปยัง\(G' \circ F'\) ในความเป็นจริงแล้วได้มีไม่เฉพาะแค่หนึ่งแต่เป็นสองเส้นทางที่เราสามารถใช้จาก\(G(Fa)\)ไปยัง\(G'(F'a)\)
\[ \begin{gather*} G'\alpha_a \circ \beta_{F a} \\ \beta_{F'a} \circ G \alpha_a \end{gather*} \]
โชคดีของเราว่าพวกมันเท่ากันเพราะว่าสี่เหลี่ยมที่เราได้สร้างก็คือสี่เหลี่ยมที่เป็นธรรมชาติของ\(\beta\)
เราได้นิยามส่วนประกอบของการแปลงแบบธรรมชาติจาก\(G \circ F\) ไปยัง\(G' \circ F'\) การพิสูจน์ของความเป็นธรรมชาติของการแปลงนี้นั้นค่อนข้างตรงไปตรงมา ถ้าคุณมีความอดทนมากพอ
เราเรียกการแปลงแบบธรรมชาตินี้ว่าการประกอบกันแนวนอนของ\(\alpha\)และ\(\beta\)
\[ \beta\circ\alpha :: G\circ F\rightarrow G'\circ F' \]
อีกครั้งตามมาจากMac Laneผมได้ใช้วงกลมเล็กสำหรับการประกอบกันในแนวนอน ถึงแม้คุณอาจจะเจอการใช้ดาวแทนที่
ในที่นี้หลักการง่ายๆทางcategpryคือในทุกๆครั้งที่คุณมีการประกอบกันตุณควรที่จะตามหาcategory เรามีการประกอบกันในแนวตั้งของการแปลงแบบธรรมชาติและมันเป็นส่วนของcategoryของfunctor แล้วการกอบกันในแนวนอนละ? มันอยู่ในcategoryอะไร?
คำตอบอยู่ที่การมอง\(\textbf{Cat}\)ในด้านข้าง มองที่การแปลงแบบธรรมชาติไม่ในฐานะลูกศรระหว่างfunctorแต่เป็นลูกศรระหว่างcategory การแปลงแบบธรรมชาติที่นีั่งระหว่างcategoryทั้งสอง ที่ที่ได้ถูกเชื่อมโดยfunctorที่มันทำการเปลี่ยนแปลง ราสามารถที่จะคิดถึงมันในฐานะการเชื่อมต่อกันของcategoryทั้งสอง
เรามาให้ความสนใจกับวัตถุทั้งสองของ\(\textbf{Cat}\)นั้นก็คือcategory\(\textbf{C}\)และ\(\textbf{D}\) ได้มีsetของการแปลงแบบธรรมชาติที่ไประหว่างfunctorที่เชื่อมจาก\(\textbf{C}\)ไปยัง\(\textbf{D}\) การแปลงแบบธรรมชาติเหล่านี้คือลูกศรแบบใหม่จาก\(\textbf{C}\)ไปยัง\(\textbf{D}\) ในรูปแบบเดียวกันได้มีการแปลงแบบธรรมชาติระหว่างfunctorที่เชื่อมต่อ\(\textbf{D}\)ไปยัง\(\textbf{E}\) ที่เราสามารถมองมันในฐานะลูกศรแบบใหม่จาก\(\textbf{D}\)ไปยัง\(\textbf{E}\) การประกอบแนวนอนกันคือการประกอบกันของลูกศรเหล่านี้
เราก็มีลูกศรแบบidentityจาก\(\textbf{C}\)ไปยัง\(\textbf{C}\) ที่คือการแปลงแบบธรรมชาติแบบidentity ที่โยงfunctorแบบidentityบน\(\textbf{C}\)ไปยังตัวมันเอง สังเกตว่าidentityสำหรับการประกอบแนวนอนก็เป็นidentityสำหรับการประกอบแนวตั้ง แต่ไม่เป็นในอีกทางหนึ่ง
สุดท้ายแล้วการประกอบกันทั้งสองอยู่ในกฎของการแลกเปลี่ยน
\[ (\beta'\cdot\alpha')\circ(\beta\cdot\alpha) = (\beta'\circ\beta)\cdot(\alpha'\circ\alpha) \]
ผมจะอ้างคำของSaunders Mac Laneในที่นี้ว่า นักอ่านในที่อาจจะชอบในการเขียนdiagramนในการพิสูจน์ความจริงข้อนี้
ได้มีเครื่องหมายอีกตัวหนึ่งที่อาจจะมีประโยชน์ในอนาคต ในการตีความแบบด้านข้างของ\(\textbf{Cat}\)นำไปสู่สองวิธีในการไปจากวัตถุไปยังอีกวัตถุ โดยการใช้functorหรือการใช้การแปลงแบบธรรมชาติ แต่เราสามารถที่จะตีความใหม่ของลูกศรfunctorในฐานะการแปลงแบบธรรมชาติแบบพิเศษที่คือการแปลงแบบธรรมชาติที่เป็นidentityที่กระทำบนfunctorนี้ ดังนั้นคุณจะเห็นในบ่อยครั้งเครื่องหมายแบบนี้
\[ F\circ\alpha \]
ที่\(F\)คือfunctorจาก\(\textbf{D}\)ไปยัง\(\textbf{E}\)และ\(\lalpha\)คือการแปลงแบบธรรมชาติระหว่างสองfunctorจาก\(\textbf{C}\)ไปยัง\(\textbf{D}\) เนื่องว่าคุณไม่สามารถที่จะประกอบfunctorกับการแปลงแบบธรรมชาติ สิ่งนี้ถูกตีความในฐานะการประกอบแนวนอนของการแปลงแบบธรรมชาติแบบidentity\(1_F\)หลัง\(\alpha\)
ในทางเดียวกัน
\[ \alpha\circ F \]
คือการประกอบแนวนอนของ\(\alpha\)หลัง\(1_F\)
11.5 สรุป
บทนี้คือจุดสิ้นสุดของส่วนแรกของหนังสือเล่มนี้ เราได้เรียนคำศัพท์พื้นฐานของทฤษฎีcategory คุณอาจจะคิดถึงวัตถุและcategoryในฐานะคำนาม และmorphism functorและการแปลงแบบธรรมชาติในฐานะคำกริยา morphismที่เชื่อมต่อวัตถุ functorเชื่อมต่อcategoryและการแปลงแบบธรรมชาติเชื่อมต่อfunctor
แต่เราก็ได้เห็นแล้วว่าสิ่งที่ดูเหมือนการกระทำในลำดับของความนามธรรม(abstraction)กลายมาเป็นวัตถุในอีกลำดับหนึ่ง setของmorphismกลายมาเป็นวัตถุประเภทfunction ในฐานะวัตถุ มันสามารถที่จะเป็นจุดเริ่มต้นหรือเป้าหมายของmorphismอีกอัน นั้นก็คือแนวคิดข้างหลังfunctionแบบhigher order
functorนั้นโยงวัตถุไปยังวัตถุ ดังนั้นเราสามารถที่จะใช้มันในฐานะconstructorของtypeหรือtypeแบบparametric functorนั้นก็โยงmorphismต่างๆดังนั้นมันก็คือfunctionแบบhigher order(fmap
) ได้มีfunctorเรียบง่ายบางตัวอย่างConst
productหรือcoproductที่สามารถถูกใช้ในการสร้างtypeข้อมูลแบบพีชคณิตที่หลากหลายมากมาย typeแบบfunctionนั้นก็มีความเป็นfunctorทั้งแบบcovariantและcontravariantและสามารถถูกใช้ในการขยายtypeข้อมูลแบบพีชคณิต
functorอาจจะถูกมองในฐานะวัตถุในcategoryของfunctor ในแบบนั้นแล้วพวกมันกลายมาเป็นจุดเริ่มต้นและเป้าหมายของmorphismนั้นก็คือการแปลงแบบธรรมชาติ โดยที่การแปลงแบบธรรมชาติคือประเภทพิเศษของfunctionแบบpolymorphic
11.6 โจทย์ท้าทาย
- ลองนิยามการแปลงแบบธรรมชาติจากfunctor
Maybe
ไปยังfunctorของlistและพิสูจน์เงื่อนไขความเป็นธรรมชาติสำหรับมัน - นิยามการแปลงแบบธรรมชาติอย่างน้อยสองตัวที่แตกต่างกัน ระหว่าง
Reader ()
และfunctorของlist แล้วได้มีlistที่ไม่เหมือนกันของ()
อยู่เท่าไหร่? - ต่อเนื่องจากข้อที่แล้วมาลองทำกับ
Reader Bool
และMaybe
- ลองแสดงว่าการประกอบแนวนอนของการแปลงแบบธรรมชาติได้ตามเงื่อนไขความเป็นธรรมชาติ(คำใบ้:ลองใช้ส่วนประกอบต่างๆ)มันคือฝึกฝนที่ดีของการไล่diagram(diagram chasing)
- ลองเขียนเรียงความขนาดสั้นเกี่ยวกับการที่คุณอาจจะสนุกกับการเขียนdiagramออกมาในความจำเป็นในการพิสูจน์กฏของการสลับหมู่
- ลองสร้างกรณีทดสอบสำหรับเงื่อนไขความเป็นธรรมชาติระหว่างfunctor
Op
ต่างๆกัน นี้คือตัวเลือกหนึ่ง
op :: Op Bool Int
= Op (\x -> x > 0) op
และ
f :: String -> Int
= read x f x
คุณสามารถที่จะอ่านต่อเกี่ยวกับทฤษฎีบทที่ได้มาโดยไม่ต้องทำอะไรในblogของผม”ความเป็นparametric: เงินไม่สำหรับอะไรเลยและทฤษฎีบทที่ได้มาโดยไม่ต้องทำอะไร” (Parametricity: Money for Nothing and Theorems for Free)↩︎