3  Typeและfunction (Draft)

Categoryของtypeและfunctionนั้นมีบทบาทสำคัญในการเขียนโปรแกรม ดังนั้นเรามาดูกันว่าtype คืออะไรและทำไมเราต้องการมัน

3.1 ใครต้องการtype?

อาจจะดูเหมือนจะมีการโต้เถียงกันเกี่ยวกับข้อดีต่างๆของ การทำtypeให้static(คงที่)เมื่อเทียบกับการทำtypeให้dynamaic(ไม่ตายตัว) และการทำtypeให้strong(เคร่งครัด)หรือให้weak(ไม่เข้มงวด) ขออนุญาตให้ผมใช้การทดลองทางความคิด(thought experiment)ในการแสดงให้เห็นถึงตัวเลือกต่างๆ ลองจิตนาการว่ามีลิงอยู่หลายล้านตัวอยู่หน้าคีย์บอร์ดคอมพิวเตอร์ที่กำลังกดปุ่มต่างๆแบบสุ่มๆอย่างมีความสุข โดยนำไปสู่ได้สร้างโปรแกรมออกมา แล้วนำมันมาcompileและใช้งาน

ด้วยการที่เป็นภาษาเครื่องจักร การผสมกันของbyteต่างๆแบบไหนก็ได้ที่ถูกเขียนโดยลิงพวกนี้ก็จะสามารถนำมาใช้งานได้ (โดยที่ไม่มีปัญหา) แต่ถ้าเป็นภาษาที่ระดับสูงมากขึ้น เราก็จะรู้สึกยินดีที่compilerนั้นสามารถที่จะตรวจจับปัญหาทางศัพท์(lexical)หรือทางไวยกรณ์(grammatical) ลิงหลายๆตัวอาจจะต้องอดกินกล้วยแต่โปรแกรมที่เหลือจะมีโอกาสที่จะมีประโยชน์มากกว่า การตรวจสอบtypeนั้นป้องกันการเขียนโปรแกรมที่ไร้ความหมายในอีกขั้นหนึ่ง นอกเหนือจากนี้ ถ้าเราใช้ภาษาที่มีtypeแบบdynamic ความไม่ลงลอยกันของtypeก็จะถูกพบในขณะโปรแกรมกำลังทำงาน (runtime) ในภาษาที่มีtypeแบบstrongและถูกตรวจสอบในแบบstatic(strongly typed statically checked) ความไม่ลงลอยของtypeก็จะถูกพบในขณะcompile ซึ่งเป็นการขจัดโปรแกรมที่ไม่ถูกต้องก่อนการที่มันจะมีโอกาสที่จะถูกใช้งานเสียอีก

ดังนั้นคำถามคือว่า เราต้องการให้ลิงพวกนี้มีความสุขหรือเราต้องการที่จะสร้างโปรแกรมที่ถูกต้อง

จุดมุ่งหมายทั่วๆของการทดลองทางความคิดนี้คือการเขียนงานของShakespeareใหม่ทั้งหมด โดยการที่มีการตรวจสอบการสะกดและไวยกรณ์ในขบวนการกในการเขียนก็จะเพิ่มความเป็นไปได้อย่างเห็นได้ชัด ในทางคล้ายๆกันการตรวจสอบtypeอาจจะเลยไปถึงการที่จะให้มั่นใจว่า หลังจากที่Romeoได้ถูกประกาศว่าเป็นมนุษย์ เขาจะไม่มีใบไม้งอกออกมาหรือดักจับphotonในสนามแรงโน้มถ่วงที่ทรงพลังของเขา

3.2 Typeต่างๆนั้นเกี่ยวกับการประกอบ

ทฤษฎีcategoryนั้นเกี่ยวกับการประกอบกันของลูกศร แต่ไม่ใช่แค่ลูกศรสองอันที่จะสามารถถูกนำมาประกอบกันได้ วัตถุเป้าหมายของลูกศรหนึ่งต้องเหมือนกับวัตถุเริ่มต้นของลูกศรถัดไป โปรแกรมจะไม่สามารถทำงานได้ถ้าfunctionเป้าหมายไม่สามารถที่จะอ่านข้อมูลที่สร้างมาจากfunctionเริ่มต้นได้อย่างถูกต้อง จุดเริ่มและจุดจบของทั้งสองลูกศรต้องเข้ากันได้ ถ้าจะให้การประกอบกันเป็นไปได้ ระบบtypeที่มีความเคร่งครัดมาเท่าไหร่การจับคู่นี้ก็สามารถถูกอธิบายและถูกตรวจสอบโดยกลไกต่างๆได้ดีมากเท่านั้น

ข้อโต้แย้งที่จริงจังอย่างเดียวที่ผมได้ยินต่อการตรวจสอบtypeแบบ staticและstrongคือการที่มันอาจจะขจัดโปรแกรมบางตัวที่ถูกต้องในทางความหมาย ในทางปฏิบัติแล้วการที่สิ่งแบบนี้จะเกิดขึ้นค่อนข้างที่จะเป็นไปไม่ได้ และอย่างไรก็ตามทุกๆภาษาก็จะมีช่องทางประตูหลังในการที่จะก้าวข้ามระบบtypeในตอนที่มีความจำเป็นจริงๆ แม้กระทั้งในHaskellก็มี unsafeCoerceแต่สิ่งเหล่านี้ควรที่จะถูกใช้อย่างรอบคอบ ตัวละครของFranz Kafkaอย่างGregor Samsaได้ทำลายระบบtypeในตอนที่เขาเปลี่ยนไปเป็นแมลงตัวใหญ่และเราทั้งหมดก็รู้ว่าจุดจบคืออะไร

