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

ระบบประเภทต่างๆ ได้เกิดขึ้นจากการละทิ้งกฎโครงสร้าง บางส่วน ของการแลกเปลี่ยน การอ่อนตัว และการหดตัว:

ประเภทเรียงลำดับสอดคล้องกับตรรกะที่ไม่สลับที่ซึ่งการแลกเปลี่ยน การหดตัว และการลดทอนจะถูกละทิ้ง สิ่งนี้สามารถใช้เพื่อจำลองการจัดสรรหน่วยความจำแบบสแต็ก (ตรงข้ามกับประเภทเชิงเส้นซึ่งสามารถใช้เพื่อจำลองการจัดสรรหน่วยความจำแบบฮีป ) ^{[ 1 ] : 30–31} หากไม่มีคุณสมบัติการแลกเปลี่ยน วัตถุจะถูกใช้ได้ก็ต่อเมื่ออยู่ที่ด้านบนสุดของสแต็กที่จำลองไว้เท่านั้น หลังจากนั้นจะถูกดึงออก ส่งผลให้ตัวแปรทุกตัวถูกใช้เพียงครั้งเดียวตามลำดับที่ถูกนำเข้ามา

ประเภทเชิงเส้นสอดคล้องกับตรรกะเชิงเส้นและรับประกันว่าวัตถุจะถูกใช้เพียงครั้งเดียวเท่านั้น ซึ่งช่วยให้ระบบสามารถยกเลิกการจัดสรรวัตถุได้อย่างปลอดภัยหลังจากใช้งาน^{[ 1 ] : 6} หรือออกแบบอินเทอร์เฟซซอฟต์แวร์ที่รับประกันว่าทรัพยากรจะไม่สามารถใช้งานได้อีกต่อไปเมื่อถูกปิดหรือเปลี่ยนสถานะเป็นสถานะอื่น^{[ 2 ]}

ภาษาการเขียนโปรแกรม Cleanใช้ประเภทเอกลักษณ์ (รูปแบบหนึ่งของประเภทเชิงเส้น) เพื่อช่วยสนับสนุนการทำงานพร้อมกันการรับ/ส่งข้อมูล และการอัปเดต อาร์เรย์แบบในตัว^{[ 1 ] : 43}

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

คุณสมบัติการอ้างอิงเดี่ยวทำให้ระบบประเภทเชิงเส้นเหมาะสมที่จะใช้เป็นภาษาโปรแกรมสำหรับการคำนวณควอนตัมเนื่องจากสะท้อนถึงทฤษฎีบทห้ามการคัดลอกของสถานะควอนตัม จาก มุมมอง ของทฤษฎีหมวดหมู่ การห้ามการคัดลอกคือข้อความที่ระบุว่าไม่มีฟังก์ชันแนวทแยงมุมใดที่สามารถทำซ้ำสถานะได้ ในทำนองเดียวกัน จาก มุมมองของ ตรรกะเชิงผสมไม่มีตัวรวม K ใดที่สามารถทำลายสถานะได้ จาก มุมมอง ของแคลคูลัสแลมบ์ดาตัวแปรxสามารถปรากฏได้เพียงครั้งเดียวในเทอม^{[ 3 ]}

ระบบประเภทเชิงเส้นเป็นภาษาภายในของหมวดหมู่โมโนอิดัลสมมาตรแบบปิดในลักษณะเดียวกับที่แคลคูลัสแลมบ์ดาแบบง่ายเป็นภาษาของหมวดหมู่ปิดแบบคาร์ทีเซียนกล่าวให้แม่นยำยิ่งขึ้น เราสามารถสร้างฟังก์ชันระหว่างหมวดหมู่ของระบบประเภทเชิงเส้นและหมวดหมู่ของหมวดหมู่โมโนอิดัลสมมาตรแบบปิดได้^{[ 4 ]}

ประเภทแอฟฟิน (Affine types)เป็นรูปแบบหนึ่งของประเภทเชิงเส้น (Linear types) ที่อนุญาตให้ละทิ้ง (กล่าวคือไม่ใช้ ) ทรัพยากร ซึ่งสอดคล้องกับตรรกะแอฟฟินทรัพยากรแอฟฟินสามารถใช้ได้มากที่สุดเพียงครั้งเดียว ในขณะที่ทรัพยากรเชิงเส้นจะต้องใช้เพียงครั้งเดียว เท่านั้น

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

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

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

ภายใต้การตีความทรัพยากร ประเภท แอฟฟินไม่สามารถใช้ได้มากกว่าหนึ่งครั้ง

ตัวอย่างเช่น รูปแบบเดียวกันของเครื่องขายสินค้าอัตโนมัติของ Hoareสามารถแสดงได้ในภาษาอังกฤษ ภาษาตรรกศาสตร์ และภาษาRust :

