7 Typeข้อมูลแบบAlgebraicอย่างง่าย (Simple Algebraic Data Types) (Draft)

เราได้เห็นสองวิธีพื้นฐานในการรวมtypeเข้าด้วยกันผ่านการใช้productและcoproduct มันกลับเป็นว่าdata structureหลายๆตัวที่ถูกใช้ในการเขียนโปรแกรมในทุกๆวันสามารถถูกสร้างขึ้นมาจากกลไกทั้งสองนี้ ความจริงข้อนี้มีผลที่ตามมาในทางการปฏิบัติที่สำคัญเป็นอย่างมาก หลายคุณสมบัติของdata structureสามารถประกอบกันได้ ตัวอย่างเช่นถ้าคุณรู้วิธีการที่จะเปรียบเทียบความเท่ากันของค่าของtypeพื้นฐานและคุณรู้วิธีการที่จะการgeneralize การเปรียบเทียบเหล่านี้ไปยังtypeของproductและcoproduct คุณก็สามารถที่จะทำให้การสร้าง(derive)วิธีการในการเปรียบเทียบความเท่ากันสำหรับtypeผสมโดยอัตโนมัติได้ ในHaskellคุณสามารถที่จะสร้างการเท่ากัน การเปรียบเทียบ การแปลง ไปยังและจากstringและอื่นๆสำหรับtypeผสมอย่างมากมาย

เรามาดูให้ละเอียดมากขึ้นกับproductและtypeประเภทsumในตอนที่มันปรากฏขึ้นมาในการเขียนโปรแกรม

7.1 TypeแบบProducts

ในการเขียนแบบมาตราฐานของproductระหว่างสองtypeการเขียนโปรแกรมคือpair ในHaskell pairนั้นเป็นconstructorของtypeที่เป็นprimitive ในC++มันคือtemplateที่ถูกนิยามในlibaryมาตราฐานที่ค่อนข้างที่จะชับช้อนเมื่อเทียบกับอย่างอื่น

จริงๆแล้วPairนั้นไม่สามาถสลับที่ได้ โดยตัวอย่างเช่น pairของ(Int, Bool)ไม่สามารถที่จะแทนที่pairของ(Bool, Int)ถึงแม้พวกมันจะถือข้อมูลชุดเดียวกันแต่พวกมันสามาถสลับที่ได้แค่จนถึงแค่ความisomorphism isomorphismถูกแสดงโดยfunctionswapที่ก็เป็นinverseของมันเอง

swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)

คุณสามารถที่จะคิดถึงpairทั้งสองตัวในการใช้รูปแบบที่แตกต่างกันออกไปในการเก็บข้อมูลเดียวกัน ก็เหมือนกันกับbig endianและlittle endian

คุณสามารถที่จะผสมtypeต่างๆกันเท่าไหร่ก็ได้เพื่อที่จะได้เป็นproductของpairต่างๆที่อยู่ข้างในpairอีกที (และไปเรื่อยๆ) แต่ก็มีวิธีที่ง่ายกว่าpairในpair(nested pair)นั้นก็คือพวกมันเท่ากับtuple มันเป็นผลเนื่องมาจากความจริงที่ว่า หลายวิธีในการนำpairเข้าไปในpairนั้นisomorphicชึ่งกันและกัน ถ้าคุณต้องการที่จะรวมtypea,bและcสามอย่างในproductตามลำดับ คุณสามารถที่จะทำมันได้ในสองรูปแบบ

((a, b), c)

หรือ

(a, (b, c))

typeเหล่านี้นั้นแตกต่างกัน (คุณไม่สามารถที่จะนำเข้าสู่functionที่คาดหวังไว้แบบหนึ่ง) แต่สมาชิกของพวกมันนั้นมีความตรงกันในแบบหนึ่งต่อหนึ่ง ได้มีfunctionที่โยงตัวหนึ่งไปยังอีกตัว

alpha :: ((a, b), c) -> (a, (b, c))
alpha ((x, y), z) = (x, (y, z))

และfunctionนี้สามารถถูกinverseได้

alpha_inv :: (a, (b, c)) -> ((a, b), c)
alpha_inv (x, (y, z)) = ((x, y), z)

