เหตุใดในประเภทข้อมูลพีชคณิต หากฉันสามารถกำหนดฟังก์ชัน `from` และ `to` พิเศษสำหรับสองประเภทได้ ทั้งสองประเภทก็ถือว่าเท่าเทียมกันได้

คำที่ผู้เขียนใช้คร่าวๆ เพื่อไม่ให้ "พูดถึงทฤษฎีหมวดหมู่หรือคณิตศาสตร์ขั้นสูง" คือ ภาวะเชิงภาวะ เขานิยามสองประเภทให้เป็น ===-เท่ากันหากมีจำนวนสมาชิกเท่ากัน นั่นคือ ถ้ามีค่าค่าหนึ่งที่เป็นไปได้มากเท่ากับค่าของอีกค่าหนึ่ง

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

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

พูดอย่างไม่เป็นทางการ เมื่อโครงสร้างทางคณิตศาสตร์สองตัว A,B มีฟังก์ชัน "ดี" สองฟังก์ชัน from,to ที่ทำให้ from . to == id และ to . from == id สอดคล้องกัน โครงสร้าง A,B จะถูกเรียกว่า ไอโซมอร์ฟิก

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

แนวคิดเบื้องหลังโครงสร้างไอโซมอร์ฟิกก็คือ พวกมัน "ทำงาน" ในลักษณะเดียวกันทุกประการ ตัวอย่างเช่น พิจารณาโครงสร้าง A ที่สร้างโดยบูลีน True,False โดยมี &&,|| เป็นการดำเนินการ ให้โครงสร้าง B ทำจาก naturals1,0 สองตัวโดยมี min,max เป็นการดำเนินการ สิ่งเหล่านี้มีโครงสร้างที่แตกต่างกัน แต่ก็มีกฎเกณฑ์เดียวกัน เช่น True && x == x และ 1 `min` x == x สำหรับ x ทั้งหมด A และ B เป็น isomorphic: ฟังก์ชัน to จะแมป True ถึง 1 และ False ถึง 0 ในขณะที่ from จะทำการแมปตรงกันข้าม

(โปรดทราบว่าแม้ว่าเราจะสามารถแมป True ถึง 0 และ False ถึง 1 และเราจะยังคงได้รับ from . to == id และคู่ของมัน การแมปนี้จะไม่ถือว่า "ดี" เนื่องจากจะไม่รักษาโครงสร้างไว้ เช่น to (True && x) == to x เลย to (True && x) == to True `min` to x == 0 `min` to x == 0 )