ข้อโต้แย้งอีกอย่างหนึ่งที่ผมได้ยินเป็นประจำคือการที่การทำงานกับtypeเป็นการโยนภาระไปยังโปรแกรมเมอร์กมากจนเกินไป ผมสามารถที่จะเข้าใจกับความรู้สึกนี้หลังจากการเขียนการประกาศiteratorsในC++ด้วยตัวเอง ยกเว้นแต่ว่าได้มีเทคโนโลยีที่เรียกว่า type inference (การคาดเดาtype) ที่อนุญาตให้compilerคาดเดาtypeเกือบทั้งหมดจากบริบทที่มันถูกใช้งาน ในC++คุณสามารถที่จะประกาศตัวแปรเป็น auto และก็ให้compilerตามหาtypeของมัน

ในHaskellนอกเหนือจากโอกาสที่เป็นไปได้ยากมาก การมีคำอธิบาย(annotation)ต่อtypeนั้นไม่ต้องจำเป็นที่มี ถึงอย่างไรก็ตามโปรแกรมเมอร์มีแนวโน้มที่จะใช้มัน ก็เพราะว่าสิ่งเหล่านี้มีสามารถที่จะบอกได้หลายๆอย่างเกี่ยวกับความหมายของcode และก็สามารถทำให้ข้อผิดพลาดในการcompileง่ายต่อการเข้าใจ มันเป็นหลักปฏิบัติทั่วไปในHaskellที่จะเริ่มprojectโดยการออกแบบtypeต่างๆ โดยหลังจากนั้นคำอธิบายของtypeก็จะเป็นแรงขับเคลื่อนในการเขียนcode และกลายมาเป็นcommentsที่บังคับใช้โดยcompiler (compiler-enforced)

ประเภทtypeที่เคร่งครัดและคงที่มักจะถูกใช้ในฐานะข้ออ้างในการไม่ทำการทดสอบcodeที่ถูกเขียน คุณอาจจะได้ยินในบางครั้งโดยโปรแกรมเมอร์Haskellที่จะพูดว่า “ถ้ามันสามารถที่จะถูกcompileได้แล้วมันจำเป็นต้องถูก” แน่นอนว่ามันไม่มีการรับประกันว่าโปรแกรมที่ถูกในเชิงของtype จะถูกในความหมายในการผลิตผลลัพธ์ที่ถูกต้อง ผลของทัศนคติที่มีความประมาทคือการที่ในหลายการศึกษาHaskellไม่ได้นำหน้าไปอย่างมากในด้านคุณภาพของcodeที่ถูกเขียนอย่างที่คาดคิดไว้ เราอาจจะมองได้ว่าในเชิงพาณิชย์แรงกดดันในการแก้bugนั้นถูกบังคับให้อยู่แค่ในบางระดับของคุณภาพ ซึ่งทั้งหมดก็เกี่ยวกับเศรษฐศาสตร์ของการการพัฒนาซอฟต์แวร์และความอดทนของend user แต่มักจะไม่เกี่ยวกับภาษาโปรแกรมหรือวิธีวิทยา (methodology) บรรทัดฐานที่ดีกว่านี้ก็อาจจะเป็นการวัดจำนวนของprojectsที่ล่าช้ากว่ากำหนดหรือถูกส่งมอบแต่มีฟังก์ชันการทำงานที่ลดลงไปอย่างมาก

สำหรับข้อโต้แย้งที่ว่าการทำunit testingสามารถที่จะแทนที่ประเภทtypeที่เคร่งครัดและคงที่ ให้ลองคิดถึงการrefactoringแบบทั่วๆไปในภาษาที่มีประเภทtypeที่เคร่งครัดอย่างการเปลี่ยนแปลงtypeของargumentในfunctionบางตัว ในภาษาที่มีประเภทtypeที่เคร่งครัดมันนั้นมากพอที่จะเปลี่ยนการประกาศของfunctionนั้นและก็แก้การbuildที่เสียหาย ในภาษาที่typeเป็นแบบไม่เข้มงวด ความจริงที่ว่าfunctionในตอนนี้คาดหวังข้อมูลที่แตกต่างออกไป ก็จะไม่สามารถถูกเผยแพร่ในที่ที่มีการนำมันมาใช้งานใได้1 การทำUnit testingอาจจะจับความไม่เข้ากันนี้ได้แต่การtestนั้นมีขึ้นอยู่กับโชค(ในการเจอปัญหา)แทนที่จะเป็นกระบวนการที่กำหนดได้อย่างสม่ำเสมอมา การtestคือตัวแทนที่ไม่ดีสำหรับการพิสูจน์

3.3 Typesต่างๆคืออะไร