ดังนั้นมันคือisomorphism แบบนี้ก็คือวิธีที่แตกต่างกันในการบรรจุใหม่ข้อมูลที่เหมือนกัน

คุณสามารถที่จะตีความการสร้างtypeแบบproductในฐานะoperator binaryลงในtypeต่างๆ จากมุมมองนี้isomorphismข้างบนดูเหมือนกฏการเปลี่ยนหมู่ที่เราเห็นในmonoid

$(a * b) * c = a * (b * c)$

ยกเว้นว่าในตัวอย่างของmonoid วิธีการประกอบกันของproductทั้งสองแบบนั้นเท่ากัน ในขณะที่ในที่นี่มันแค่เท่ากันจนถึงความisomorphism

ถ้าเราสามารถที่จะอยู่กับisomorphismต่างๆได้และไม่ต้องยืนยันในความเท่ากับแบบเคร่งครัด เราสามารถที่จะไปไกลออกไปมากกว่านี้และสามารถแสดงให้เห็นว่าtypeแบบunit() คือunitของproductในแบบเดียวกันกับวิธีการที่ $1$ คือunitของการคูณ แน่นอนว่าการpairกันระหว่างค่าของtypeaบางอย่างกับunitไม่ได้เพิ่มข้อมูลเข้ามา typeอย่างที่

(a, ())

นั้นisomorphicกับaและนี่คือisomorphismระหว่างกัน

rho :: (a, ()) -> a
rho (x, ()) = x

rho_inv :: a -> (a, ())
rho_inv x = (x, ())

ข้อสังเกตเหล่านี้สามารถถูกformalizedโดยการบอกว่า $Set$ (categoryของset)นั้นเป็นcategoryแบบmonoidal มันคือcategroyที่ก็เป็นmonoidในความหมายเดียวกันกับการที่คุณสามารถคูณหลายวัตถุต่างๆเข้าด้วยกัน (ในที่นี้คือการนำproduct cartesianมาใช้) ผมจะพูดเกี่ยวกับcategory monoidalมากขึ้นและให้นิยามที่สมบูรณ์ในอนาคต

ได้มีวิธีในการนิยามtypeแบบproductที่ทั่วไปมากกว่านี้ในHaskell โดยเฉพาะ(ในการที่เราจะได้เห็นเร็วๆนี้)ในตอนที่มีการรวมมันเข้ากับtypeประเภทsum มันได้ใช้constructorที่มีชื่อ(named constructors)ที่มีargumentหลายตัว ตัวอย่างเช่นpairที่สามารถที่จะถูกนิยามในอีกแบบหนึ่งว่า

data Pair a b = P a b

ในที่นี้Pair a bคือชื่อของtypeที่มีparameterเป็นtypeอีกสองประเภทaและb และPคือชื่อของconstructorของข้อมูล คุณนิยามtypeแบบpairโดยการนำสองtypeเข้าไปยังPairที่เป็นconstructorของtype คุณสร้างค่าของpairโดยการนำค่าทั้งสองค่าในtypeที่ถูกต้องเข้าไปยังconstructorP ตัวอย่างเช่นเรามานิยามค่าstmtในฐานะpairของStringและBoolว่า

stmt :: Pair String Bool
stmt = P "This statement is" False

ในบรรทัดแรกคือการประกาศtypeที่ใช้constructorของtypePairกับStringและBoolที่แทนที่aและbในนิยาม genericของPair บรรทัดสองคือการนิยามค่าจริงๆโดยการนำstringจริงๆและBooleanจริงๆเข้าไปยังconstructorของข้อมูลP constructorของtypeจะถูกใช้ในการสร้างtypeต่างๆและconstructorข้อมูลจะถูกใช้ในการสร้างค่าต่างๆ

เนื่องว่าname spaceสำหรับconstructorของtypeและข้อมูล นั้นแยกกันในHaskellคุณจะเห็นในบ่อยครั้งว่าชื่อเดียวกันจะถูกใช้ในแบบนี้

data Pair a b = Pair a b

และถ้าคุณสังเกตมันให้ลึกขึ้นคุณก็อาจจะมองtype pairแบบbuilt-inในฐานะอีกแบบหนึ่งของการประกาศในรูปแบบนี้ในที่ที่ชื่อPairถูกแทนที่ด้วยopeartor binary(,) ที่จริงๆแล้วคุณสามารถที่จะใช้(,)เหมือนกันกับconstructorที่มีชื่อและสร้างpairผ่านสัญลักษณ์แบบprefixที่ว่า