อีกตัวอย่างหนึ่งในสภาพแวดล้อมที่แตกต่างกัน: ถือว่า A เป็นวงกลมในระนาบ ในขณะที่ B เป็นสี่เหลี่ยมจัตุรัสในระนาบดังกล่าว จากนั้นเราสามารถกำหนดการแมป ต่อเนื่อง to,from ระหว่างกันได้ ซึ่งสามารถทำได้โดยใช้ "ลูปปิด" สองอันใดก็ได้ พูดง่ายๆ ซึ่งอาจกล่าวได้ว่าเป็นไอโซมอร์ฟิก วงกลมและรูปร่าง "แปด" ไม่ยอมรับการแมปที่ต่อเนื่องเช่นนี้ จุดที่ตัดกันเองใน "แปด" ไม่สามารถแมปกับจุดใดๆ ในวงกลมในลักษณะต่อเนื่องกัน (ประมาณ "วิธี" สี่ทางออกจากจุดนั้น ในขณะที่จุดในวงกลมมี "ทาง" ดังกล่าวเพียงสองทางเท่านั้น

ใน Haskell ประเภทต่างๆ ได้รับการกล่าวในทำนองเดียวกันว่าเป็น isomorphic เมื่อมีฟังก์ชัน from,to ที่ Haskell กำหนดได้ 2 รายการอยู่ระหว่างฟังก์ชันเหล่านั้นซึ่งเป็นไปตามกฎข้างต้น การเป็นฟังก์ชัน "ดี" ตรงนี้หมายถึงสามารถกำหนดได้ใน Haskell เว็บบล็อก แสดงประเภทไอโซมอร์ฟิกดังกล่าวบางประเภท นี่เป็นอีกตัวอย่างหนึ่งที่ใช้ประเภทเรียกซ้ำ:

List1 a = Add Unit (Mul a (List1 a))
List2 a = Add Unit (Add a (Mul a (Mul a (List2 a))))

โดยสังหรณ์ใจ รายการแรกอ่านว่า: "รายการอาจเป็นรายการว่าง หรือเป็นคู่ที่สร้างจากองค์ประกอบและรายการ" รายการที่สองอ่านว่า: "รายการคือรายการว่างหรือองค์ประกอบเดียว หรือองค์ประกอบสามรายการ องค์ประกอบอื่น และรายการ" หนึ่งสามารถแปลงระหว่างสองโดยการจัดการองค์ประกอบทั้งสองในแต่ละครั้ง

ตัวอย่างอื่น:

Tree a = Add Unit (Mul a (Mul (Tree a) (Tree a)))

คุณสามารถพิสูจน์ได้ว่าประเภท Tree Unit นั้นมีรูปร่างสมส่วนเป็น List1 (Tree Unit) โดยใช้ประโยชน์จากกฎพีชคณิตที่ใช้ในบล็อก ด้านล่าง = ย่อมาจาก isomorphism

List1 (Tree Unit)
-- definition of List1 a
= Add Unit (Mul (Tree Unit) (List1 (Tree Unit))) 
-- by inductive hypothesis, the inner `List1 (Tree Unit)` is isomorphic to `Tree Unit`
= Add Unit (Mul (Tree Unit) (Tree Unit))
-- definition of Tree a
= Tree Unit

ภาพร่างการพิสูจน์ข้างต้นทำให้เกิดฟังก์ชัน to ดังต่อไปนี้

data Add a b = InL a | InR b
data Mul a b = P a b
type Unit = ()
newtype List1 a = List1 (Add Unit (Mul a (List1 a)))
newtype Tree a  = Tree  (Add Unit (Mul a (Mul (Tree a) (Tree a))))

to :: List1 (Tree Unit) -> Tree Unit
to (List1 (InL ())) = Tree (InL ())
to (List1 (InR (P t ts))) = Tree (InR (P () (P t (to ts))))

สังเกตว่าการโทรซ้ำมีบทบาทอย่างไรตามสมมติฐานอุปนัยในการพิสูจน์

การเขียน from ถือเป็นแบบฝึกหัด :-P

เหตุใดในประเภทข้อมูลพีชคณิต หากฉันสามารถกำหนดฟังก์ชัน from และ to พิเศษสำหรับสองประเภทได้ ทั้งสองประเภทก็ถือว่าเท่ากันได้

คำที่ดีกว่าที่จะใช้ในที่นี้ไม่ใช่ "เท่ากัน" แต่เป็น ไอโซมอร์ฟิก ประเด็นก็คือเมื่อทั้งสองประเภทเป็นไอโซมอร์ฟิก โดยพื้นฐานแล้วพวกมันจะใช้แทนกันได้ โดยหลักการแล้วโปรแกรมใดๆ ที่เขียนด้วย A สามารถเขียนด้วย B แทนได้ โดยไม่เปลี่ยนความหมายของโปรแกรม สมมติว่าคุณมี:

from :: A -> B
to   :: B -> A

และฟังก์ชันทั้งสองนี้ประกอบขึ้นเป็นมอร์ฟิซึม นั่นคือ:

to (from a) == a
from (to b) == b

ตอนนี้ ถ้าคุณมีฟังก์ชันใดๆ ที่รับ A เป็นอาร์กิวเมนต์ คุณสามารถเขียนคู่ที่รับ B เป็นอาร์กิวเมนต์แทนได้:

foo :: B -> Something
foo = originalFoo . from
    where originalFoo :: A -> Something
          originalFoo a = ...

และสำหรับฟังก์ชันใดๆ ที่สร้าง A คุณก็ทำสิ่งนี้ได้เช่นกัน:

bar :: Something -> B
bar = to . originalBar
    where originalBar :: Something -> A
          originalBar something = ...

ตอนนี้ คุณได้ซ่อนการใช้ A ทั้งหมดไว้ในคำจำกัดความย่อย where แล้ว คุณสามารถดำเนินต่อไปตามเส้นทางนี้และกำจัดการใช้ A ทั้งหมดโดยอัตโนมัติ และคุณรับประกันว่าโปรแกรมจะทำงานเหมือนกับตอนที่คุณเริ่มต้น