จากเรื่องราวทั้งหมดในหนังสือเล่มนี้ เรื่องราวของ Harry Potter อาจเป็นเรื่องที่เป็นที่รู้จักมากที่สุด ปัจจัยหลายอย่างที่ทำให้เรื่องนี้ได้รับความนิยมนั้นคือการที่เนื้อเรื่องเกี่ยวกับเวทมนตร์ ซึ่งปฏิบัติตามกฎที่ต่างจากกฎของโลกทางกายภาพทั่วไป ดังนั้น เรื่องราวเหล่านี้จึงต้องกำหนดกฎว่าอะไรเป็นไปได้และอะไรเป็นไปไม่ได้ในโลกแห่งเวทมนตร์ และอธิบายว่ากฎเหล่านั้นทำงานร่วมกับกฎธรรมชาติอย่างไร แง่มุมนั้นสำคัญเป็นพิเศษสำหรับการผจญภัยของ Harry Potter เพราะเรื่องเหล่านี้—ไม่เหมือนนิทานพ่อมดหลายเรื่อง—เกิดขึ้นในอังกฤษยุคปัจจุบัน ไม่ใช่ในสถานที่หรือยุคที่ห่างไกล

ถ้าเวทมนตร์ในหนังสือ Harry Potter เป็นเรื่องที่เกิดขึ้นแบบสุ่มและไม่ได้ถูกควบคุมโดยกฎ เรื่องราวเหล่านั้นก็คงไร้ความหมายทันที เมื่อผู้อ่านไม่สามารถตั้งความคาดหวังที่สมเหตุสมผลได้ว่าจะเกิดอะไรขึ้นต่อไปหรือสาเหตุที่ไม่ทราบของเหตุการณ์หนึ่งๆ คืออะไร พวกเขาก็จะมีแรงจูงใจอ่านต่อได้น้อยลง กฎที่อธิบายกฎของธรรมชาติ กฎ "ของ" เวทมนตร์ และความสม่ำเสมออื่นๆ ในชีวิตของเรา จึงมีความสำคัญต่อการเข้าใจเหตุการณ์และสาเหตุของมัน และยังจำเป็นต่อการวางแผนล่วงหน้า กฎเหล่านี้โดยธรรมชาติมักเป็นกฎทั่วไปและอ้างถึงประเภทของสิ่ง ไม่ใช่บุคคล เพราะพลังของกฎอยู่ที่ความสามารถในการแทนกรณีปัจเจกจำนวนมาก ประเภทไม่เพียงแต่บอกคุณสมบัติของวัตถุ แต่ยังจัดหมวดหมู่การกระทำด้วย ตัวอย่างเช่น การเทเลพอร์ต การนั่งรถไฟ หรือการเดินของ Hansel และ Gretel ในป่า ต่างเป็นตัวอย่างของการเคลื่อนที่ กฎง่ายๆ เกี่ยวกับการเคลื่อนที่คือการเคลื่อนย้ายสิ่งของจะเปลี่ยนตำแหน่งของมัน และเพราะเป็นจริงสำหรับการเคลื่อนที่ทุกรูปแบบและวัตถุทุกชนิด กฎนี้จึงเกี่ยวกับประเภท ไม่ใช่ปัจเจกบุคคล

ในเชิงคอมพิวติ้ง กฎที่อธิบายความสม่ำเสมอของการคำนวณเรียกว่า typing rules (กฎการกำหนดชนิด) กฎเหล่านี้จำกัดอินพุตและเอาต์พุตที่ยอมรับได้ของ algorithms (อัลกอริทึม) และด้วยเหตุนี้จึงช่วยค้นหาข้อผิดพลาดเมื่อรันอัลกอริทึม ยิ่งไปกว่านั้น เพราะ types ทำงานในระดับที่ละเอียดกว่าระบบรวมถึงการดำเนินการและอาร์กิวเมนต์ในแต่ละขั้นของ algorithm กฎการกำหนดชนิดจึงสามารถใช้ตรวจหา type errors (ข้อผิดพลาดชนิด) ในอัลกอริทึมได้ งานนี้สำคัญถึงขนาดที่มีอัลกอริทึมชนิดหนึ่งทำหน้าที่นี้โดยเฉพาะ เรียกว่า type checkers (ตัวตรวจชนิด) หากอัลกอริทึมไม่ละเมิดกฎการกำหนดชนิดใดๆ ก็ถือว่าเป็น type correct (ถูกต้องตามชนิด) และการรันจะปลอดจากข้อผิดพลาดบางประเภท Types และ typing rules ช่วยให้แน่ใจว่าอัลกอริทึมทำงานตามที่ตั้งใจไว้ และยังเป็นแนวทางในการสร้างอัลกอริทึมที่เชื่อถือได้

The Types of Magic and the Magic of Types (ชนิดของเวทมนตร์และเวทมนตร์ของชนิด)

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

เพื่อช่วยทำความเข้าใจโลกเวทมนตร์ มันถูกจัดเป็นแนวความคิดที่เกี่ยวข้องหลายอย่าง ตัวอย่างเช่น คนที่สามารถใช้เวทมนตร์เรียกว่า wizard (หรือ witch) ในขณะที่คนธรรมดาที่ไม่สามารถใช้เวทมนตร์เรียกว่า muggle พ่อมดยังแยกเป็นอาชีพต่างๆ เช่น aurors, arithmancers, curse breakers, herbologists และอื่นๆ การกระทำทางเวทมนตร์เรียกว่า spells และแยกย่อยเป็น charms, curses, transfigurations และหมวดอื่นๆ ชื่อที่ตั้งให้หมวดต่างๆ ค่อนข้างเป็นการตกลงกันและสำคัญน้อยกว่าสิ่งที่สำคัญจริงๆ คือคุณสมบัติและพฤติกรรมที่วัตถุในหมวดเดียวกันมีร่วมกัน และความสัมพันธ์ระหว่างหมวดเหล่านั้นก็สำคัญไม่แพ้กัน ตัวอย่างเช่น spells สามารถร่ายได้โดย wizards เท่านั้น แต่ผลของเวทมนตร์อาจมีผลกับทั้ง wizards และ muggles ได้ เช่นกัน เวทมนตร์ใน Harry Potter อาจซับซ้อนมาก เพื่อร่ายคาถาอย่างมีประสิทธิภาพ พ่อมดมักต้องใช้ wand และต้องสวดคาถา อย่างไรก็ตาม พ่อมดที่มีประสบการณ์ก็สามารถร่ายคาถาที่ไม่ต้องใช้คำพูดหรือไม้กายสิทธิ์ได้ ผลของคาถามักมีระยะเวลาจำกัด และบางครั้งสามารถป้องกันได้ด้วย counterspell เวทมนตร์ยังสามารถถูกเก็บไว้ใน potion ทำให้แม้แต่ muggles ก็สามารถทำเวทย์ได้ถ้าพวกเขามี access to potions การที่เวทมนตร์ไม่ใช่เรื่องง่ายแสดงให้เห็นจากการที่พ่อมดและแม่มดหนุ่มต้องไปเรียนโรงเรียนเวทมนตร์เป็นเวลาเจ็ดปีเพื่อเชี่ยวชาญเรื่องนี้

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