stmt = (,) "This statement is" False

ในแบบคล้ายๆกันคุณก็สามารถที่จะใช้ (,,)ในการสร้างtupleและอื่นๆ

แทนที่จะใช้pair genericหรือtupleต่างๆ คุณก็สามารถที่จะนิยามtypeแบบproductที่มีชื่อเฉพาะในแบบนี้

data Stmt = Stmt String Bool

ที่แค่คือproductระหว่างStringกับBoolแต่มีชื่อและconstructorเป็นของตนเอง ข้อดีของรูปแบบของการประกาศแบบนี้คือคุณสามารถที่จะนิยามหลายๆtypeที่มีข้อมูลเดียวกันแต่มีความหมายและการใช้งานที่แตกต่างออกไป และไม่สามารถใช้แทนกันได้

การเขียนโปรแกรมที่มีtupleและconstructorที่มีargumentหลายตัว ก็สามารถที่จะก่อให้เกิดความยุ่งเหยิงและมีโอกาสที่จะเกิดปัญหา ในการที่เราจะติดตามว่าของแต่ละส่วนประกอบเป็นตัวแทนของอะไร มันมักจะดีกว่าที่จะให้ชื่อกับส่วนประกอบต่างๆ type productที่มีชื่อของข้อมูล(named field)จะถูกเรียกว่าrecordในHaskellและstructในC

7.2 Records

เรามาลองดูในตัวอย่างง่ายๆ เราต้องการที่จะอธิบายธาตุในเคมีโดยการรวมสองstringเข้าด้วยกัน ที่ก็คือชื่อกับเครื่องหมายและจำนวนเต็มซึ่งก็คือเลขอะตอมในdata structureเดียว เราสามารถที่จะใช้tuple(String, String, Int)และสามารถจำได้ว่าแต่ละส่วนประกอบเป็นตัวแทนของอะไร เราอาจจะดึงส่วนประกอบต่างๆโดยการการจับคู่รูปแบบ โดยที่functionนี้ตรวจสอบว่าเครื่องหมายของธาตุนั้นเป็นprefixของชื่อของมัน (ในแบบที่Heเป็นprefixของHelium)หรือไม่

startsWithSymbol :: (String, String, Int) -> Bool
startsWithSymbol (name, symbol, _) = isPrefixOf symbol name

โค้ดส่วนนี้นั้นมีความเป็นไปได้ที่มีปัญหาและยากที่จะอ่านและดูแลมัน มันนั้นง่ายกว่าที่จะนิยามเป็นrecord

data Element = Element { name :: String 
                       , symbol :: String 
                       , atomicNumber :: Int }

ในรูปแบบทั้งสองนั้นisomorphicกันโดยที่เห็นได้จากfunctionในการแปลงที่เป็นinverseระหว่างกัน

tupleToElem :: (String, String, Int) -> Element
tupleToElem (n, s, a) = Element { name = n 
                                , symbol = s 
                                , atomicNumber = a }

elemToTuple :: Element -> (String, String, Int)
elemToTuple e = (name e, symbol e, atomicNumber e)

สังเกตได้ว่าชื่อของข้อมูล(field)ในrecordก็สามารถถูกใช้ในฐานะfunctionในการเข้าถึงข้อมูลเหล่านี้ ตัวอย่างเช่นatomicNumber eสามารถดึงข้อมูลatomicNumberจากe เราได้ใช้atomicNumberในฐานะfunctionของtype

atomicNumber :: Element -> Int

คู่กับsyntaxของrecordสำหรับElement functionstartsWithSymbolของเราก็กลายมาเป็นสิ่งที่อ่านได้ง่ายขึ้น

startsWithSymbol :: Element -> Bool
startsWithSymbol e = isPrefixOf (symbol e) (name e)

เราก็อาจจะใช้เคล็ดลับของHaskellโดยการเปลี่ยนfunctionของisPrefixOfไปยังoperator infixโดยการนำbackquotesมาครอบและทำให้มันอ่านคล้ายกับประโยค(ของมนุษย์)