ภาพ(intuition)ที่ง่ายที่สุดของtypeคือการมองมันเป็นsetของค่าต่างๆ typeอย่างBool (อย่าลืมว่าtypeที่เป็นรูปธรรม (concrete types)จะเริ่มด้วยตัวพิมพ์ใหญ่ในภาษาHaskell) คือsetที่มีสองสมาชิกอย่าง True และ False typeอย่างCharคือsetของตัวอักษรUnicodeทั้งหมกอย่าง a หรือ ą

setเหล่านี้สามารถมีขนาดที่จำกัดหรือไม่จำกัด typeอย่างStringที่ก็คือlistของCharที่คือตัวอย่างของsetที่มีจำนวนไม่จำกัด

ในตอนที่เราประกาศxให้เป็นInteger

x :: Integer

เรากำลังบอกว่ามันคือสมาชิกของsetของจำนวนเต็ม IntegerในHaskellคือsetที่มีจำนวนไม่จำกัดและมันสามารถนำมาใช้ในการทำการคำนวนที่กำหนดความเที่ยงตรงได้ (arbitrary precision arithmetic) มันก็มีsetที่จำกัดอย่างIntที่จะสอดคล้องกับประเภทของเครื่อง ที่ก็เหมือนกับintของC++

แต่ก็จะมีรายละเอียดปลีกย่อยที่ทำให้การมองtypeและsetแบบนี้ยุ่งยาก ได้มีปัญหากับfunctionแบบpolymorphicที่เกี่ยวข้องกับการนิยามเป็นวงกลมและความจริงที่ว่าคุณไม่สามารถมีsetของsetทั้งหมดได้ แต่ตามที่ผมให้สัญญาเอาไว้ผมจะไม่เคร่งกับคณิตศาสตร์มาก สิ่งที่ดีคือมันมีcategoryของsetต่างๆที่เราจะเรียกว่า\(\textbf{Set}\) และเราจะแค่ทำงานกับมัน ใน\(\textbf{Set}\)นั้นวัตถุคือsetและmorphism(ลูกศร)คือfunctionต่างๆ

\(\textbf{Set}\)นั้นเป็นcategoryที่พิเศษอย่างมากเพราะว่าเราสามารถที่จะมองเข้าไปในวัตถุต่างๆของมันได้และได้ความเข้าใจจากการทำแบบนี้ ตัวอย่างเช่น เรารู้ว่าเซตว่างนั้นไม่มีสมาชิก เรารู้ว่ามันมีsetพิเศษที่มีสมาชิกอยู่ตัวเดียว เรารู้ว่าfunctionจะโยงสมาชิกของsetหนึ่งๆไปยังสมาชิกของอีกsetหนึ่ง มันสามารถที่จะโยงสองสมาชิกไปยังหนึ่งแต่ไม่สามารถมาจากหนึ่งสมาชิกไปยังสองได้ เรารู้ว่า function identityโยงแต่ละสมาชิกของsetนั้นสู่ตัวเองและอื่นๆอีกมาก จุดหมายของเราคือการที่จะค่อยๆลืมข้อมูลพวกนี้และเขียน(แปลง)แนวคิดเหล่านี้ในแบบcategoryทั้งหมด นั่นก็คือให้อยู่ในแบบของวัตถุและลูกศร

ในโลกอุดคติเราก็อาจจะพูดได้ว่าtypeของHaskellคือsetและfunctionของHaskellคือfunctionทางคณิตศาสตร์ระหว่างset แต่ก็จะมีปัญหาเล็กน้อย: functionทางคณิตศาสตร์ไม่ได้ทำการดำเนินการผ่านcodeเลย มันก็แค่รู้คำตอบของปัญหา functionของHaskellมีความจำเป็นที่จะต้องคํานวณคำตอบ นี่จะไม่เป็นปัญหาถ้าเราสามารถได้รับคำตอบในขั้นตอนการคำนวณที่จำกัด โดยไม่คำนึงถึงขนาดของตัวเลข(ที่จะใหญ่อย่างไรก็ได้) แต่ก็มีการคํานวณบางประเภทที่ข้องที่เกี่ยวกับการrecursionและที่ที่อาจจะไม่มีวันยุติ เราไม่สามารถแค่สั่งห้ามไม่ให้มีfunctionที่ไม่สามารถยุติได้ในHaskellก็เพราะว่าการแยกแยะระหว่างfunctionที่ยุติได้และยุติไม่สามารถทำได้ ที่ก็คือปัญหาการยุติการทำงาน (Halting Problem) ที่โด่งดังเป็นสิ่งที่กำหนดไม่ได้ (undeciable) นั่นจึงเป็นเหตุผลที่ว่าทำไมนักวิทยาศาสตร์คอมพิวเตอร์ จึงคิดค้นแนวคิดที่ฉลาดเป็นอย่างมาก หรือเป็นการhack(ในความหมายที่เป็นการแก้ปัญหาเฉพาะหน้า)ที่สำคัญ แล้วแต่มุมมองของคุณ โดยการขยายtypeทุกประเภทด้วยค่าพิเศษเพียงอย่างเดียวที่เรียกว่า bottom(ตัวล่าง) โดยถูกเขียนว่า _|_ หรือในUnicodeอย่าง ⊥ ค่าๆนี้ตรงกับการคำนวนที่ไม่มีที่สิ้นสุด functionนี้จะถูกประกาศอย่าง:

f :: Bool -> Bool

