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

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

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

The Types of Magic and the Magic of Types (ประเภทของเวทมนตร์และเวทมนตร์แห่งประเภท)

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

เพื่อช่วยให้เข้าใจโลกแห่งเวทมนตร์ได้ง่ายขึ้น มันถูกจัดหมวดหมู่เป็นแนวคิดต่างๆ ที่เกี่ยวข้องกัน ตัวอย่างเช่น คนที่ทำเวทมนตร์ได้เรียกว่าพ่อมด (wizard) หรือแม่มด (witch) ในขณะที่คนธรรมดาที่ทำเวทมนตร์ไม่ได้เรียกว่ามักเกิล (muggle) พ่อมดยังถูกแบ่งย่อยออกเป็นอาชีพต่างๆ เช่น ออโรร์ (auror) นักเลขศาสตร์เวทมนตร์ (arithmancer) ผู้สลายคำสาป (curse breaker) นักสมุนไพรศาสตร์ (herbologist) และอื่นๆ อีกมากมาย การกระทำทางเวทมนตร์เรียกว่าคาถาหรือสเปลล์ (spell) และถูกจำแนกเพิ่มเติมเป็นมนตร์เสน่ห์ (charm) คำสาป (curse) การแปรรูป (transfiguration) และหมวดหมู่อื่นๆ ชื่อที่กำหนดให้กับหมวดหมู่ค่อนข้างจะเป็นไปตามอำเภอใจและไม่ได้สำคัญอะไรมากนัก สิ่งที่สำคัญคือคุณสมบัติและพฤติกรรมที่วัตถุทั้งหมดในหมวดหมู่หนึ่งมีร่วมกัน และที่สำคัญพอๆ กับความหมายของหมวดหมู่เวทมนตร์แต่ละประเภท ก็คือความสัมพันธ์ระหว่างหมวดหมู่เหล่านั้น ตัวอย่างเช่น สเปลล์สามารถร่ายได้โดยพ่อมดเท่านั้น แต่สเปลล์สามารถส่งผลกระทบต่อทั้งพ่อมดและมักเกิลได้เหมือนกัน เวทมนตร์ใน แฮร์รี่ พอตเตอร์ ค่อนข้างซับซ้อน ในการร่ายสเปลล์อย่างมีประสิทธิภาพ พ่อมดโดยทั่วไปต้องใช้ไม้กายสิทธิ์และต้องสวดมนต์คาถา อย่างไรก็ตาม พ่อมดที่มีประสบการณ์สามารถร่ายสเปลล์แบบไม่มีเสียงพูดได้โดยไม่ต้องใช้ไม้กายสิทธิ์ ผลของสเปลล์มักมีขอบเขตจำกัดทางเวลา และบางครั้งก็สามารถป้องกันได้ด้วยการร่ายสเปลล์โต้ตอบ เวทมนตร์ยังสามารถถูกเก็บรักษาไว้ในยาต้มได้อีกด้วย ซึ่งทำให้แม้แต่มักเกิลก็สามารถใช้เวทมนตร์ได้หากพวกเขาสามารถเข้าถึงยาต้มเหล่านี้ ความที่เวทมนตร์ไม่ใช่เรื่องเล็กน้อยยังสะท้อนให้เห็นในความจริงที่ว่าพ่อมดและแม่มดรุ่นเยาว์ต้องเข้าเรียนโรงเรียนพ่อมดแม่มดเป็นเวลาเจ็ดปีเพื่อให้เชี่ยวชาญในวิชานี้

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