ในวิทยาการคอมพิวเตอร์ หมวดของวัตถุที่มีพฤติกรรมแบบหนึ่งเรียกว่า type (ประเภท) เราได้เจอเรื่องของ types ในหลายมุมแล้ว ในchapter 4 เราเห็น data types ต่างๆ (set, stack, และ queue) สำหรับเก็บและจัดการคอลเลกชันของวัตถุ แต่ละ data type มีวิธีเฉพาะในการใส่ ดึง และลบองค์ประกอบจากคอลเลกชัน เช่น stack ดึงวัตถุตามลำดับย้อนกลับจากที่ถูกใส่ (last in, first out) และ queue ดึงตามลำดับที่ถูกป้อน (first in, first out) ดังนั้น data type หนึ่งจึงห่อหุ้มพฤติกรรมเฉพาะสำหรับการจัดการคอลเลกชันขององค์ประกอบ พฤติกรรมของ data type ทำให้มันเหมาะกับงานคำนวณชนิดเฉพาะ เช่น ในchapter 13 ฉันใช้ data type stack เพื่ออธิบายการทำงานของ interpreter และการติดตามอาร์กิวเมนต์ต่างๆ เมื่อเรียกใช้อัลกอริทึมแบบ recursive

อีกการใช้หนึ่งของ types คือการอธิบายอินพุตและเอาต์พุตที่จำเป็นหรือคาดหวังสำหรับอัลกอริทึม ตัวอย่างเช่น type ของอัลกอริทึมที่บวกตัวเลขสองจำนวนสามารถเขียนได้ดังนี้:

(Number, Number) → Number

ประเภทของอาร์กิวเมนต์ของอัลกอริทึมจะแสดงทางซ้ายของลูกศร ส่วนประเภทของผลลัพธ์จะแสดงทางขวา ดังนั้น type นี้บอกว่าอัลกอริทึมรับคู่ของตัวเลขและให้ผลลัพธ์เป็นตัวเลข สังเกตว่า type ของอัลกอริทึมที่ลบ คูณ หรือการดำเนินการทวินามอื่นๆ จะเหมือนกับของการบวก นี่แสดงให้เห็นว่า type ไม่ผูกกับอัลกอริทึมเฉพาะหรือการคำนวณหนึ่งๆ ซึ่งสอดคล้องกับแนวคิดที่ว่า types เป็นคำอธิบายของคลาสของสิ่ง ในกรณีนี้ type อธิบายกลุ่มการคำนวณที่กว้าง

ตัวอย่างอีกอันคืออัลกอริทึมการตื่นนอนในchapter 2 ที่มีพารามิเตอร์ wake-up-time เพื่อบอกว่าอัลกอริทึมควรส่งเสียงปลุกเมื่อไร พารามิเตอร์นี้ต้องการค่าเวลาเป็นอินพุต นั่นคือคู่ของตัวเลขที่ระบุชั่วโมงและนาทีของเวลาปลุก นอกจากนี้ ตัวเลขทั้งสองไม่สามารถเป็นค่าใดก็ได้: ค่าชั่วโมงต้องเป็นตัวเลขระหว่าง 0 ถึง 23, และค่านาทีต้องเป็นตัวเลขระหว่าง 0 ถึง 59 ตัวเลขนอกช่วงเหล่านี้ไม่มีความหมายและจะทำให้อัลกอริทึมทำงานผิดพลาดได้ ดังนั้นเราจึงสามารถอธิบาย type ของอัลกอริทึมการตื่นนอนได้ดังนี้:

(Hour, Minute) → Alarm

ที่นี่ Hour และ Minute เป็น types สำหรับส่วนย่อยของตัวเลขตามที่อธิบายไว้ และ Alarm เป็น type สำหรับพฤติกรรมการปลุก พฤติกรรมการปลุกคือการส่งเสียงแบบเฉพาะเวลา และเช่นเดียวกับที่ type Minute มีตัวเลข 0 ถึง 59 type Alarm จะมีพฤติกรรมปลุกที่เป็นไปได้ 24 × 60 = 1,440 แบบ หนึ่งแบบสำหรับแต่ละนาทีของวัน หากเสียงปลุกสามารถตั้งค่าได้ อัลกอริทึมก็ต้องมีพารามิเตอร์อีกตัว ซึ่งต้องสะท้อนใน type ด้วย และผลลัพธ์ประเภท Alarm ก็ต้องกว้างขึ้นเพื่อรองรับเสียงที่ต่างกัน

เราจะเห็นว่า type ของอัลกอริทึมบอกอะไรบางอย่างเกี่ยวกับอัลกอริทึม มันไม่บอกอย่างละเอียดว่าอัลกอริทึมทำอะไร แต่จะจำกัดฟังก์ชันการทำงานของมัน ซึ่งมักเพียงพอสำหรับการเลือกใช้อัลกอริทึม เราคงไม่เอาอัลกอริทึมที่ใช้บวกมาใช้กับปัญหาการส่งเสียงปลุกตามเวลา โดยไม่ต้องดูรายละเอียดของอัลกอริทึมการบวกและการตื่นนอน เพียงจาก type ที่ต่างกันเราก็รู้ได้แล้ว Type ของอัลกอริทึมมีลูกศรเพื่อแยกชนิดของอาร์กิวเมนต์ (ซ้าย) ออกจากชนิดของผลลัพธ์ (ขวา) มันบอกว่าการคำนวณที่สอดคล้องกันแปลงอินพุตชนิดหนึ่งเป็นผลลัพธ์อีกชนิดหนึ่ง ผลลัพธ์อาจเป็นค่า เช่น กรณีการบวก หรือเป็นผล (effect) เช่น กรณีอัลกอริทึมการตื่นนอน