โดยที่มันอาจจะคืนค่าเป็น True, False หรือ _|_ โดยอย่างหลังหมายความว่ามันจะไม่มีทางสิ้นสุด

น่าสนใจอยู่ว่า หลังจากการที่คุณยอมรับbottomในฐานะส่วนๆหนึ่งของระบบtype มันเป็นการสะดวกที่จะคิดถึงทุกๆข้อผิดพลาดในขณะดำเนินการในฐานะbottom หรือก็อาจจะอนุญาตfunctionทำการคืนbottomกลับมาอย่างโจ่งแจ้ง การทำอย่างหลังสามารถทำได้โดยทั่วไปโดยการใช้ คำเฉพาะอย่าง undefined ในแบบที่ว่า:

f :: Bool -> Bool
f x = undefined

นิยามนี้ผ่านการตรวจสอบtypeได้ก็เพราะว่า undefined ถูกตีค่าเป็น bottom ซึ่งก็เป็นสมาชิกของทุกๆtype รวมไปถึง Bool ที่คุณก็สามารถที่จะเขียนว่า

f :: Bool -> Bool
f = undefined

(แบบไม่มี x) เพราะว่า bottom ก็เป็นสมาชิกของtype Bool -> Bool

functionที่อาจจะคืนค่าbottonจะถูกเรียกว่าfunctionไม่สมบูรณ์(partial)ตรงกันข้ามกับfunctionสมบูรณ์(total)ที่จะคืนผลลัพธ์ที่ใช้ได้สำหรับargumentที่เป็นไปได้ทั้งหมด

เพราะว่าbottom คุณจะเห็นได้ว่าcategoryของtypesและfunctionในHaskellจะถูกเรียกถึงว่า \(\textbf{Hask}\)แทนที่จะเป็น\(\textbf{Set}\) จากมุมมองเชิงทฤษฎีแล้ว นี่เป็นเหมือนจุดเริ่มต้นของความซับซ้อน (complication) ดังนั้นในจุดๆนี้ผมจะใช้มีดทำครัวของผมและยุติแนวทางของความคิดไว้แค่นี้(line of reasoning) ในมุมมองเชิงปฏิบัติมันเป็นไปได้ที่จะไม่ต้องสนใจfunctionที่ไม่ยุติและbottom และมอง\(\textbf{Hask}\)ให้เป็นยังกับ\(\textbf{Set}\)จริงๆ2

3.4 แล้วทำไมเราต้องการmodelทางคณิตศาสตร์ ?

ในฐานะที่เป็นโปรแกรมเมอร์ คุณนั้นมีความใกล้ชิดและคุ้นชินกับsyntax และ grammarของภาษาโปรแกรมของคุณ ด้านต่างๆเหล่านี้ของภาษานั้นโดยปกติแล้วถูกอธิบายโดย สัญลักษณ์อย่างเป็นทางการในจุดเริ่มต้นของข้อกำหนดของภาษา แต่ความหมาย (meaning หรือ semantics) ของภาษานั้นยากมากกว่าที่จะอธิบาย มันใช้จำนวนหน้าที่มากกว่ามากๆและนานๆครั้งที่จะเป็นทางการมากพอ ดังนั้นจึงมีการสนทนาระหว่างทนายภาษาและวงการหนังสือที่อุทิศให้กับการตีความของจุดย่อยๆต่างๆของมาตรฐานทางภาษา

ได้มีเครื่องมือที่เป็นทางการในการอธิบายความหมายในภาษาแต่เนื่องด้วยความชับช้อนของพวกมัน มันจึงถูกใช้คู่กับภาษาเชิงวิชาการที่ถูกทำให้ง่ายขึ้น ไม่ใช่ ภาษาโปรแกรมในความเป็นจริงที่มีขนาดใหญ่ หนึ่งในเครื่องมือที่ทำแบบนี้ถูกเรียกว่า ความหมายเชิงการดำเนินงาน (opeartional semantics) ที่อธิบายกลไกของการดำเนินการของโปรแกรมโดยการจำกัดความinterpreterในอุดมคติ ในอีทางหนึ่งความหมายในภาษาที่ใช้ในทางพาณิชย์(industrial) อย่างเช่น C++ นั้นมักจะถูกอธิบายโดยการใช้ การให้เหตุผลเชิงการดำเนินงาน (opeartional reasoning) ที่ไม่เป็นทางการ ส่วนมากอยู่ในแง่ของ “เครื่องจักรนามธรรม”

ปัญหาคือว่ามันเป็นไปได้ยากที่จะพิสูจน์สิ่งต่างๆที่เกี่ยวกับโปรแกรมนั้นๆผ่านความหมายเชิงการดำเนินงาน ในการแสดงคุณสมบัติของprogramจริงๆคุณต้อง “ดำเนินการมัน”ผ่านinterpreterในอุดมคติ