ในวิทยาการคอมพิวเตอร์ กลุ่มของวัตถุที่มีพฤติกรรมในลักษณะใดลักษณะหนึ่งเรียกว่า type (ชนิด/ประเภท) เราได้พบกับ types ในหลายรูปแบบมาก่อนแล้ว ใน บทที่ 4 เราเห็น data types (ชนิดข้อมูล) ที่แตกต่างกัน (เซ็ต สแต็ก และคิว) สำหรับการจัดเก็บและดูแล collections ของวัตถุ แต่ละ data type มีวิธีการแทรก ดึงข้อมูล และลบองค์ประกอบออกจาก collection ที่ Distinctive ตัวอย่างเช่น สแต็กจะดึงวัตถุในลำดับย้อนกลับจากที่ใส่เข้าไป (เข้าหลังออกก่อน) และคิวจะดึงวัตถุในลำดับที่ใส่เข้าไป (เข้าก่อนออกก่อน) ดังนั้น data type หนึ่งๆ จะ encapsulate พฤติกรรมเฉพาะสำหรับการจัดการ collection ขององค์ประกอบ พฤติกรรมของ data type ทำให้มันเหมาะสมที่จะรองรับงานคำนวณเฉพาะ ตัวอย่างเช่น ใน บทที่ 13 ผมใช้ data type แบบสแต็กเพื่ออธิบายว่าอินเทอร์พรีเตอร์ทำงานและติดตามอาร์กิวเมนต์ต่างๆ อย่างไรเมื่ออัลกอริทึมถูกเรียกใช้แบบเรียกซ้ำ

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

( Number , Number ) → Number

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

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

( Hour , Minute ) → Alarm

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

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

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

( Wand , Incantation , Object ) → Levitating

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

List ( Number ) → List ( Number )

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

List ( comparable ) → List ( comparable )

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

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

Qsort : List ( comparable ) → List ( comparable )

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

Count : List ( any ) → Number

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

ประการแรก ถ้าเราต้องการ execute อัลกอริทึมใดอัลกอริทึมหนึ่ง input type ของมันบอกเราว่าเราต้องเตรียมอาร์กิวเมนต์ประเภทใด ตัวอย่างเช่น สเปลล์ต้องใช้คาถาและไม้กายสิทธิ์ในการร่าย ในขณะที่ยาต้มต้องดื่ม การดื่มสเปลล์หรือการใช้คาถาและท่าทางไม้กายสิทธิ์กับยาต้มนั้นไม่สมเหตุสมผล ในทำนองเดียวกัน อัลกอริทึมการเรียงลำดับเช่น Qsort สามารถใช้กับ list ได้ แต่การนำไปใช้กับค่าเวลา (time value) นั้นไม่มีความหมาย หากไม่มีอาร์กิวเมนต์ของ type ที่ต้องการ อัลกอริทึมก็ไม่สามารถทำงานได้

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

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

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

Rules Rule (กฎคือกฎ)

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

typing rule อธิบาย type ของวัตถุภายใต้เงื่อนไขบางประการ เงื่อนไขที่ต้อง fulfilled เพื่อให้กฎสามารถใช้ได้เรียกว่า premises (ข้อตั้งต้น) และข้อความเกี่ยวกับ type ของวัตถุที่กฎ derived จาก premises เรียกว่า conclusion (ข้อสรุป) กฎเกี่ยวกับการแตกของวัตถุเปราะบางมีสาม premises คือ วัตถุนั้นเปราะบาง มันถูก dropped และพื้นผิวที่มันตกลงมาแข็งแรง conclusion ของกฎคือวัตถุนั้นแตกแล้ว typing rule ที่มีแต่ conclusion โดยไม่มี premises เรียกว่า axiom (สัจพจน์) เพื่อบ่งชี้ว่ามันเป็นจริงอย่างไม่มีเงื่อนไข ตัวอย่างเช่น "แฮร์รี่ พอตเตอร์เป็นพ่อมด" "3 เป็นตัวเลข" หรือ "กระจกบางเปราะบาง"

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

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