เนื่องจากคาถาก็เป็นการแปลงเช่นกัน เราจึงสามารถใช้ types มาบรรยายผลของมันได้ ตัวอย่างเช่น ในหนังสือ Harry Potter วัตถุสามารถถูกยกขึ้นด้วยคาถา Wingardium Leviosa ซึ่งพ่อมดต้องขยับไม้กายสิทธิ์ ชี้ไปยังวัตถุ และท่องคาถา "Wingardium Leviosa" สมมติว่า types Object และ Levitating แทนวัตถุปกติและวัตถุที่ลอยได้ตามลำดับ type ของคาถานี้สามารถอธิบายได้ดังนี้:

(Wand, Incantation, Object) → Levitating

Types เป็นสัญกรณ์ที่มีประโยชน์สำหรับการพูดคุยและให้เหตุผลเกี่ยวกับคุณสมบัติของ algorithms และการคำนวณ ลูกศรที่แยกอาร์กิวเมนต์ออกจากผลลัพธ์เป็นส่วนสำคัญ ส่วนการใช้ type parameters เป็นอีกส่วนหนึ่ง ตัวอย่างเช่น พิจารณา sorting algorithms ที่กล่าวถึงในchapter 6 อัลกอริทึมการเรียงต้องการรายการขององค์ประกอบเป็นอินพุต และให้รายการขององค์ประกอบเดียวกันเป็นผลลัพธ์ นอกจากนี้ องค์ประกอบนั้นต้องเปรียบเทียบกันได้ กล่าวคือ เราต้องสามารถกำหนดได้ว่าสององค์ประกอบเท่ากันหรือองค์ประกอบหนึ่งใหญ่กว่าอีกองค์ประกอบหนึ่ง เพราะตัวเลขเปรียบเทียบได้ ดังนั้น type ต่อไปนี้จึงเป็น type ที่ถูกต้องสำหรับ sorting algorithm ที่จัดเรียงรายการของตัวเลข:

List(Number) → List(Number)

การเขียน type สำหรับรายการของตัวเลขเป็น List(Number) แสดงว่าประเภทของรายการต่างๆ สามารถได้จากการแทนที่ Number ด้วยชนิดอื่นได้ ตัวอย่างเช่น เราสามารถเรียงข้อมูลตัวอักษรได้ ดังนั้น sorting algorithm ก็จะมี type เป็น List(Text) → List(Text) เพื่อแสดงว่า sorting algorithms อาจมีหลาย type ที่เกี่ยวข้อง เราสามารถแทนที่ item type เฉพาะ เช่น Number หรือ Text ด้วย type parameter ที่สามารถถูกแทนที่ด้วย type เฉพาะได้ ดังนั้นเราสามารถแสดง type ของ sorting algorithms ด้วยเทมเพลตต่อไปนี้ โดยที่ comparable แทนชนิดใดๆ ที่องค์ประกอบสามารถเปรียบเทียบได้:

List(comparable) → List(comparable)

Type เฉพาะใดๆ เช่น List(Number) → List(Number) สามารถได้จากเทมเพลตชนิดนี้โดยการแทนที่ item type ให้กับพารามิเตอร์ชนิด comparable.

การแนบชนิดให้กับชื่อของอัลกอริทึมด้วยโคลอน เป็นการยืนยันว่าอัลกอริทึมนั้นมีชนิดดังกล่าว ตัวอย่างเช่น เพื่อยืนยันว่า sorting algorithm Qsort มีชนิดนี้ เราจะเขียนดังนี้:

Qsort : List(comparable) → List(comparable)

อัลกอริทึม Count ในchapter 12 ก็รับรายการขององค์ประกอบเป็นอินพุตเช่นกัน แต่ไม่ต้องการให้องค์ประกอบเปรียบเทียบได้ และคืนค่าเป็นตัวเลข ดังนั้น type ของ Count สามารถอธิบายได้ดังนี้ โดยที่ any เป็นพารามิเตอร์ชนิดที่แทนชนิดใดๆ:

Count : List(any) → Number

การรู้ชนิดของสิ่งใดสิ่งหนึ่งบอกเราว่ามันทำอะไรได้และอะไรที่สามารถทำกับมันได้ การรู้ชนิดของอัลกอริทึมช่วยให้เราเลือกและประยุกต์ใช้อัลกอริทึมได้อย่างถูกต้อง ข้อมูลชนิดสามารถช่วยในหลายๆ ทาง

อันดับแรก หากเราต้องการรันอัลกอริทึมใดๆ type ของอินพุตจะบอกชนิดของอาร์กิวเมนต์ที่ต้องส่งให้ เช่น คาถาต้องการ incantation และ wand ในขณะที่ potion ต้องถูกดื่ม ไม่มีความหมายที่จะดื่มคาถาหรือใช้ incantation กับ potion ในทำนองเดียวกัน sorting algorithm อย่าง Qsort สามารถใช้งานกับรายการได้ แต่ไม่สามารถใช้งานกับค่าเวลาได้ หากไม่มีอาร์กิวเมนต์ที่มีชนิดที่ต้องการ อัลกอริทึมก็รันไม่ได้

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

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

ลักษณะที่แพร่หลายในและการใช้ types มาจากพลังของมันในการจัดระเบียบความรู้ Types ช่วยให้เราสามารถละเลยกรณีตัวอย่างเดี่ยวๆ และให้เหตุผลเกี่ยวกับสถานการณ์ในระดับทั่วไป ตัวอย่างเช่น เมื่อรู้ว่าเฉพาะ witch หรือ wizard เท่านั้นที่ขี่ไม้กวาดได้ เราสามารถอนุมานได้ว่า Harry Potter อาจขี่ไม้กวาดได้ แต่ป้าของเขา Petunia ซึ่งเป็น muggle จะทำไม่ได้ หรือเมื่อ Harry ใช้ผ้าคลุมล่องหน เขาพึ่งคุณสมบัติว่าทุกสิ่งที่คลุมด้วยมันจะมองไม่เห็น ตัวอย่างมากมายพบได้ในชีวิตประจำวันที่ไม่เกี่ยวกับเวทมนตร์ เช่น เมื่อเราเลือกเครื่องมือเฉพาะเพราะคุณสมบัติโดยทั่วไป (ไขควง ร่ม นาฬิกา เครื่องปั่น) หรือเมื่อเราคาดการณ์ผลของปฏิสัมพันธ์เฉพาะ (คิดถึงการชนกันของวัตถุ การเสียบอุปกรณ์ไฟฟ้า หรือพฤติกรรมของคนในบทบาทต่างๆ เช่น ลูกค้า ผู้ป่วย พ่อแม่ ฯลฯ)