มันไม่สำคัญสำหรับโปรแกรมเมอร์ที่จะไม่เคยทำการพิสูจน์อย่างเป็นทางการกับความถูกต้องของโปรแกรม เรา”คิด”ว่าเราเขียนโปรแกรมที่ถูกต้องเสมอ ไม่มีใครนั่งอยู่หน้าคีย์บอร์ดแล้วพูดว่า “เราแค่จะเขียนโค้ดเพียงไม่กี่บรรทัดและดูว่ามันจะเกิดอะไรขึ้น” เราคิดว่าโค้ดที่เราเขียนจะกระทำการบางอย่างที่จะนำไปสู่ผลที่เราต้องการ โดยปกติเราก็จะประหลาดใจในตอนที่มันไม่เป็นแบบนั้น นั้นหมายความว่าเราให้เหตุผลจริงๆเกี่ยวกับโปรแกรมที่เราเขียนและเราทำมันโดยปกติโดยการใช้งานinterpreterในหัวของเรา มันก็แค่ยากมากที่จะติดตามตัวแปรทั้งหมด คอมพิวเตอร์นั้นเก่งในการดำเนินการโปรแกรม มนุษย์นั้นไม่ค่อย แต่ถ้าเราเก่งแล้วจะมีคอมพิวเตอร์ไปทำไม

แต่เราก็มีทางเลือกอื่นๆ มันถูกเรียกว่าความหมายเชิงสัญลักษณ์(denotational semantics)ที่มีพื้นฐานมาจากคณิตศาสตร์ ในความหมายเชิงสัญลักษณ์ทุกๆสิ่งที่สร้างจากการเขียนโปรแกรมจะมีการตีความทางคณิตศาสตร์ ในแบบนี้แล้วถ้าคุณต้องการที่จะพิสูจน์คุณสมบัติของโปรแกรม คุณแค่ต้องพิสูจน์ทฤษฎีบททางคณิตศาสตร์ คุณอาจจะคิดว่าการพิสูจน์ทฤษฎีบทนั้นยากแต่ความจริงที่ว่าเรามนุษย์ได้ทำการสร้างวิธีการทางคณิตศาสตร์มาแล้วหลายพันปี เพราะฉะนั้นจึงมีความรู้ที่สั่งสมเป็นจำนวนมากที่เราสามารถนำมาใช้ได้ แล้วก็ถ้านำมันมาเปรียบเทียบกับทฤษฎีบทที่นักคณิตศาสตร์ทำการพิสูจน์ ปัญหาที่เราเจอในการเขียนโปรแกรมนั้นค่อนข้างง่ายไม่ก็ตรงตัวเลย

มาลองดูนิยามของfunction factorialของHaskellที่เป็นภาษาที่ค่อนข้างตรงตามความหมายเชิงสัญลักษณ์อย่าง

fact n = product [1..n]

โดยเครื่องหมาย [1..n] คือlistของจำนวนเต็มจาก 1 ไปยัง n โดยfunctionproductได้ทำการคูณสิ่งที่อยู่ในlistทั้งหมด นั่นก็คือนิยามของfactorialที่มาจากคณิตศาสตร์ เมื่อนำมาเทียบกับการเขียนในCแล้ว:

int fact(int n) {
    int i;
    int result = 1;
    for (i = 2; i <= n; ++i)
        result *= i;
    return result;
}

ผมจำเป็นที่จะต้องพูดอะไรอีกไหม?

Ok ผมจะยอมรับว่านี่ก็เป็นการชกใต้เข็มขัด functionของfactorialนั้นมีการแสดงออกทางคณิตศาสตร์ที่ชัดเจน ผู้อ่านที่มีไหวพริบก็จะอาจจะถามว่า อะไรคือmodelทางคณิตศาสตร์สำหรับการอ่านตัวอักษรจากคีย์บอร์ดหรือการส่งpackageข้ามมาผ่านnetwork เป็นเวลาที่นานมากที่นี่เป็นคำถามที่อึดอัด และนำไปสู่การอธิบายที่สับสน มันราวกับว่าในหลายๆครั้ง ความหมายเชิงสัญลักษณ์ไม่เหมาะสมสำหรับสิ่งที่ต้องมีในการที่เขียนโปรแกรมที่ใช้ได้ และที่ความหมายเชิงการดำเนินงาน(operational semantics)สามารถนำมาใช้ได้ง่ายกว่า พัฒนาแบบก้าวกระโดดนั้นมาจากทฤษฎีcategory โดยที่Eugenio Moggiได้ค้นพบว่าeffectของการคำนวน(computation effect)สามารถถูกผูกไว้กับmonads นี่กลับกลายมาเป็นการสังเกตที่สำคัญ ไม่แค่ทำให้ความหมายเชิงสัญลักษณ์มีชีวิตชีวาขึ้นอีกครั้งและทำให้โปรแกรมที่pureแบบfunctionalสามารถใช้งานได้ง่ายขึ้น แต่ก็ได้ช่วยอธิบายในมุมมองใหม่ต่อการเขียนโปรแกรมแบบดั่งเดิม ผมจะพูดเกี่ยวกับmonadในถัดๆไปในตอนที่เราได้พัฒนาเครื่องมือทางcategoryมากพอแล้ว