Premise แรกของกฎต้องการให้อัลกอริทึมมี input และ output type ข้อกำหนดนี้เกี่ยวข้องอย่างใกล้ชิดกับกฎการแปรรูปธาตุของแกมป์ (Gamp's Law of Elemental Transfiguration) ที่นำเสนอใน แฮร์รี่ พอตเตอร์กับเครื่องรางยมทูต ซึ่งกล่าวว่าอาหารไม่สามารถสร้างขึ้นจากความว่างเปล่าได้ มันสามารถ summon มาจากที่อื่นหรือทำให้ใหญ่ขึ้นได้เท่านั้น application rule สะท้อนคุณสมบัติ fundamental ของอัลกอริทึม นั่นคือ อัลกอริทึม depend on input เพื่อสร้าง output ที่แปรผันได้

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

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

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

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

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

ซอง A: ( Hour, Minute ) → Alarm

ซอง B: List ( any ) → Number

ซอง C: List ( comparable ) → List ( comparable

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

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

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

“ Wingardium Leviosa! ” เขาตะโกน พร้อมกับโบกแขนยาวๆ ของเขาเหมือนกังหันลม “นายร่ายผิด” แฮร์รี่ได้ยินเฮอร์ไมโอนี่พูดอย่างฉุนเฉียว “มันต้อง Wing-gardium Levi-o-sa ทำเสียง ‘การ์’ ให้ยาวและชัดเจน”

เนื่องจาก premise หนึ่งของการใช้สเปลล์ยกของลอยไม่ถูก fulfilled กฎจึงใช้ไม่ได้ และ conclusion ของมันคือการทำให้ขนนกลอย ก็ไม่เป็นจริง

การพบสถานการณ์ที่ typing rule ใช้ไม่ได้ไม่ได้หมายความว่ากฎนั้นผิด มันหมายความว่ากฎมีขอบเขตจำกัดและไม่สามารถใช้ทำนายพฤติกรรมในสถานการณ์ปัจจุบันได้ ยิ่งไปกว่านั้น เมื่อกฎใช้ไม่ได้ ก็ไม่ได้หมายความว่า conclusion ของกฎนั้นเป็นเท็จแน่นอน มันอาจยังเป็นจริงได้เพราะปัจจัยอื่นๆ ที่ไม่ได้ covered โดยกฎ ตัวอย่างเช่น กฎ "ถ้าฝนตก ถนนจะเปียก" ใช้ไม่ได้เมื่อแดดออก อย่างไรก็ตาม ถนนอาจยังเปียกได้ถ้ามีสปริงเกอร์ทำงาน หรือยกตัวอย่างจาก แฮร์รี่ พอตเตอร์ แม้ว่ารอนจะร่ายสเปลล์ Wingardium Leviosa ไม่ถูกต้อง ขนนกก็อาจเริ่มลอยได้เพราะคนอื่นร่ายสเปลล์ใส่ขนนกพร้อมกัน หรือค้อนที่ dropped อาจยังแตกเมื่อกระทบพื้นเพราะด้ามจับของมันร้าวอยู่แล้ว ดังนั้น เมื่อกฎใช้ไม่ได้ ก็ไม่สามารถสรุปอะไรได้ทั้งสิ้น

ดังนั้นมันอาจดูเหมือนไม่ใช่เรื่องใหญ่เมื่อ typing rules ใช้ไม่ได้ แต่มันขึ้นอยู่กับว่าการทำให้แน่ใจว่า conclusion เฉพาะเป็นจริงนั้นสำคัญแค่ไหน ในขณะที่การทำให้ขนนกลอยหรือการแตกของวัตถุที่ dropped เป็นเพียงเรื่องน่าสนใจ แต่ก็มีสถานการณ์มากมายที่ conclusion มีความสำคัญจริงๆ ลองนึกถึงมุก "คำพูดสุดท้ายอันโด่งดัง" ทั้งหลายที่เล่นกับ conclusion ที่ผิด เช่น "สายสีแดงตัดได้ปลอดภัย" "หมาดีๆ นี่นา" "เห็ดพวกนี้เป็นเห็ดกินได้" และอื่นๆ สำหรับการคำนวณ การทำให้ types ถูกต้องก็สำคัญเช่นเดียวกัน แม้ว่าจะไม่ค่อยถึงตาย แต่การดำเนินการกับค่าที่มี type ผิดจะทำให้การคำนวณล้มเหลวในกรณีส่วนใหญ่ นี่คือเหตุผล แต่ละขั้นตอนของอัลกอริทึมจะ transform ค่าหนึ่งค่าหรือมากกว่า และแต่ละ operation ที่ใช้ในกระบวนการนี้ depend on อาร์กิวเมนต์ของมันในการมี type เฉพาะ เพราะมันถูก define ให้ทำสิ่งที่มีความหมายเฉพาะกับค่าดังกล่าวเท่านั้น จำไว้ว่า เราไม่สามารถเรียงลำดับเวลาปลุก และเราไม่สามารถคำนวณรากที่สองของ list ได้ ถ้าขั้นตอนใดๆ ของอัลกอริทึมพบค่าที่มี type ที่ไม่คาดคิด มันก็ไม่รู้จะทำอย่างไรกับมันและติดขัด ผลที่ตามมาคือการคำนวณไม่สามารถเสร็จสมบูรณ์ได้และไม่สามารถ deliver ผลลัพธ์ที่มีความหมายได้ กล่าวโดยสรุปคือ ความสำเร็จของการคำนวณ depends on การส่งค่าเฉพาะที่มี type ถูกต้องให้กับ operations เท่านั้น

ดังนั้น typing rules จึงเป็นองค์ประกอบที่สำคัญของการคำนวณ เพราะมันสามารถ ensure ว่า operations จะไม่ติดขัดกับค่าที่ผิด และการคำนวณโดยรวมสามารถเสร็จสมบูรณ์ได้ 3 เช่นเดียวกับที่ typing rules สามารถใช้ระบุประโยคที่ไม่มีความหมาย เช่น "แฮร์รี่ พอตเตอร์ดื่มสเปลล์" มันก็สามารถระบุการใช้อัลกอริทึมที่ไร้สาระได้ เช่น Qsort (6:30 น.) และเนื่องจากอัลกอริทึมประกอบด้วยหลายขั้นตอนที่เกี่ยวข้องกับการใช้ operations และอัลกอริทึมอื่นๆ กับค่า typing rules จึงสามารถใช้ระบุข้อผิดพลาดภายในนิยามของอัลกอริทึม และสามารถสนับสนุนการสร้างอัลกอริทึมที่ type-correct ได้อย่าง active ซึ่งเป็นกระบวนการที่บางครั้งเรียกว่า type-directed programming (การเขียนโปรแกรมแบบชี้นำด้วยชนิด)

Typing rules ไม่เพียงป้องกันการใช้งาน operations กับค่าที่เป็นไปไม่ได้ซึ่งทำให้ติดขัดเท่านั้น แต่ยังป้องกันการใช้งานที่ไม่สมเหตุสมผลในบริบทใดบริบทหนึ่งด้วย ตัวอย่างเช่น ส่วนสูงและอายุของคุณสามารถแสดงเป็นตัวเลขได้ทั้งคู่ แต่การนำตัวเลขสองค่านี้มาบวกกันนั้นไม่สมเหตุสมผล การบวกไม่มีความหมายในกรณีนี้เพราะตัวเลขสองตัวเป็น represent ของสิ่งที่แตกต่างกัน (ดู บทที่ 3 ) ดังนั้นผลรวมของตัวเลขสองตัวจึงไม่ใช่ represent ของสิ่งใดและจึงไร้ความหมาย 4 เราพบตัวอย่างใน แฮร์รี่ พอตเตอร์ เช่นกัน ตัวอย่างเช่น ในเกมควิดดิช สองทีมพยายามทำประตูโดยการโยนลูกบอลที่เรียกว่าควาฟเฟิลเข้าห่วงประตูของฝ่ายตรงข้าม การใช้สเปลล์เทเลพอร์ตคงทำให้เรื่องนี้ง่ายมาก แต่นั่นจะทำให้เกมน่าเบื่อ และจะบั่นทอนเป้าหมายของเกมซึ่งก็คือการหาว่าทีมควิดดิชทีมไหนเก่งกว่า ดังนั้น การใช้เวทมนตร์อื่นนอกจากการบินไม้กวาดจึงไม่ได้รับอนุญาตสำหรับผู้เล่นในเกม ข้อจำกัดดังกล่าวมีอยู่ทั่วไปในเกม ข้อกำหนดในการเล่นตามดอกในเกมไพ่ หรือการเคลื่อนที่ของบิชอปในหมากรุกในแนวทแยงเท่านั้น ไม่ได้สะท้อนถึงความเป็นไปไม่ได้ที่จะเล่นไพ่ใบอื่นหรือเคลื่อนบิชอปเป็นเส้นตรง มันเป็นข้อจำกัดในบริบทเฉพาะเพื่อสนับสนุนเป้าหมายของเกม Types สามารถใช้ติดตาม represent เหล่านี้ควบคู่ไปกับการคำนวณเพื่อ ensure ว่า operations เคารพกฎของการรวมค่าที่ถูก represent ไว้

การละเมิด typing rule ในอัลกอริทึมเรียกว่า type error (ข้อผิดพลาดทางชนิด) มันบ่งบอกถึงความไม่สอดคล้องกันในการรวมกันของ operations และค่า อัลกอริทึมที่ไม่มี type error ใดๆ เรียกว่า type correct (ถูกต้องทางชนิด) type error ในอัลกอริทึมสามารถมีผลกระทบหลายแบบ ประการแรก มันอาจทำให้การคำนวณติดขัด ซึ่งอาจนำไปสู่การยกเลิกการคำนวณ และอาจตามด้วยการรายงานข้อผิดพลาด การพยายามหารตัวเลขด้วยศูนย์ typically มีผลกระทบแบบนี้ ใน แฮร์รี่ พอตเตอร์กับห้องแห่งความลับ ไม้กายสิทธิ์ของรอนหักและทำให้สเปลล์ทั้งหมดของเขาทำงานผิดพลาด ตัวอย่างเช่น สเปลล์กินทากที่เขาร่ายใส่มาลฟอยย้อนกลับมาใส่เขา และความพยายามของเขาในการเปลี่ยนหนูให้เป็นถ้วยก็ได้ผลลัพธ์เป็นถ้วยขนปุยที่มีหาง ในขณะที่ผลลัพธ์ที่แน่นอนอาจเป็นเรื่องที่น่าประหลาดใจ แต่การขาดความสำเร็จในเวทมนตร์ของรอนนั้นสามารถคาดเดาได้ เนื่องจากไม้กายสิทธิ์ที่หักของเขาละเมิด premise หนึ่งของ typing rule สำหรับเวทมนตร์ ในกรณีเหล่านี้ ผลกระทบของเวทมนตร์ที่ใช้ไม่ได้นั้นมองเห็นได้ทันที ประการที่สอง type error อาจไม่นำไปสู่ผลกระทบที่สังเกตได้ทันที ซึ่งหมายความว่าการคำนวณดำเนินต่อไปและ eventually เสร็จสิ้น แต่มันทำด้วยค่าที่ไร้ความหมายและจึง ultimately ให้ผลลัพธ์ที่ไม่ถูกต้อง การเพิ่มอายุและส่วนสูงของบุคคลเป็นตัวอย่างหนึ่ง

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

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

เนื่องจาก type correctness เป็น prerequisite ที่สำคัญสำหรับการทำงานที่ถูกต้องของอัลกอริทึมใดๆ จึงเป็นความคิดที่ดีที่จะตรวจสอบ type correctness โดยอัตโนมัติโดยใช้อัลกอริทึม อัลกอริทึมดังกล่าวเรียกว่า type checker (ตัวตรวจสอบชนิด) type checker จะ determine ว่าขั้นตอนในอัลกอริทึม conform กับ typing rules เกี่ยวกับ control structures ตัวแปร และค่าหรือไม่ type checker สามารถ spot type errors ในอัลกอริทึมและด้วยเหตุนี้จึงป้องกันการคำนวณที่ผิดพลาด

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

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

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

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

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

เพื่อจัดการกับความไม่สามารถ inherent ในการทำนายพฤติกรรมของอัลกอริทึมนี้ static type checking จะ approximate types ภายในอัลกอริทึม เพื่อหลีกเลี่ยงการคำนวณที่อาจนำไปสู่การไม่ยุติ (nontermination) static type checking จะระมัดระวังเกินไปและรายงาน type error เมื่อใดก็ตามที่อาจมี type error ในกรณีของ conditional นี่หมายความว่า static type checker จะ require ทั้งสอง alternatives ต้องไม่มี type error เนื่องจากมันไม่สามารถคำนวณค่าของเงื่อนไขได้ มันจึงรายงาน type error แม้ว่ามีเพียง branch เดียวของ conditional ที่มี type error ถึงแม้ว่าอัลกอริทึมอาจไม่แสดง type error ใดๆ เมื่อถูก execute แต่ static type checker จะ flag อัลกอริทึมว่า type-incorrect และไม่ execute มัน นี่คือราคาที่ต้องจ่ายเพื่อความปลอดภัยของ static type checking: อัลกอริทึมบางตัวจะถูกปฏิเสธแม้ว่ามันอาจจะไม่ produce ข้อผิดพลาดจริงๆ เมื่อถูก execute

Static type checking แลกเปลี่ยน immediacy เพื่อ accuracy ในขณะที่ข้อผิดพลาดอาจไม่เกิดขึ้นจริงในภายหลัง แต่มันก็อาจเกิดขึ้นได้ ถ้าการคำนวณมีความสำคัญมากพอที่จะไม่เสี่ยงต่อความล้มเหลว ก็ควรแก้ไขข้อผิดพลาดที่อาจเกิดขึ้นในอัลกอริทึมก่อนที่จะ execute มัน แนวทางที่ระมัดระวังของ static type checking ไม่ได้มีเฉพาะในการคำนวณเท่านั้น ยังมีอีกหลายโดเมนที่ทำการตรวจสอบล่วงหน้า ถ้าคุณกำลังขึ้นเครื่องบิน คุณ rely on นักบินที่ตรวจสอบให้แน่ใจว่ามีน้ำมันเพียงพอและระบบสำคัญทั้งหมดทำงาน正常 คุณกำลังคาดหวัง static type checking ของกฎสำหรับการบินที่ประสบความสำเร็จ ลองคิดถึงทางเลือกอื่นคือการตรวจสอบระบบหลังจากเครื่องขึ้นแล้ว การตรวจพบปัญหาในเวลานั้นอาจสายเกินไป หรือถ้าคุณกำลังจะได้รับการรักษาทางการแพทย์หรือใบสั่งยา หมอควรทำให้แน่ใจว่ามีการ determine ข้อห้ามใช้ใดๆ ก่อนการรักษาเพื่อป้องกันอันตราย Static type checking เป็นไปตามคติ "ปลอดภัยไว้ก่อน" (Better safe than sorry) ตามหลัก static typing รอนไม่ควรใช้สเปลล์กินทาก เพราะด้วยไม้กายสิทธิ์ที่หักของเขา กฎสำหรับการใช้เวทมนตร์จึงใช้ไม่ได้และบ่งบอกถึงความผิดพลาดระหว่างการ execute สเปลล์ ในทางตรงกันข้าม dynamic typing เป็นแนวทางที่ aggressive น้อยกว่าสำหรับการบังคับใช้ typing rules ที่ไม่ปล่อยให้โอกาสในการคำนวณใดๆ ผ่านไป โดยเสี่ยงต่อการพบข้อผิดพลาดระหว่างการ execute อัลกอริทึม นี่คือสิ่งที่รอนทำ เขาลองเสี่ยงและมันก็ไม่สำเร็จ

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

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

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

เพื่อ illustrate ลองกลับไปดูเกมควิดดิชอีกครั้ง เกมสามารถอธิบายได้โดยไม่ต้องแสดงเกมจริง โดยการอธิบายกติกาทั่วไปและบทบาทของผู้เล่นต่างๆ อันที่จริง นี่คือวิธีที่แฮร์รี่เรียนรู้เกมจากโอลิเวอร์ วูดใน แฮร์รี่ พอตเตอร์กับศิลาอาถรรพ์ . 5 กฎของเกม constraining การกระทำที่ถูกต้องในเกมและ define ว่าคะแนนถูกบันทึกอย่างไร ประเด็นสำคัญคือกฎของเกมก็คือ typing rules ที่ใช้ types สำหรับบทบาทของผู้เล่น (เช่น "ซีกเกอร์") และประเภทของวัตถุ (เช่น "ควาฟเฟิล") ในขณะที่การดูตัวอย่างเกมจะมีประโยชน์ แต่มันไม่เพียงพอที่จะเข้าใจเกม โดยเฉพาะอย่างยิ่ง แม้หลังจากดูเกมหลายเกม คนที่ไม่รู้กฎก็อาจถูก surprise ได้ง่าย ตัวอย่างเช่น เกมควิดดิชจะจบลงทันทีเมื่อซีกเกอร์จับโกลเด้นสนิทช์ สิ่งนี้อาจไม่เคยเกิดขึ้นในตัวอย่างที่ถูกดู ดังนั้นมันจะ surprise ผู้สังเกตการณ์ในครั้งแรกที่มันเกิดขึ้น เกมอื่นๆ ก็มีกฎพิเศษที่อาจ surprising เช่น กฎล้ำหน้าในฟุตบอล หรือการเดิน en passant ในหมากรุก การเรียนรู้เกมโดยแค่ดูตัวอย่างเป็นเรื่องยาก และอาจใช้เวลานานมากกว่ากฎทั้งหมดจะถูกแสดงออกมา

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

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