startsWithSymbol e = symbol e `isPrefixOf` name e

วงเล็บสามารถที่จะถูกยกเว้นในตัวอย่างนี้เพราะว่าoperator infixมีลำดับความสำคัญที่ต่ำกว่าการเรียกใช้function

7.3 TypeแบบSum

เหมือนกับการที่productในcategoryของsetนั้นทำก่อให้เกิดtypeแบบproduct coproductก็จะทำให้เกิดtypeแบบsum การเขียนที่เป็นมาตราฐานของtypeแบบsumในHaskellที่ก็คือ

data Either a b = Left a | Right b

และก็เหมือนกับpair Eitherมันสามารถที่จะสลับที่ได้ (ได้จนถึงความisomorphism)ที่สามารถนำEitherมาใส่ในEitherได้ และลำดับการใส่ก็ไม่มีความสำคัญ (จนถึงความisomorphism) ดังนั้นในตัวอย่างเช่นเราสามารถที่จะนิยามsumที่เป็ยแบบtriple

data OneOfThree a b c = Sinistral a | Medial b | Dextral c

และอื่นๆ

มันกลายมาเป็นว่า $Set$ นั้นก็เป็นcategoryแบบmonoidalที่มีความสมมาตรของcoproduct disjoint sumมีบทบาทเป็นoperation binary และวัตถุเริ่มต้นมีบทบาทเป็นสมาชิกunit ในภาษาของtypeเรามีEitherในฐานะoperator monoidalและVoidที่ไม่มีอะไรอยู่เลยในฐานะสมาชิกnaturalของมัน คุณสามารถที่จะคิดถึงEitherในฐานะการบวกและVoidในฐานะเลขศูนย์ แน่นอนว่าการบวกVoidไปยังtypeแบบsumไม่ได้เปลี่ยนแปลงข้อมูลของมันโดยตัวอย่างเช่น

Either a Void

นั้นisomorphicกับa นั่นก็เพราะว่าไม่มีวิธีการที่จะสร้างรูปแบบRightของtypeนี้ (ไม่มีค่าอยู่ในtypeของVoid)สิ่งที่อยู่ในEither a Voidนั้นสร้างมาโดยใช้constructorLeftและพวกมันเก็บค่าของtypeaเอาไว้ ดังนั้นในทางสัญลักษณ์แล้วเราก็จะมี $a + 0 = a$

typeแบบsumนั้นถูกใช้ค่อนข้างที่จะทั่วไปในHaskell แต่สิ่งที่เหมือนกันใน++อย่างunionหรือvariantsนั้นพบได้น้อยกว่า และเหตุผลสำหรับสิ่งนี้คือ

ในสิ่งแรกtypeแบบsumที่ง่ายที่สุดคือแค่การenumeration และถูกเขียนโดยการใช้enumในC++ที่เหมือนกับtypeแบบsumของHaskell

data Color = Red | Green | Blue

หรือในC++

enum { Red, Green, Blue };

และtypeแบบsumที่ง่ายกว่านี้คือ

data Bool = True | False

นั่นก็คือboolที่เป็นprimitiveในC++

typeแบบsumแบบเรียบง่ายที่เก็บข้อมูลของการมีและไม่มีอยู่ของค่า นั้นถูกเขียนได้ในหลายหลายรูปแบบในC++โดยการใช้เคล็ดลับพิเศษและค่าที่เป็น”ไปไม่ได้“อย่างstringว่าง จำนวนลบ null pointersและอื่นๆ การที่มีตัวเลือกแบบนี้(ถ้าต้องการแล้ว)สามารถถูกเขียนในHaskellโดยการใช้typeMaybe

data Maybe a = Nothing | Just a

typeแบบMaybeคือsumระหว่างtypeสองตัว คุณสามารถที่จะเห็นสิ่งนี้ได้ถ้าคุณแยกconstructorทั้งสองไปเป็นtypeเดี่ยวๆ ตัวแรกอาจจะดูเหมือนดังนี้

data NothingType = Nothing

มันคือenumerationที่มีค่าค่าเดียวอย่างNothing ในอีกความหมายหนึ่งมันคือsetที่มีสมาชิกเพียงตัวเดียวที่เท่ากันกับtypeแบบunit() ส่วนตัวที่สอง