Rules Rule (กฎคือกฎ)

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

กฎการกำหนดชนิดอธิบายชนิดของวัตถุภายใต้เงื่อนไขบางประการ เงื่อนไขที่ต้องเป็นจริงเพื่อให้กฎใช้ได้เรียกว่า premises และข้อความเกี่ยวกับชนิดของวัตถุที่กฎอนุมานจาก premises เรียกว่า conclusion กฎเกี่ยวกับการแตกของสิ่งเปราะมีสาม premises ได้แก่ วัตถุเป็นสิ่งเปราะ ถูกทิ้ง และพื้นที่มันตกลงมานั้นเป็นพื้นแข็ง ข้อสรุปของกฎคือวัตถุนั้นแตก กฎการกำหนดชนิดที่มีเพียงข้อสรุปแต่ไม่มี premises เรียกว่า axiom เพื่อบอกว่ามันเป็นจริงโดยไม่มีเงื่อนไข ตัวอย่างเช่น “Harry Potter is a wizard,” “3 is a number,” หรือ “thin glass is fragile.”

การระบุชนิดและการกำหนดชนิดให้กับวัตถุเป็นเรื่องของการออกแบบและถูกชี้นำโดยสถานการณ์และวัตถุประสงค์เฉพาะ ตัวอย่างเช่น ความแตกต่างระหว่าง muggles และ wizards สำคัญในบริบทของเรื่อง Harry Potter แต่ไม่เป็นประโยชน์ในบริบทที่เวทมนตร์ไม่มีอยู่จริง กฎส่วนใหญ่เกี่ยวกับวัตถุในชีวิตประจำวันพัฒนาขึ้นเพื่อช่วยให้เรารอดชีวิตในโลกธรรมชาติ พวกมันช่วยให้เราเลี่ยงความผิดพลาดที่อาจถึงตาย ด้วยเทคโนโลยีและวัฒนธรรมใหม่ๆ ก็ต้องมีกฎใหม่ๆ เพื่อให้อยู่รอดได้ในด้านต่างๆ ของชีวิตสมัยใหม่ เช่น วิธีใช้ลิฟต์หรือโทรศัพท์มือถือ หรือวิธีสมัครและใช้ประกันสุขภาพ ตัวอย่างเหล่านี้แสดงว่าการออกแบบ types และ typing rules เป็นกระบวนการที่ต่อเนื่องโดยมีเป้าหมายเฉพาะเป็นตัวขับเคลื่อน

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

Premise แรกของกฎต้องการให้อัลกอริทึมมีชนิดอินพุตและเอาต์พุต ความต้องการนี้สอดคล้องกับ Gamp’s Law of Elemental Transfiguration ที่ปรากฏใน Harry Potter and the Deathly Hallows ซึ่งบอกว่าอาหารไม่สามารถถูกสร้างขึ้นจากอากาศ มันสามารถถูกเรียกมาจากที่อื่นหรือขยายขนาดกว้างขึ้นเท่านั้น กฎการนำไปใช้สะท้อนคุณสมบัติพื้นฐานของอัลกอริทึม นั่นคือมันขึ้นกับอินพุตเพื่อผลิตเอาต์พุตที่เปลี่ยนแปลงได้

เพียงแต่เมื่อ premises ทั้งหมดของกฎเป็นจริง ข้อสรุปของกฎจึงจะถูกดึงออกมาได้ เช่น ไข่ที่ตกลงบนทางเข้าโรงจอดรถจะสอดคล้องกับกฎเกี่ยวกับการแตกของสิ่งเปราะ ดังนั้นข้อสรุปว่าไข่จะแตกจึงเป็นไปได้ นอกจากนี้ เนื่องจาก 6 เป็นชั่วโมงที่ถูกต้องและ 30 เป็นนาทีที่ถูกต้อง และเนื่องจากชนิดของอาร์กิวเมนต์ของอัลกอริทึมการตื่นนอนคือ (Hour, Minute) เราจึงสามารถนำอัลกอริทึมนี้ไปใช้กับสองอาร์กิวเมนต์และสรุปได้ว่าผลลัพธ์เป็นพฤติกรรมที่ถูกต้องตามชนิด Alarm การประยุกต์ของกฎการกำหนดชนิดจะได้มาจากการแทนที่อัลกอริทึมเฉพาะด้วย Alg และอาร์กิวเมนต์ด้วย Arg พร้อมกับประเภทที่สอดคล้องกันสำหรับ Input และ Output การประยุกต์ของกฎนี้กับอัลกอริทึมการตื่นนอนมีลักษณะดังนี้:

ในทำนองเดียวกัน หาก L เป็นรายการของตัวเลข เราสามารถใช้กฎกับชนิด List(Number) → List(Number) สำหรับ Qsort เพื่อสรุปว่าการนำ Qsort ไปใช้กับ L จะให้รายการของตัวเลข

ความสามารถในการคาดการณ์ผลจากชนิดของวัตถุที่เกี่ยวข้องอย่างเดียวเป็นกลไกการให้เหตุผลที่ทรงพลังที่ทำให้คนมีเหตุผลใช้ช้อนกินซุปหรือถอดเสื้อก่อนอาบน้ำ Types และ typing rules ให้การแทนวัตถุและเหตุการณ์ที่คล้ายกันอย่างกะทัดรัดซึ่งทำให้กระบวนการนี้มีประสิทธิภาพ และนี่ไม่ได้ใช้ได้แค่การให้เหตุผลเกี่ยวกับสถานการณ์ในชีวิตประจำวันเท่านั้น แต่ยังใช้ได้ในโดเมนอย่างโลกเวทมนตร์ของ Harry Potter หรือโลกของการคำนวณ

ในโลกของ Harry Potter พลังของเวทมนตร์ละเมิดกฎธรรมชาติจำนวนมาก ดังนั้นพ่อมดบางครั้งจึงให้เหตุผลต่างออกไปเกี่ยวกับวัตถุประจำวันและทำตามนั้น ตัวอย่างเช่น พ่อมดสามารถหลีกเลี่ยงงานน่าเบื่อที่ muggles ต้องทำ เช่น แม่ของ Ron Weasley ใช้เวทมนตร์ช่วยการทำอาหารและกวาดบ้าน สำหรับพ่อมดมันไม่สมเหตุสมผลที่จะทำด้วยมืออีกตัวอย่างคือการขับรถในรถปกติ ซึ่งถูกดูถูกในชุมชนเวทมนตร์เพราะไม่ประหยัดเมื่อเทียบกับการเดินทางแบบเวทมนตร์ เช่น teleportation, floo powder, portkeys และแน่นอนการบิน