หนึ่งในข้อดีที่สำคัญของการมีmodelทางคณิตศาสตร์สำหรับการเขียนโปรแกรมคือความเป็นไปได้ที่จะแสดงการพิสูจน์แบบเป็นทางการของความถูกต้องของsoftware ที่อาจจะดูเหมือนไม่มีความสำคัญมากในตอนที่คุณกำลังเขียนโปรแกรมให้สำหรับผู้บริโภค(ทั่วไป) แต่ในสาขาของการเขียนโปรแกรมที่ค่าของความผิดพลาดอาจจะสูงลิบลิ่วหรือที่ที่มีชีวิตของมนุษย์อยู่ในความเสี่ยง แต่ถึงแม้ในการเขียนapplicationในwebสำหรับระบบทางสุขภาพ คุณอาจจะชื่นชมความคิดที่ว่าfunctionและalgorithmต่างๆจากHaskellในlibraryมาตรฐานมาคู่กับการพิสูจน์ความถูกต้อง

3.5 Functionที่ PureและDirty

สิ่งที่เราเรียกว่าfunctionในC++หรือภาษาimperativeอื่นๆไม่เหมือนกับสิ่งที่เราเรีกว่าfunctionในทางคณิตศาสตร์ functionทางคณิตศาสตร์คือการจับคู่(map)ของค่าไปยังอีกค่า

เราสามารถเขียนfunctionทางคณิตศาสตร์ในภาษาโปรแกรมอย่างเช่น functionในแบบที่ถ้าให้ค่าเป็นinputแล้วก็จะคำนวนค่าคำตอบออกมา functionในการผลิตจำนวนที่เป็นกำลังสองของตัวเลขก็คงที่จะคูณค่าที่เข้ามา กับตนเอง มันจะทำแบบนั้นในทุกที่ที่เรียกมันมาใช้และรับประกันที่จะผลิตคำตอบที่เหมือนกันทุกครั้งในตอนที่มันถูกเรียกโดยinputที่เหมือนกัน กำลังสองของตัวเลขนั้นจะไม่เปลี่ยนต่อข้างขึ้นข้างแรมของดวงจันทร์

แล้วก็การคำนวนกำลังสองของตัวเลขไม่ควรที่จะมีผลข้างเคียง(side effect)อย่างการปล่อยขนมให้กับน้องหมาของคุณ “function”ที่ทำแบบนั้นไม่สามารถถูกmodelในฐานะfunctionทางคณิตศาสตร์ได้อย่างง่ายๆ

ในภาษาในการเขียนโปรแกรม functionที่ผลิตผลลัพธ์ที่เหมือนกันถ้าinputที่ถูกให้มาเป็นแบบเดียวกันและไม่มีผลข้างเคียงจะถูกเรียกว่าfunctionที่pure ในภาษาที่pureแบบfunctionalอย่างHaskell ทุกๆfunctionนั้นเป็นแบบpure เพราะว่าอย่างนี้ มันจึงง่ายกว่าที่จะให้ภาษาพวกนี้ความหมายเชิงสัญลักษณ์และmodelพวกมันผ่านทฤษฎีcategory สำหรับภาษาอื่นๆ มันเป็นไปได้ตลอดที่จะจำกัดตัวเราเองในการใช้functionที่pureอย่างเดียวหรือแยกการให้เหตุผลกับผลข้างเคียงออกไป ต่อไปจากนี้เราจะเห็นการที่monads อนุญาติให้เราmodelทุกๆประเภทของผลต่างๆโดนการใช้functionที่pureอย่างเดียว ดังนั้นเราจะไม่สูญเสียอะไรเลยโดยการจำกัดเราเองกับfunctionทางคณิตศาสตร์

3.6 ตัวอย่างของ Type ต่างๆ

หลังจากที่คุณตระหนักว่าtypeต่างๆคือsetคุณสามารถที่จะคิดถึงtypeบางtypeที่อาจจะแปลกประหลาด ตัวอย่างเช่นอะไรคือtypeที่ตรงกันกับsetว่าง ไม่มันไม่ใช่voidของC++ ถึงแม้typeนี้จะถูกเรียกว่าVoid(ว่างเปล่า)ในHaskell มันคือtypeที่ไม่มีค่าต่างๆอาศัยอยู่ คุณสามารถที่จะนิยามfunctionที่นำVoidเข้ามาแต่คุณจะไม่สามารถท่ีจะเรียกมันได้ ในการที่จะเรียกมัน คุณต้องนำค่าที่อยู่ในtypeVoidและมันไม่มีค่าแบบนี้ ในสิ่งที่functionนี้จะนำกลับมา ก็จะไม่มีข้อจำกัดใดๆทั้งสิ้น มันสามารถที่จะคืนtypeแบบไหนก็ได้ (ถึงแม้มันจะทำไม่ได้เพราะมันไม่สามารถถูกเรียกได้) ในความหมายเดียวกันมันคือfunctionที่polymorphicในtypeของสิ่งที่คืนมา คนที่ใช้งานHaskellมีชื่อสำหรับมัน

absurd :: Void -> a

(เตือนความจำว่าaคือตัวแปรtypeที่สามารถเป็นtypeอะไรก็ได้) ชื่อนี้(absurdแปลว่าไม่สมเหตุผล) ไม่ใช่ความบังเอิญ ได้มีการตีความที่ลึกไปกว่านี้ของtypeและfunctionต่างๆในแง่ของlogicที่เรียกว่าisomorphismของCurry-Howard โดนที่typeVoidแสดงถึงความไม่จริง(falisty)และtypeของfunctionabsurdสอดคล้องกับคำประกาศ(statement)ที่ว่าจากความไม่จริงจะมีอะไรตามก็ได้ เหมือนกับสุภาษิตLatinที่ว่า “ex falso sequitur quodlibet.”