data JustType a = Just a

คือการใส่typea เราอาจจะที่เก็บข้อมูลของMaybeอย่าง

data Maybe a = Either () a

ในtypeแบบsumที่ชับช้อนกว่านี้มักจะถูกทำแบบปลอมๆโดยการใช้pointerของC++ pointerสามารถที่จะเป็นได้ทั้งnullหรือที่จะชี้ไปยังtypeบางประเภท ตัวอย่างเช่นtypeแบบlistในHaskellสามารถที่จะถูกนิยามในแบบtypeแบบsum(ที่recursive)ว่า

data List a = Nil | Cons a (List a)

สามารถที่จะถูกแปลไปเป็นC++โดนการใช้เคล็ดลับของnull pointerในการเขียนlistว่าง

template<class A>
class List { 
    Node<A> * _head;
public:
    List() : _head(nullptr) {} // Nil
    List(A a, List<A> l)       // Cons
      : _head(new Node<A>(a, l))
    {}
};

สังเกตได้ว่าconstructorสองตัวของHaskellอย่างNilและConsสามารถที่จะถูกแปลไปยังcostructorListที่ถูกoverloadedคู่กับargumentที่คล้ายๆกัน (ไม่มีค่าอยู่สำหรับNilและค่าlistสำหรับCons)classของListไม่จำเป็นต้องมีชื่อเรียกเพื่อที่จะแยกระหว่างสองส่วนประกอบของtypeแบบsum มันใช้ค่าnullptrที่พิเศษสำหรับ_headในการเก็บข้อมูลแบบNil

แต่ความแตกต่างที่สำคัญระหว่างtypeของHaskellและC++คือการที่data structuresของHaskellนั้นไม่สามารถแก้ไขค่าได้(immutable) ถ้าคุณสร้างวัตถุโดยการใช้constructorเฉพาะ วัตถุนี้จะจำconstructorที่ถูกใช้และargumenที่นำเข้ามาไปโดยตลอด ดังนั้นวัตถุแบบMaybeที่ถูกสร้างในฐานะJust "energy"จะไม่เปลี่ยนไปเป็นNothingเลย ในทางคล้ายๆกันที่listว่างจะว่างไปตลอดและlistที่มีสมาชิกสามตัวก็จะมีสมาชิกสามตัวเดิมไปตลอด

ความที่ไม่สามารถแก้ไขค่าได้ที่ทำให้การสร้างย้อนกลับได้ ถ้ามีวัตถุคุณสามารถที่จะแยกส่วนประกอบมันลงมาจงถึงส่วนต่างๆที่ถูกใช้ในการสร้างมัน การแยกชิ้นส่วนถูกทำผ่านการจับคู่รูปแบบและใช้constructorซ้ำในฐานะรูปแบบ argumentของconstructor(ถ้ามีอยู่)ก็จะถูกแทนที่ด้วยตัวแปร (หรือรูปแบบอื่นๆ)

ประเภทข้อมูลของListมีconstrunctorอยู่สองแบบ ดังนั้นการแยกชิ้นส่วนของListแบบใหนก็ตามก็จะใช้สองรูปแบบที่ตรงกันกับconstructทั้งสอง ตัวหนึ่งคู่กับlistNilและตัวอื่นๆคือlistที่สร้างจากCons ตัวอย่างเช่นนี่คือนิยามของfunctionบนListแบบง่ายๆอย่าง

maybeTail :: List a -> Maybe (List a)
maybeTail Nil = Nothing
maybeTail (Cons _ t) = Just t

ในส่วนแรกของนิยามmaybeTailได้ใช้constructorNilในฐานะรูปแบบและที่คือค่าNothing ในส่วนที่สองใช้constructorConsในฐานะรูปแบบ ที่แทนที่argumentของconstructorแรกด้วยตัวแทนเพราะว่าเราไม่ได้สนใจมัน argumentที่สองที่ไปยังConsนั้นอยู่ภายใต้ตัวแปรt (ผมจะเรียกพวกมันว่าตัวแปลว่าถึงแม้ถ้าให้พูดตามหลักการแล้วพวกมันไม่เคยเปลี่ยนแปลงค่า หลังจากการอยู่ภายใต้expressionแล้ว ตัวแปรจะไม่เปลี่ยนอีกต่อไป) ค่าของการคืนคือJust t ในตอนนี้ขึ้นอยู่กับวิธีการที่Listของคุณที่ถูกสร้างมา มันจะคู่กับเงื่อนไขใดสักข้อ ถ้ามันถูกสร้างโดยการใช้Cons argumentทั้งสองที่ถูกนำมาและดึงออกมา (ตัวแรกก็จะถูกทิ้ง)