ชนิดของอัลกอริทึมทำนายผลของการคำนวณและถูกใช้ให้เหตุผลเกี่ยวกับการคำนวณเช่นกัน สมมติว่าคุณได้รับมอบหมายให้เรียงรายการแต่คุณไม่รู้วิธีการ คุณได้รับสามซองผนึก A, B, และ C แต่ละซองมีอัลกอริทึมคนละแบบ คุณไม่รู้ว่าอัลกอริทึมไหนอยู่ในซองไหน แต่รู้ว่าหนึ่งในนั้นมี sorting algorithm เป็นตัวเลือกหนึ่ง ในการช่วยบอกชนิดของแต่ละอัลกอริทึม จะมีการเขียนชนิดของอัลกอริทึมภายนอกซอง ซองต่างๆ แสดงชนิดดังนี้:

Envelope A: (Hour, Minute) → Alarm

Envelope B: List(any) → Number

Envelope C: List(comparable) → List(comparable)

ซองไหนคุณควรเลือก?

When Rules Do Not Apply (เมื่อกฎไม่ใช้)

Types และ typing rules ให้กรอบสำหรับการให้เหตุผลที่มีประสิทธิภาพเมื่อใช้ได้ แต่บ่อยครั้งมีสถานการณ์ที่กฎไม่สามารถใช้ได้ เมื่อหนึ่งหรือหลาย premises ไม่เป็นจริง กฎก็ใช้ไม่ได้ ซึ่งหมายความว่าข้อสรุปของมันไม่ถูกต้อง ตัวอย่างเช่น ค้อนที่ตกบนทางเข้าโรงจอดรถไม่ได้สอดคล้องกับ premise เกี่ยวกับวัตถุที่เปราะ และสถานการณ์ที่ไข่ตกลงในกล่องเลื่อยก็ไม่สอดคล้องกับ premise เกี่ยวกับพื้นแข็ง ดังนั้นในทั้งสองกรณี ข้อสรุปเกี่ยวกับการแตกของวัตถุจึงไม่สามารถสรุปได้ ในทำนองเดียวกัน เมื่อ Ron Weasley พยายามร่ายคาถา Wingardium Leviosa เพื่อยกขนนก ขนนกไม่ได้ขยับเพราะเขาท่องคาถาผิด:

"Wingardium Leviosa!" he [Ron] shouted, waving his long arms like a windmill. "You're saying it wrong," Harry heard Hermione snap. "It's Wing-gardium Levi-o-sa, make the ‘gar’ nice and long."

เนื่องจากหนึ่งใน premises ของคาถายกวัตถุไม่ได้เป็นจริง กฎจึงใช้ไม่ได้ และข้อสรุปว่าขนนกจะลอยขึ้นจึงไม่เกิดขึ้น

การเผชิญสถานการณ์ที่กฎการกำหนดชนิดไม่สามารถใช้ได้ไม่ได้หมายความว่ากฎนั้นผิด มันแค่หมายความว่าขอบเขตของมันจำกัดและไม่สามารถใช้ทำนายพฤติกรรมในสถานการณ์ปัจจุบันได้ ยิ่งไปกว่านั้น เมื่อกฎไม่สามารถใช้ได้ไม่ได้หมายความว่าข้อสรุปของกฎนั้นผิดโดยสิ้นเชิง มันอาจยังเป็นจริงได้เพราะปัจจัยอื่นๆ ที่กฎไม่ได้ครอบคลุม ตัวอย่างเช่น กฎว่า "ถ้าฝนตก ทางเข้าโรงจอดรถจะเปียก" จะไม่สามารถใช้ได้เมื่อท้องฟ้าแจ่มใส อย่างไรก็ตาม ทางเข้าอาจเปียกได้ถ้าหมุนฉีดพ่นทำงาน หรือในตัวอย่างจาก Harry Potter แม้ว่า Ron จะร่าย Wingardium Leviosa ไม่ถูกต้อง ขนนกก็ยังอาจลอยขึ้นได้เพราะมีคนอื่นร่ายคาถาพร้อมกัน หรือค้อนที่ตกอาจแตกเพราะด้ามมันเคยแตกร้าวก่อนหน้านั้น ดังนั้นเมื่อกฎไม่สามารถใช้ได้ ก็ไม่อาจสรุปได้ทั้งสองทาง

ดังนั้น อาจดูไม่สำคัญนักเมื่อกฎการกำหนดชนิดไม่สามารถใช้ได้ แต่นั่นขึ้นกับความสำคัญที่เราต้องการให้ผลลัพธ์นั้นเป็นจริง ในขณะที่การลอยของขนนกหรือการแตกของวัตถุตกลงเป็นเรื่องเพียงความอยากรู้ แต่มีหลายสถานการณ์ที่ผลการอนุมานมีความสำคัญ ลองคิดถึงมุกตลกแบบ "คำพูดสุดท้ายที่มีชื่อเสียง" ที่เล่นกับการอนุมานผิด เช่น "สายไฟสีแดงตัดได้ปลอดภัย" หรือ "น้องหมาน่ารัก" หรือ "นี่คือเห็ดที่ดี" สำหรับการคำนวณ การได้ชนิดที่ถูกต้องก็สำคัญเช่นกัน แม้จะไม่ร้ายแรงในหลายกรณี แต่การนำค่าที่มีชนิดผิดไปใช้งานมักทำให้การคำนวณล้มเหลว นี่คือเหตุผล ทุกขั้นตอนของอัลกอริทึมแปลงค่าหนึ่งหรือหลายค่า และแต่ละการดำเนินการที่นำมาใช้ในกระบวนการนี้ขึ้นกับอาร์กิวเมนต์ว่ามีชนิดที่กำหนดไว้หรือไม่ เพราะนิยามการทำงานของมันจะมีความหมายเฉพาะกับค่าเหล่านั้น จำไว้ว่าเราไม่สามารถเรียงเวลาในการปลุก และเราไม่สามารถคำนวณรากที่สองของรายการ หากขั้นตอนใดของอัลกอริทึมเจอค่าที่มีชนิดที่ไม่คาดหมาย มันจะไม่รู้ว่าต้องทำอะไรและติดค้าง ผลคือ การคำนวณไม่สามารถเสร็จสมบูรณ์และไม่สามารถให้ผลลัพธ์ที่มีความหมายได้ สรุปคือ ความสำเร็จของการคำนวณขึ้นกับการส่งให้การดำเนินการเฉพาะค่าโดยมีชนิดที่ถูกต้อง