ต่อมาtypeที่ตรงกันกับsetที่มีสมาชิกเพียงตัวเดียว(singleton set)ก็คือtypeที่มีค่าที่เป็นไปได้เพียงอย่างเดียว ค่าค่านี้แค่“มีอยู่” คุณอาจจะไม่เห็นมันโดยทันทีในแบบนั้น แต่นี่คือvoidของC++ ลองคิดต่อfunctionsจากtypeนี้ไปยังสู่typeนี้ functionจากvoidสามารถถูกเรียกได้ตลอด ถ้ามันเป็นfunctionที่pureมันก็จะคืนผลลัพธ์ที่เหมือนกันตลอดเวลา นี่คือตัวอย่างของfunctionแบบนี้

int f44() { return 44; }

คุณอาจจะคิดว่าfunctionนี้ไม่ได้นำอะไรเข้ามาเลยแต่เราพึ่งเห็นว่าfunctionที่ไม่ได้นำอะไรเข้ามาเลยไม่สามารถถูกเรียกได้เพราะว่ามันไม่มีค่าอะไรเลยที่จะเป็นตัวแทนของความไม่มีอะไร แล้วfunctionนี้นำอะไรเข้ามา? ในทางแนวคิด(conceptually)แล้วมันนำค่าที่ไม่มีความหมาย(dummy value)ที่มันมีแค่ค่าค่าเดียวมา เพื่อที่เราจะไม่ต้องกล่าวถึงมันอย่างชัดแจ้ง แต่ในHaskellได้มีเครื่องหมายสำหรับค่านี้นั่นก็คือวงเล็บที่ไม่มีอะไรอยู่ข้างใน () ดังนั้นโดยความบังเอิญที่ตลก (หรือมันคือบังเอิญจริงๆใช่ไหม?) ในการเรียกfunctionของvoidดูเหมือนกันทั้งของC++และHaskell แล้วก็เพราะว่าความชอบความเข้มงวดของHaskell เครื่องหมาย ()ก็ถูกใช้สำหรับtype (เป็นconstructor)และค่าเพียงค่าเดียวที่ตรงกับsetที่มีสมาชิกเพียงตัวเดียว และนี่คือfunctionนั้นในHaskell

f44 :: () -> Integer
f44 () = 44

ในบรรทัดแรกเป็นการประกาศว่า f44 นำtype()ที่เรียกว่า”unit”ไปสู่typeIntegerในบรรทัดสองนิยามf44ผ่านการการจับคู่รูปแบบ(Pattern matching)โดยที่ที่แค่constructorของunitที่นี้ก็คือ()และผลิตตัวเลข\(44\)ออกมา คุณสามารถที่จะเรียกfunctionนี้โดยการให้ค่าunit()กับมัน

f44 ()

เราจะเห็นว่าทุกๆfunctionของunitจะเป็นเหมือนกับการเลือกสมาชิกเดี่ยวจากtypeเป้าหมาย (ในที่นี้เป็นการเลือกInteger 44) ในความจริงแล้วคุณสามารถที่จะคิดว่าf44ในฐานะการแสดงในอีกรูปแบบหนึ่งของตัวเลข\(44\) นี่คือตัวอย่างของวิธีการที่เราสามารถที่จะพูดถึงfunction(ลูกศร)แทนที่จะเป็นการกล่าวถึงสมาชิกของsetอย่างโจ่งแจ้ง functionจากunitไปยังtypeอะไรก็ตามนั้นมีความตรงกันเป็นหนึ่งต่อหนึ่งกับสมาชิกของsetนั้น

แล้วถ้าเป็นfunctionที่คืนค่าเป็นtypeประเภทvoidหรือในHaskellที่มีtypeที่คืนเป็นunitจะเป็นอย่างไร? ในC++functionแบบนี้ถูกใช้สำหรับผลข้างเคียงแต่เรารู้ว่าfunctionเหล่านี้ไม่ได้เป็นfunctionจริงๆในทางความหมายของคำนี้ในทางคณิตศาสตร์ functionที่pureนั้นคืนค่าunitโดยที่ไม่ทำอะไรและทิ้งargumentของมัน

ในทางคณิตศาสตร์ functionจากset\(A\)ไปยังsetที่มีสมาชิกเพียงตัวเดียวจับคู่ทุกสมาชิกของ\(A\)ไปยังสมาชิกเดี่ยวของsetที่มีสมาชิกเพียงตัวเดียว สำหรับทุกๆ\(A\)แล้วมันจะมีfunctionแบบนี้เพียงอย่างเดียว นี่คือfunctionแบบนี้ในInteger

fInt :: Integer -> ()
fInt x = ()

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

fInt :: Integer -> ()
fInt _ = ()

สังเกตว่าการเขียนของfunctionนี้ไม่ได้แค่ไม่ได้ขึ้นอยู่กับค่าที่ถูกใส่มาเท่านั้นแต่ก็ไม่ได้ขึ้นอยู่กับtypeของargumentด้วย

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

unit :: a -> ()
unit _ = ()

ในC++คุณก็จะเขียนfunctionนี้ว่า

template<class T>
void unit(T) {}