ในtypeแบบsumที่มีความซับซ้อนจะถูกเขียนในC++โดยการใช้ลำดับชั้นของclass polymorphic ชุดของclassต่างๆที่มีบรรพบุรุษร่วมอาจจะถูกเข้าใจในฐานะtypeที่หลากหลาย โดยที่มีvtableทำตัวเหมือนตัวระบุที่ถูกซ่อน สิ่งที่ในHaskellสามารถทำได้โดยจับคู่รูปแบบบนconstructorและการเรียกโค้ดเฉพาะทาง ในC++นั้นมาคู่กับการทำปล่อยการเรียกไปยังfunctionแบบvirtualที่ขึ้นอยู่กับpointerแบบvtable

เราจะเห็นไม่ค่อยบ่อยที่unionจะถูกใช้ในฐานะtypeแบบsumในC++ ก็เพราะมีข้อจำกัดที่มากไปในสิ่งที่สามารถเข้าไปยังunionได้ คุณไม่สามารถที่จะนำstd::stringเข้าไปในunionได้ก็เพราะว่ามันมีconstructorในการทำสำเนา (copy constructor)

7.4 AlgebraของTypes

ในการคิดถึงทั้งสองtypeแยกๆกัน productและsumสามารถถูกใช้ในการนิยามdata structureหลากหลายที่มีประโยชน์ แต่จุดแข็งที่แท้จริงมาจากการนำทั้งสองมารวมกัน ในอีกครั้งเรากำลังจะนำพลังของการประกอบมาใช้

เราจะสรุปสิ่งที่เราได้ค้นพบจนถึงตอนนี้ เราได้เห็นโครงสร้าง monoidalที่สลับที่ได้ ที่ทั้งสองเป็นพื้นฐานของระบบtype เรามีtypeแบบsumกับVoidในฐานะสมาชิกnatural และtypeแบบproductที่มีunit type()ในฐานะสมาชิกnatural เราต้องการที่จะคิดถึงทั้งสองในฐานะคล้ายกับการบวกและคูณ ในการเปรียบเทียบนี้Voidอาจจะคู่กับเลขศูนย์และunit()ไปยังอีกเลขหนึ่ง

เราจะมาดูว่าเราจะนำเปรียบเทียบนี้ไปได้ใกลที่สุดได้อย่างไร ตัวอย่างเช่นการคูณโดยเลขศูนย์ก็จะได้เลขศูนย์หรือไม่ ในอีกความหมายหนึ่ง typeแบบproductที่มีส่วนประกอบตัวหนึ่งเป็นVoidนั้นisomorphicกับVoidหรือเปล่า ตัวอย่างเช่นมันเป็นไปได้หรือเปล่าที่จะสร้างpairของIntและVoid

ในการสร้างpair คุณจะต้องมีค่าสองค่า ถึงแม้คุณสามารถที่จะคิดถึงจำนวนเต็มอย่างไรก็ได้ แต่ไม่มีค่าที่อยู่ในtypeVoid ดังนั้นสำหรับtypeaใดๆก็ได้ typeแบบ(a, Void)นั้นไม่มีอะไรค่าอยู่และดังนั้นจึงเท่ากับVoidในอีกความหมายหนึ่ง $a \times 0 = 0$

ในอีกสิ่งหนึ่งที่โยงการบวกและคูณคือคุณสมบัติการแจกแจงอย่าง

$a \times (b + c) = a \times b + a \times c$

แล้วสิ่งนี้จะสามารถที่จะเป็นไปได้ในtypeแบบsumและproductหรือเปล่า ใช่มันเป็นไปได้จนถึงความisomorphismเหมือนทุกๆครั้ง ในด้านช้ายนั้นคู่กับtypeดังนี้