ดังนั้น กฎการกำหนดชนิดเป็นส่วนสำคัญของการคำนวณเพราะมันช่วยให้มั่นใจว่าการดำเนินการจะไม่ติดกับค่าที่ผิดและการคำนวณทั้งหมดสามารถเสร็จสมบูรณ์ได้ เช่นเดียวกับกฎการกำหนดชนิดที่สามารถตรวจจับประโยคที่ไม่มีความหมาย เช่น "Harry Potter drank a spell," มันยังสามารถจุดการประยุกต์อัลกอริทึมที่ไม่สมเหตุผล เช่น Qsort(6:30am) และเนื่องจากอัลกอริทึมประกอบด้วยหลายขั้นตอนที่เกี่ยวข้องกับการนำการดำเนินการและอัลกอริทึมอื่นๆ ไปใช้กับค่า กฎการกำหนดชนิดจึงช่วยระบุข้อผิดพลาดภายในนิยามของอัลกอริทึม และสามารถสนับสนุนการสร้างอัลกอริทึมที่ถูกต้องตามชนิดได้อย่างแข็งขัน กระบวนการนี้บางครั้งเรียกว่า type-directed programming.

กฎการกำหนดชนิดไม่เพียงป้องกันการประยุกต์ใช้งานที่เป็นไปไม่ได้กับค่าที่ทำให้ติดค้าง แต่ยังป้องกันการประยุกต์ใช้งานที่ไม่มีความหมายในบริบทหนึ่งๆ อีกด้วย ตัวอย่างเช่น ความสูงและอายุของคุณอาจแสดงเป็นตัวเลขทั้งคู่ แต่การนำสองตัวเลขนี้มาบวกกันไม่มีความหมาย ผลรวมไม่มีความหมายเพราะตัวเลขสองตัวเป็นการแทนสองสิ่งที่ต่างกัน (ดูchapter 3) ดังนั้นผลรวมของสองตัวเลขจึงไม่เป็นตัวแทนของสิ่งใดและไม่มีความหมาย เราพบตัวอย่างใน Harry Potter ด้วย เช่น ในเกม Quidditch สองทีมพยายามทำคะแนนโดยโยนลูกบอล quaffle เข้าเสา แต่ถ้าใช้คาถา teleportation เกมคงง่ายเกินไปและทำให้เป้าหมายของเกมซึ่งคือการหาทีมที่เก่งกว่าหมดความหมาย ดังนั้นการใช้เวทมนตร์นอกเหนือจากการบินด้วยไม้กวาดจึงไม่ได้รับอนุญาตสำหรับผู้เล่น การจำกัดประเภทเช่นการต้องตามชุดการ์ดหรือการเดินของพระในหมากรุกเป็นการจำกัดในบริบทที่สนับสนุนเป้าหมายของเกม ไม่ใช่การบ่งชี้ถึงความเป็นไปไม่ได้ของการกระทำดังกล่าว Types สามารถใช้ติดตามตัวแทนเหล่านี้ควบคู่ไปกับการคำนวณเพื่อให้แน่ใจว่าการดำเนินการเคารพกฎการรวมกันของค่าที่แทน

การละเมิดกฎการกำหนดชนิดในอัลกอริทึมเรียกว่า type error มันบ่งชี้ถึงความไม่สอดคล้องในการรวมกันของการดำเนินการและค่า อัลกอริทึมที่ไม่มี type errors ถูกเรียกว่า type correct ข้อผิดพลาดชนิดหนึ่งในอัลกอริทึมอาจมีผลหลายแบบ ประการแรก มันอาจทำให้การคำนวณติดค้าง ซึ่งอาจนำไปสู่การยุติการคำนวณและรายงานข้อผิดพลาด การพยายามหารค่าด้วยศูนย์มักมีผลเช่นนี้ ใน Harry Potter and the Chamber of Secrets ไม้กายสิทธิ์ของ Ron แตกและทำให้คาถาทั้งหมดของเขาทำงานผิดพลาด ตัวอย่างเช่น คาถา Eat Slugs ที่เขาร่ายใส่ Malfoy กลับกลายเป็นว่ากลายเป็นหน้าคล้ายถ้วย และความพยายามแปลงหนูเป็นถ้วยของเขาก็ให้ผลเป็นถ้วยมีขนและมีหาง ผลลัพธ์ที่แน่นอนอาจเป็นเรื่องน่าประหลาดใจ แต่ความล้มเหลวของเวทมนตร์ของเขาเป็นเรื่องที่คาดได้ เพราะไม้กายสิทธิ์ที่แตกของเขาละเมิดหนึ่งใน premises ของกฎการใช้เวท ในกรณีเหล่านี้ ผลของเวทมนตร์ที่ไม่ทำงานมักจะมองเห็นได้ทันที ประการที่สอง type error อาจไม่ก่อให้เกิดผลที่สังเกตได้ทันที นั่นหมายความว่าการคำนวณยังคงดำเนินต่อและจบลง แต่มันให้ค่าที่ไม่มีความหมายและสุดท้ายให้ผลลัพธ์ที่ไม่ถูกต้อง การบวกอายุและความสูงเป็นตัวอย่างเช่น

ในขณะที่การหยุดการคำนวณทันทีโดยไม่มีผลลัพธ์ดูเหมือนแย่ แต่การคำนวณที่ยังดำเนินต่อแต่ให้ผลลัพธ์ที่ไม่มีความหมายอาจแย่ยิ่งกว่า ปัญหาในกรณีนั้นคือเราอาจไม่รู้ว่าผลลัพธ์นั้นผิดและอาจตัดสินใจสำคัญจากผลที่ผิด ตัวอย่างเช่น Harry พูดคำว่า “Diagon Alley” ผิดเป็น “Diagonally” เมื่อพยายามเดินทางด้วย floo powder ซึ่งทำให้เขามาจบที่ Knockturn Alley แทน การเดินทางไม่ได้ถูกยุติ และ floo powder ยังคงทำงาน แต่ให้ผลลัพธ์ที่ผิด จะดีกว่าเมื่อการเดินทางถูกยกเลิกตั้งแต่ต้น เพราะเขาเกือบถูกลักพาตัวและพบกับวัตถุอันตรายในร้านที่เขามาจบลง

Law Enforcement (การบังคับใช้กฎ)

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