fn ซื้อลูกอม( _ : เหรียญ) -> ลูกอม{ ลูกอม{} } fn ซื้อเครื่องดื่ม( _ : เหรียญ) -> เครื่องดื่ม{ เครื่องดื่ม{} }

ในตัวอย่างนี้ การที่ Coinเป็นประเภทแอฟฟิน (ซึ่งเป็นเช่นนั้น เว้นแต่ว่ามันจะใช้งาน คุณสมบัติ Copy ) หมายความว่า การพยายามใช้เหรียญเดียวกันสองครั้งเป็นโปรแกรมที่ไม่ถูกต้อง ซึ่งคอมไพเลอร์มีสิทธิ์ที่จะปฏิเสธ:

let coin = Coin {}; let candy = buy_candy ( coin ); // อายุการใช้งานของตัวแปร coin สิ้นสุดลงที่นี่let drink = buy_drink ( coin ); // ข้อผิดพลาดในการคอมไพล์: การใช้ตัวแปรที่ถูกย้ายซึ่งไม่มีคุณสมบัติ Copy

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

แต่สิ่งนี้ไม่ได้หมายความว่าไม่สามารถใช้ตัวแปรได้หากไม่ใช้ตัวแปรนั้นให้หมดเสียก่อน:

// ฟังก์ชันนี้แค่ยืมเหรียญ: เครื่องหมาย & หมายถึงการยืมfn validate ( _ : & Coin ) -> Result < (), () > { Ok (()) }// ตัวแปรเหรียญเดียวกันนี้สามารถใช้ได้ไม่จำกัดจำนวนครั้งตราบใดที่ยังไม่ได้ถูกย้ายlet coin = Coin {}; loop { validate ( & coin ) ? ; }

สิ่งที่ Rust ไม่สามารถแสดงได้คือประเภทเหรียญที่ไม่สามารถอยู่นอกขอบเขตได้ – ซึ่งจะต้องใช้ประเภทเชิงเส้น

ภายใต้การตีความทรัพยากร ประเภท เชิงเส้นไม่เพียงแต่สามารถเคลื่อนย้ายได้เช่นเดียวกับประเภทเชิงเส้นแบบแอฟฟิน แต่ต้องเคลื่อนย้ายด้วย เพราะการอยู่นอกขอบเขตถือเป็นโปรแกรมที่ไม่ถูกต้อง

{ // ต้องส่งต่อ ห้ามทิ้งlet token = HotPotato {};// สมมติว่าไม่ใช่ทุกสาขาที่จะกำจัดมันออกไป: ถ้า! คิว. is_full () { คิว. push ( token ); }// ข้อผิดพลาดในการคอมไพล์: ถือวัตถุที่ไม่สามารถทิ้งได้เมื่อขอบเขตสิ้นสุดลง}

ข้อดีอย่างหนึ่งของประเภทเชิงเส้นคือตัวทำลายกลายเป็นฟังก์ชันปกติที่สามารถรับอาร์กิวเมนต์ สามารถล้มเหลว และอื่นๆ ได้^{[ 5 ]}ตัวอย่างเช่น อาจช่วยหลีกเลี่ยงความจำเป็นในการเก็บสถานะที่ใช้เฉพาะสำหรับการทำลายเท่านั้น ข้อดีโดยทั่วไปของการส่งผ่านการพึ่งพาฟังก์ชันอย่างชัดเจนคือลำดับของการเรียกฟังก์ชัน – ลำดับการทำลาย – สามารถตรวจสอบได้แบบคงที่ในแง่ของอายุการใช้งานของอาร์กิวเมนต์ เมื่อเปรียบเทียบกับการอ้างอิงภายใน วิธีนี้ไม่จำเป็นต้องมีคำอธิบายประกอบอายุการใช้งานเหมือนใน Rust

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

ภายใต้การตีความทรัพยากร ประเภท ปกติจะไม่จำกัดจำนวนครั้งที่สามารถย้ายตัวแปรได้ภาษา C++ (โดยเฉพาะอย่างยิ่งความหมายของการย้ายแบบไม่ทำลาย) จัดอยู่ในประเภทนี้

auto coin = std :: unique_ptr <Coin> ( ); auto candy = buy_candy ( std :: move ( coin )); auto drink = buy_drink ( std :: move ( coin )); // นี่คือ โค้ดC++ ที่ถูกต้อง

ภาษาโปรแกรมต่อไปนี้รองรับชนิดข้อมูลเชิงเส้นหรือเชิงอัฟฟิน:

• ระบบเอฟเฟกต์
• ตรรกะเชิงเส้น
• ตรรกศาสตร์เชิงเส้น