(a, Either b c)

และในด้านขวานี้นคู่กับtypeดังนี้

Either (a, b) (a, c)

นี่คือfunctionที่เปลี่ยนไปในทางหนึ่ง

prodToSum :: (a, Either b c) -> Either (a, b) (a, c)
prodToSum (x, e) =
    case e of
      Left  y -> Left  (x, y)
      Right z -> Right (x, z)

และนี่คือfunctionอีกตัวหนึ่งที่เปลี่ยนไปในทางหนึ่ง

sumToProd :: Either (a, b) (a, c) -> (a, Either b c)
sumToProd e =
    case e of
      Left  (x, y) -> (x, Left  y)
      Right (x, z) -> (x, Right z)

statementcase ofถูกใช้สำหรับการจับคู่รูปแบบข้างในfunction รูปแบบแต่ละรูปแบบก็ถูกตามด้วยลูกศรและexpressionในการประเมินค่าในตอนที่รูปแบบถูกจับคู่ ตัวอย่างเข่นถ้าคุณเรียกprodToSumกับค่าๆนี้

prod1 :: (Int, Either String Float)
prod1 = (2, Left "Hi!")

eในcase eนั้นจะเท่ากับLeft "Hi!" เราจะจับคู่รูปแบบLeft yโดยการแทนที่ Hi!โดยy เนื่องด้วยxได้ถูกจับคู่ไปยัง2แล้ว ผลของส่วนcase ofและfunctionทั้งหมดก็จะเป็นLeft (2, "Hi!")ในแบบที่คาดไว้

ผมจะไม่พิสูจน์ว่าทั้งสองfunctionนั้นเป็นinverseของกันและกันถ้าคุณคิดเกี่ยวกับมัน มันจำเป็นต้องเป็น มันก็คือแค่การบรรจุใหม่อย่างตรงไปตรงมาของเนื้อหาในdata structureทั้งสอง มันคือข้อมูลเดียวกันแค่มีรูปแบบที่ต่างกัน

นักคณิตศาสตร์มีชื่อให้กับmonoidที่มีความสัมพันธ์กันนี้ มันถูกเรียกว่าsemiring มันไม่ใช่ringเพราะว่าเราไม่สามารถนิยามการลบกันของtype นั้นก็คือเหตุผลว่าทำไมsemiringจึงในบางครั้งถูกเรียกว่าrig ซึ่งเป็นการเล่นคำว่า “ringที่ไม่มีตัวn” (ด้านลบ, negative) แต่ยกเว้นสิ่งนี้เราสามารถที่จะได้ประสบการมากมายจากการแปลงstatementที่เกี่ยวกับจำนวนธรรมชาติที่เป็นrig ไปยังstatementที่เกี่ยวกับtype นี่คือตารางในการแปลที่มีสิ่งต่างๆที่เราให้ความสนใจ

Numbers	Types
$0$	`Void`
$1$	`()`
$a + b$	`Either a b = Left a \| Right b`
$a \times b$	`(a, b)` or `Pair a b = Pair a b`
$2 = 1 + 1$	`data Bool = True \| False`
$1 + a$	`data Maybe = Nothing \| Just a`

typeแบบlistนั้นมีความน่าสนใจเป็นอย่างมากเพราะว่ามันถูกนิยามในฐานะคำตอบของสมการ typeที่เรากำลังนิยามโผล่ขึ้นมาในทั้งสองด้านของสมการ

data List a = Nil | Cons a (List a)

ถ้าเราทำการแทนที่สมการแบบทั่วไปและทำการแทนList aด้วยxเราก็จะมีสมการนี้

x = 1 + a*x

เราไม่สามารถที่จะหาค่าได้ในวิธีการทางพีชคณิตแบบดั่งเดิมเพราะว่าเราไม่สามารถลบหรือหารtypeต่างๆได้ แต่เราสามารถลองที่จะแทนที่ไปได้เรื่อยๆที่ที่เราแทนxในด้านขวาด้วย(1+a*x) โดนการใช้คุณสมบัติการแจกแจงก็จะกลายมาเป็นค่าต่างๆในแบบนี้