ชนิดในอัลกอริทึมสามารถถูกตรวจสอบได้สองวิธี หนึ่งวิธีคือการตรวจชนิดขณะรันอัลกอริทึม วิธีนี้เรียกว่า dynamic type checking เพราะมันเกิดขึ้นขณะที่พฤติกรรมแบบไดนามิกของอัลกอริทึมมีผล ก่อนที่การดำเนินการจะถูกนำไปใช้ จะมีการตรวจสอบว่าชนิดของอาร์กิวเมนต์ตรงกับข้อกำหนดของการดำเนินการนั้นหรือไม่ ปัญหาของวิธีนี้คือมันไม่ช่วยอะไรเมื่อเกิด type error ในหลายกรณี ทางเลือกเดียวคือการยุติการคำนวณ ซึ่งอาจน่าหงุดหงิด โดยเฉพาะอย่างยิ่งในกรณีที่ส่วนใหญ่ของการคำนวณที่ตั้งใจไว้ได้เกิดขึ้นแล้วและอัลกอริทึมถูกยุติใกล้กับผลสุดท้าย จะดีกว่าถ้ารู้ล่วงหน้าว่าการคำนวณจะเสร็จสมบูรณ์โดยไม่เจอ type error และจะไม่เสียทรัพยากรไปกับการคำนวณที่พัง

วิธีทางเลือกคือการตรวจสอบอัลกอริทึมโดยไม่รันมันและตรวจว่าขั้นตอนทั้งหมดสอดคล้องกับกฎการกำหนดชนิด จากนั้นจะรันอัลกอริทึมก็ต่อเมื่อไม่มี type errors ในกรณีนี้ เราสามารถมั่นใจได้ว่าอัลกอริทึมจะไม่ยุติก่อนเวลาอันเนื่องมาจาก type error วิธีนี้เรียกว่า static type checking เพราะมันเกิดขึ้นโดยไม่คำนึงถึงพฤติกรรมการรันของอัลกอริทึม และต้องการเพียงคำอธิบายแบบคงที่ของอัลกอริทึม Static type checking คงบอก Ron ไม่ให้ลองใช้เวทมนตร์ด้วยไม้กายสิทธิ์ที่แตก

ข้อได้เปรียบเพิ่มเติมของ static type checking คืออัลกอริทึมต้องถูกตรวจเพียงครั้งเดียว หลังจากนั้นสามารถรันซ้ำได้หลายครั้งด้วยอาร์กิวเมนต์ต่างกันโดยไม่ต้องตรวจอีก นอกจากนี้ ขณะที่ dynamic type checking ต้องตรวจการดำเนินการในลูปซ้ำๆ จริงๆ static type checking ต้องตรวจการดำเนินการใดๆ เพียงครั้งเดียว ซึ่งนำไปสู่การรันที่เร็วกว่าของอัลกอริทึม ในทางกลับกัน dynamic type checking ต้องทำทุกครั้งที่อัลกอริทึมถูกรัน

อย่างไรก็ตาม dynamic type checking มีข้อได้เปรียบตรงที่โดยทั่วไปมันมีความแม่นยำมากกว่า เพราะมันพิจารณาค่าที่แท้จริงที่ถูกประมวลผล โดยที่ static type checking รู้เพียงชนิดของพารามิเตอร์ แต่ dynamic type checking รู้ค่าจริง Static type checking คงป้องกันไม่ให้ Ron ใช้ไม้กายสิทธิ์ที่แตกได้ทั้งหมด และด้วยเหตุนี้จะป้องกันความล้มเหลวทั้งหมด ในขณะที่ dynamic type checking ให้โอกาสให้เขาลองคาถาและอาจสำเร็จหรือล้มเหลวในสถานการณ์ต่างๆ ตัวอย่างเช่น เมื่อ Ron พยายามแปลงหนูเป็นถ้วย เขาประสบความสำเร็จเพียงบางส่วน: ถ้วยยังคงมีหาง

การกำหนดพฤติกรรมการพิมพ์ชนิดที่แน่นอนของอัลกอริทึมเป็นปัญหาที่ไม่ตัดสินได้เหมือนกับการพิจารณาพฤติกรรมการยุติของมัน (ดูchapter 11) พิจารณาอัลกอริทึมที่ในนั้นเฉพาะสาขา "then" ของเงื่อนไขมี type error อัลกอริทึมนี้มี type error เฉพาะเมื่อเงื่อนไขของเงื่อนไขประเมินเป็น true และเลือกสาขานั้น ปัญหาคือการหาค่าของเงื่อนไขนั้นอาจต้องการการคำนวณที่ซับซ้อนอย่างไม่จำกัด (เช่น เงื่อนไขอาจเป็นตัวแปรที่ค่าถูกคำนวณในลูป) เนื่องจากเราไม่สามารถแน่ใจได้ว่าการคำนวณดังกล่าวจะยุติหรือไม่ (เพราะเราไม่สามารถแก้ปัญหา halting) เราจึงไม่สามารถรู้ล่วงหน้าว่าเงื่อนไขจะเป็นจริงหรือไม่ และดังนั้นเราจึงไม่สามารถรู้ได้ว่าโปรแกรมจะมี type error หรือไม่

เพื่อจัดการกับความไม่สามารถทำนายพฤติกรรมของอัลกอริทึมนี้ static type checking ประมาณค่าภายในอัลกอริทึม เพื่อหลีกเลี่ยงการคำนวณที่อาจนำไปสู่การไม่ยุติ static type checking จะระมัดระวังเกินไปและรายงาน type error เมื่อไหร่ก็ตามที่อาจมีข้อผิดพลาด ในกรณีของเงื่อนไขนี้ static type checker จะต้องการให้ทั้งสองทางเลือกไม่มี type error เพราะมันไม่สามารถคำนวณค่าของเงื่อนไขได้ ดังนั้นมันจะรายงาน type error แม้ว่าจะมีเพียงสาขาเดียวที่มีข้อผิดพลาด แม้ว่าอัลกอริทึมอาจจะไม่แสดง type error เมื่อรันจริง static type checker ก็จะแสดงว่าอัลกอริทึมไม่ถูกต้องตามชนิดและจะไม่รันมัน นี่คือราคาที่ต้องจ่ายเพื่อความปลอดภัยของ static type checking: บางอัลกอริทึมจะถูกปฏิเสธแม้ว่ามันอาจจะไม่ก่อให้เกิดข้อผิดพลาดเมื่อรันจริง