ต่อไปในประเภทของtypeคือsetที่มีสมาชิกสองตัว ในC++มันถูกเรียกว่าboolและในHaskellก็เดาไม่ยากว่าคือBool ความแตกต่างคือว่าในC++boolเป็นtypeที่build-inในขณะที่Haskellมันสามารถที่จะถูกนิยามว่า

data Bool = True | False

(วิธีการอ่านนิยามนี้คือการที่ว่าBoolนั้นเป็นTrueหรือFalse)ในทางหลักการแล้วเราควรที่จะสามารถนิยามtype BooleanในC++ในฐานะenumerationว่า

enum bool {
    true,
    false
};

แต่enumของC++นั้นเป็นจำนวนเต็มอย่างลับๆ ในC++11 “enum class”ควรที่จะถูกใช้แทนที่แต่คุณต้องให้สมบัติต่อค่าต่างๆของมันคู่กับชื่อของclassอย่าง bool::trueและbool::false ไม่ต้องพูดถึงการที่จะต้องนำheaderที่ถูกต้องมาในทุกๆfileที่ใช้งานกับมัน

functionที่pureจากBoolก็แค่ต้องเลือกค่าทั้งสองค่าจากtypeเป้าหมาย ที่หนึ่งในนั้นคู่กับTrueและอีกตัวคู่กับFalse

functionไปยังBoolจะถูกเรียกว่าpredicate ตัวอย่างเข่นในlibaryData.CharของHaskelนั้นเต็มไปด้วยpredicateอย่างisAlphaหรือisDigit ในC++ก็มีlibaryที่คล้ายๆกันที่กำหนด ในชุดของfunctionต่างๆ อย่างisalphaและisdigit แต่functionเหล่านี้จะคืนค่าเป็นintแทนที่จะเป็นBoolean predicateจริงๆจะถูกนิยามใน std::ctype และมีรูปร่างแบบ ctype::is(alpha, c), ctype::is(digit, c) และอื่นๆ

3.7 โจทย์ท้าทาย

  1. ลองนิยามfunctionลำดับสูง(หรือก็คือobjectแบบfunction) memoize ในภาษาโปรดของคุณ functionนี้นำfunctionที่pure f เป็นargumentและคืนfunctionที่ทำการเหมือนfแต่แค่ว่ามันจะเรียกfunctionดั้งเดิมในหนึ่งครั้งต่อทุกๆargument เก็บผลลัพธ์เอาไว้ข้างในและหลังจากนั้นก็คืนผลลัพธ์ที่ถูกเก็บไว้ในทุกๆครั้งที่มันถูกเรียกโดยarguemntอันเดียวกัน คุณสามารถที่จะแยกแยะfunctionที่มีการจำจากตัวดั้งเดิมโดยการดูความเร็วในการคำนวน (performance) ตัวอย่างเช่นให้ลองการจำfunctionที่ใช้เวลานานในการที่จะหาค่า คุณจะต้องรอสำหรับค่าที่ออกมาในตอนแรกที่คุณเรียกมัน แต่ในการเรียกถัดๆไปโดยargumentที่เหมือนเดิมแล้วนั้นคุณควรที่จะได้ผลลัพธ์มาโดยทันที
  2. ลองที่จะจำfunctionจากlibraryมาตรฐานที่คุณใช้ในการสร้างหมายเลขสุ่ม มันจะสามารถทำได้หรือเปล่า
  3. สิ่งในการสร้างหมายเลขสุ่มส่วนมากสามารถที่จะinitializedโดยseed ลองเขียนfunctionที่นำseedเข้ามาและเรียกfunctionในการสร้างหมายเลขสุ่มด้วยseedและreturnผลลัพธ์ออกมาและทำการจำfunctionนี้ มันจะทำได้หรือเปล่า
  4. functionของC++อันไหนที่pure ลองทำการจำมันและสังเกตว่าอะไรจะเกิดขึ้นในตอนที่คุณเรียกมันในหลายๆครั้ง ทั้งที่จำไปแล้วและไยังไม่ได้จำ
    1. functionที่เป็นfactorialที่อยู่ในตัวอย่างข้างบน
    2. std::getchar()
    3.      bool f() {
         std::cout << "Hello!" << std::endl;
         return true;
     }
    4.      int f(int x) {
         static int y = 0;
         y += x;
         return y;
     }
  5. แล้วมีfunctionที่แตกต่างกันระหว่างBoolไปยังBoolอยู่กี่ตัวแล้ว คุณสามารถที่จะเขียนมันมาทั้งหมดหรือเปล่า
  6. ลองวาดภาพของcategoryที่objectคือtypeVoid, () (unit) และ Bool โดยที่ลูกศรจะคู่กับfunctionที่เป็นไปได้ทั้งหมดระหว่างtypeต่างๆ แล้วก็เขียนช่ือของแต่ละfunctionด้วย

  1. Original: “cannot be propagated to call sites”↩︎

  2. ในบทความของNils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbonsที่มีชื่อว่า Fast and Loose Reasoning is Morally Correct (การให้เหตุผลอย่างรวดเร็วและหละหลวมนั้นถูกต้องทางจริยธรรม) ได้เสนอเหตุผลสำหรับการไม่ต้องใส่ใจต่อbottomในบริบทส่วนมาก↩︎