x=1+a*x
x = 1 + a*(1 + a*x) = 1 + a + a*a*x
x = 1 + a + a*a*(1 + a*x) = 1 + a + a*a + a*a*a*x
...
x = 1 + a + a*a + a*a*a + a*a*a*a...

เราก็จะจบลงที่sumของproduct(ที่เป็นtuple)ที่สามารถถูกนิยามในแบบที่ว่า listนั้นว่างหรือมีสมาชิกเดี่ยวaหรือเป็นpaira*aหรือtriplea*a*aไปเรื่อยๆ นั้นก็คือสิ่งที่listเป็น เป็นstringของaต่างๆ

แต่listก็มีอะไรมากกว่านั้นและเราจะกลับมายังdata structureแบบrecursiveหลังจากที่เราเรียนเกี่ยวกับfunctorและfixed point

การแก้สมการด้วยตัวแปรที่เป็นเครื่องหมาย ที่ก็คือalgebra มันคือสิ่งที่ให้typeมีชื่อว่าtypeข้อมูลแบบalgebraic

สุดท้ายแล้วเราควรที่จะพูดถึงการตีความที่สำคัญเป็นอย่างมากของalgebraของtypeต่างๆ สังเกตว่าproductของสองtypeaและbนั้นต้องมีค่าของtypeaและค่าของtypeb นั่นหมายความว่าtypeทั้งสองต้องอยู่ในtypeแบบproductนั้น sumระหว่างtypeทั้งสองในอีกทางหนึ่งประกอบด้วย ค่าของtypeaหรือค่าของtypeb ดังนั้นมันเพียงพอที่จะให้อย่างใดอย่างหนึ่งอยู่ในtypeแบบsumนั้น และและหรือในทางตรรกศาสตร์(Logic)ก็เป็นsemiringและมันสามารถที่จะถูกโยงไปสู่ทฤษฎีtypeว่า

Logic	Types
false	`Void`
true	`()`
$a ∥ b$	`Either a b = Left a \\| Right b`
$a & & b$	`(a, b)`

การเปรียบเทียบนี้นั้นลงลึกไปได้กว่านี้ นี่คือพื้นฐานของisomorphismของCurry-Howardระหว่างlogicและทฤษฎีtype เราจะกลับมาในตอนที่เราพูดเกี่ยวกับtypeแบบfunction

7.5 โจทย์ท้าทาย

ลองแสดงดูว่ามันมีisomorphismระหว่างMaybe aและEither () a
นี่คือtypeแบบsumที่ถูกนิยามในHaskell

data Shape = Circle Float 
           | Rect Float Float

ในที่นี้เราต้องการที่จะนิยามfunctionอย่างareaที่กระทำบนShape เราทำโดยการใช้การจับคู่รูปแบบต่อconstructorทั้งสอง

area :: Shape -> Float
area (Circle r) = pi * r * r
area (Rect d h) = d * h

ลองเขียนShapeในC++หรือJavaดูในฐานะinterfaceและสร้างclassสองclassอย่างCircleและRect และเขียนareaในรูปของfunctionแบบvirtual

ติดตามมาจากข้อสอง เราสามารถที่จะเพิ่มfunctionใหม่อย่างcircที่คำนวณเส้นรอบวงของShapeเราสามารถที่จะทำมันได้โดยที่ไม่ต้องแตะนิยามของShape

circ :: Shape -> Float
circ (Circle r) = 2.0 * pi * r
circ (Rect d h) = 2.0 * (d + h)

ลองเพิ่มcircไปยังโค้ดของC++หรือJavaแล้วมีส่วนไหนของโค้ดดั้งเดิมที่เราต้องแตะ

ติดตามมาจากข้อสาม ลองเพิ่มSqaureที่เป็นรูปร่างใหม่เข้ามาในShapeและทำการแก้จุดต่างๆที่จำเป็น มีส่วนไหนที่คุณต้องแตะในHaskellเมื่อเทียบกับC++หรือJava(ถึงแม้คุณจะไม่เป็นคนที่เขียนHaskellการแก้ไขนั้นค่อนข้างตรงไปตรงมา)
ลองดูว่า $a + a = 2 \times a$ นั้นจริงในtypeต่างๆ(จนถึงความisomorphism) จำไว้ว่า $2$ นั้นคู่กับBoolโดยตามมาจากตารางการแปลของเรา