Static type checking แลกความเร็วด้วยความแม่นยำ ในขณะที่ข้อผิดพลาดอาจจะไม่เกิดขึ้นจริงในภายหลัง มันอาจเกิดขึ้นได้ หากการคำนวณสำคัญพอที่จะไม่เสี่ยงต่อความล้มเหลว ก็จะดีกว่าแก้ไขข้อผิดพลาดที่อาจเกิดขึ้นในอัลกอริทึมก่อนการรัน วิธีการระมัดระวังของ static type checking ไม่ได้จำกัดอยู่แค่การคำนวณ มีโดเมนอื่นๆ ที่ทำการตรวจล่วงหน้า เช่น หากคุณขึ้นเครื่องบิน คุณคาดหวังว่าคนขับจะตรวจให้แน่ใจว่ามีน้ำมันเพียงพอและระบบสำคัญทำงาน ถือเป็น static type checking สำหรับการบิน ลองคิดทางเลือกคือการตรวจระบบหลังจากเครื่องบินขึ้น การตรวจพบปัญหาในเวลานั้นอาจสายเกินไป หรือถ้าคุณจะรับการรักษาทางการแพทย์ แพทย์ควรตรวจหาข้อห้ามก่อนการรักษาเพื่อป้องกันอันตราย Static type checking ตามสุภาษิตว่า "Better safe than sorry." ตาม static typing Ron ไม่ควรใช้คาถา Eat Slugs; เพราะไม้กายสิทธิ์ของเขาแตก กฎสำหรับการประยุกต์เวทมนตร์จึงไม่ใช้ได้และเป็นสัญญาณล่วงหน้าของความผิดพลาดในระหว่างการรัน ในทางกลับกัน dynamic typing เป็นวิธีที่ไม่รุกล้ำมากนักสำหรับบังคับกฎที่ไม่ได้ปล่อยโอกาสใดๆ ให้กับการคำนวณ มันคือสิ่งที่ Ron เลือกทำ เขาเสี่ยง และมันก็ไม่เวิร์ก

Building Code (การสร้างโค้ด)

การละเมิดกฎการกำหนดชนิดเป็นสัญญาณว่ามีบางสิ่งผิดปกติ Type error ในอัลกอริทึมบอกว่าอัลกอริทึมอาจจะไม่ทำงานอย่างถูกต้อง มองในแง่บวก เมื่อทุกส่วนของอัลกอริทึมสอดคล้องกับกฎการกำหนดชนิด ชนิดของข้อผิดพลาดบางอย่างก็จะถูกตัดออก และอัลกอริทึมก็ถูกต้องในระดับหนึ่ง แน่นอนว่าอัลกอริทึมยังอาจให้ผลลัพธ์ที่ไม่ถูกต้องได้ เช่น ถ้าเราต้องการอัลกอริทึมสำหรับการบวกสองตัวเลข ซึ่งมีชนิดเป็น (Number, Number) → Number แต่เราสร้างอัลกอริทึมสำหรับการลบตัวเลขโดยบังเอิญ อัลกอริทึมนี้ยังคงมี type ถูกต้อง แต่ไม่ได้คำนวณค่าที่ถูกต้อง อย่างไรก็ตาม ในโปรแกรมที่ถูกต้องตามชนิด ข้อผิดพลาดจำนวนมากจะถูกตัดออก และเราสามารถมั่นใจได้ว่าสเต็ปของอัลกอริทึมสอดคล้องกับระดับความสอดคล้องที่สำคัญ

การป้องกันการคำนวณที่ผิดหรือไม่มีความหมายเป็นบทบาทสำคัญของ types และ typing rules แต่ไม่ใช่ประโยชน์เดียวที่พวกมันให้ Types ยังทำหน้าที่เป็นคำอธิบายของขั้นตอนในอัลกอริทึมโดยที่เราไม่ต้องเข้าใจรายละเอียดของทุกขั้นตอนเพียงแค่ดูชนิด เราสามารถได้ภาพรวมว่ากำลังคำนวณอะไร ความสามารถแยกความแตกต่างของการคำนวณตามชนิดถูกยกตัวอย่างด้วยงานเลือกซองที่มีอัลกอริทึมที่ถูกต้อง ความสามารถของ types ในการสรุปการคำนวณจำนวนมากให้เป็นภาพรวมช่วยให้เห็นเชิงลึกที่ไม่สามารถได้จากการดูตัวอย่างเพียงไม่กี่ตัวอย่าง ดังนั้น types และ typing rules จึงมีคุณค่าเชิงอธิบายด้วย

ตัวอย่างเช่น ลองมาดูเกม Quidditch อีกครั้ง เกมสามารถอธิบายได้โดยไม่ต้องแสดงเกมจริงโดยการบรรยายกฎทั่วไปและบทบาทของผู้เล่นต่างๆ นี่เป็นวิธีที่ Harry เรียนรู้จาก Oliver Wood ใน Harry Potter and the Sorcerer’s Stone. กฎของเกมจำกัดการกระทำที่ถูกต้องในเกมและกำหนดวิธีการคิดคะแนน สิ่งสำคัญคือกฎของเกมเป็น typing rules ที่ใช้ types สำหรับบทบาทของผู้เล่น (เช่น "seeker") และชนิดของวัตถุ (เช่น "quaffle") แม้การดูตัวอย่างเกมจะช่วยได้ แต่ก็ไม่พอที่จะเข้าใจเกม โดยเฉพาะแม้หลังจากดูเกมหลายๆ ครั้ง คนที่ไม่รู้กฎก็ยังอาจประหลาดใจได้ เช่น การจบเกมทันทีเมื่อ seeker จับ Golden Snitch สิ่งนี้อาจไม่เกิดขึ้นในตัวอย่างที่ได้ดูมาก่อน ดังนั้นคนดูคนหนึ่งอาจประหลาดใจครั้งแรกที่เห็นมันเกิดขึ้น เกมอื่นๆ ก็มีเฉพาะกฎพิเศษที่น่าประหลาดใจเช่นนี้ เช่น กฎล้ำหน้าในฟุตบอลหรือการเดิน en passant ในหมากรุก การเรียนรู้เกมจากการดูตัวอย่างเพียงอย่างเดียวจึงยาก และอาจต้องใช้เวลานานมากกว่ากฎทั้งหมดจะถูกแสดงขึ้น

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

Types โครงสร้างวัตถุในโดเมน และ typing rules อธิบายวิธีการผสมผสานพวกมันในทางที่มีความหมาย ในวิทยาการคอมพิวเตอร์ types และ typing rules รับประกันการโต้ตอบที่มีความหมายของส่วนต่างๆ ของอัลกอริทึม ดังนั้นพวกมันเป็นเครื่องมือสำคัญสำหรับการสร้างระบบใหญ่จากระบบย่อย นี่จะถูกสำรวจในchapter 15