Mengapa dalam tipe data aljabar, jika saya dapat mendefinisikan fungsi `dari` dan `ke` khusus untuk dua tipe, kedua tipe tersebut dapat dianggap setara?

Saya membaca blog ini: http://chris-taylor.github.io/blog/2013/02/10/the-algebra-of-algebraic-data-types/

Ia mengatakan:

Namun, ketika saya berbicara tentang kesetaraan, yang saya maksud bukan kesetaraan Haskell, dalam arti fungsi (==). Sebaliknya, yang saya maksud adalah kedua tipe tersebut berkorespondensi satu-satu – yaitu, ketika saya mengatakan bahwa dua tipe a dan b adalah sama, maksud saya Anda dapat menulis dua fungsi

    from :: a -> b
    to   :: b -> a

yang memasangkan nilai a dengan nilai b, sehingga persamaan berikut selalu berlaku (di sini == adalah persamaan asli dengan rasa Haskell):

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

Dan kemudian, banyak undang-undang yang didasarkan pada definisi ini:

Add Void a === a
Add a b === Add b a
Mul Void a === Void
Mul () a === a
Mul a b === Mul b a

Saya tidak mengerti mengapa kita bisa dengan aman menetapkan undang-undang ini berdasarkan definisi "kesetaraan"? Bisakah menggunakan definisi lain? Apa yang bisa kita lakukan dengan definisi ini? Apakah masuk akal untuk sistem tipe Haskell?


equality haskell algebraic-data-types
person Freewind    schedule 03.08.2014    source sumber

Jawaban (3)


arrow_upward
5
arrow_downward

Istilah yang penulis gunakan, agar tidak "menyebutkan teori kategori atau matematika tingkat lanjut", adalah kardinalitas. Dia mendefinisikan dua tipe menjadi ===-sama satu sama lain jika keduanya memiliki kardinalitas yang sama -- yaitu, jika ada banyak kemungkinan nilai pada salah satu tipe tersebut dibandingkan dengan nilai lainnya.

Karena jika dua tipe mempunyai kardinalitas yang sama, maka terdapat isomorfisme di antara keduanya. Mul () Bool mungkin merupakan tipe yang berbeda dari Bool, tetapi jumlah anggota yang satu sama persis dengan yang lainnya, dan seseorang dapat dengan mudah mendefinisikan suatu fungsi untuk berpindah dari satu fungsi ke fungsi lainnya, atau fungsi lainnya ke fungsi lainnya. (Bukan berarti hanya ada satu isomorfisme -- intinya adalah, Anda dapat memilih salah satu.)

Ini bukan pendekatan yang bagus. Ini berfungsi dengan baik untuk himpunan berhingga, pada dasarnya, tetapi menimbulkan efek samping yang tidak menguntungkan untuk himpunan tak terhingga, seperti Add Int Int === Int. Namun, untuk deskripsi dasar penjumlahan dan perkalian jenis, sepertinya berguna.

person Sneftel    schedule 03.08.2014
comment
Terima kasih atas jawaban yang bagus. Untuk memahami hal ini dengan baik, mis. cardinality, category theory, bisakah Anda merekomendasikan saya buku apa saja? - person Freewind; 03.08.2014
comment
Selain itu, Add Int Int dan Int tidak memiliki persamaan yang sama karena Int adalah bilangan bulat 32-bit. Untuk tipe bilangan besar sembarang Anda akan menulis Integer. - person ThreeFx; 03.08.2014
comment
@Freewind Matematika Konseptual: Pengantar kategori yang pertama adalah pengantar teori kategori yang baik dan mudah dibaca yang tidak memerlukan banyak pengetahuan matematika prasyarat. Oleh karena itu, topik ini tidak terlalu mendalami pokok bahasannya, namun merupakan awal yang baik. Itu memang mencakup gagasan isomorfisme (dan beberapa gagasan terkait). Selain itu, Anda bukan Sneftel yang sama dari GDNet, bukan? Dunia kecil - person David Young; 04.08.2014
comment
@Freewind Selain itu, Anda mungkin ingin mencari gagasan tentang hubungan kesetaraan dan mencoba membuktikan bahwa definisi kesetaraan ini memenuhi hukum hubungan kesetaraan sebagai latihan. - person David Young; 04.08.2014
comment
@Freewind Oh, juga, ada buku Teori Tipe Homotopi yang menjelaskan banyak detail tentang apa artinya dua tipe setara satu sama lain (nilai juga) dan implikasinya (dan bagaimana gagasan itu sebenarnya memiliki pengaruh yang kuat koneksi ke gagasan homotopi dari topologi dan teori homotopi). Ini lebih mendalam, namun secara signifikan lebih sulit daripada Matematika Konseptual (saya masih mempelajari Teori Tipe Homotopi dan saya sedang berjuang dalam beberapa hal), namun pada akhirnya Anda mungkin tertarik untuk mempelajarinya. Saya pasti menyarankan memulai dengan Matematika Konseptual. - person David Young; 04.08.2014
comment
@DavidYoung, terima kasih banyak! Saya akan menemukan buku-buku ini, semoga saya bisa belajar lebih banyak tentang tipe - person Freewind; 04.08.2014
comment
@DavidYoung Ya, itu saya. - person Sneftel; 04.08.2014

arrow_upward
2
arrow_downward

Secara informal, ketika dua struktur matematika A,B mempunyai dua fungsi "bagus" from,to memuaskan from . to == id dan to . from == id, maka struktur A,B dikatakan isomorfik.

Definisi sebenarnya dari fungsi "bagus" bervariasi menurut jenis struktur yang ada (dan terkadang, definisi "bagus" yang berbeda menimbulkan pengertian isomorfisme yang berbeda).

Gagasan di balik struktur isomorfik adalah, secara kasar, mereka "bekerja" dengan cara yang persis sama. Misalnya, pertimbangkan struktur A yang dibuat oleh boolean True,False dengan &&,|| sebagai operasi. Misalkan struktur B terbuat dari dua natural1,0 dengan min,max sebagai operasi. Ini adalah struktur yang berbeda, namun memiliki aturan yang sama. Misalnya True && x == x dan 1 `min` x == x untuk semua x. A dan B bersifat isomorfik: fungsi to akan memetakan True ke 1, dan False ke 0, sedangkan from akan melakukan pemetaan sebaliknya.

(Perhatikan bahwa meskipun kita dapat memetakan True ke 0 dan False ke 1, dan kita masih akan mendapatkan from . to == id dan rangkapnya, pemetaan ini tidak akan dianggap "bagus" karena tidak akan mempertahankan strukturnya: misalnya, to (True && x) == to x namun to (True && x) == to True `min` to x == 0 `min` to x == 0 .)

Contoh lain dalam situasi berbeda: anggap A sebagai lingkaran pada bidang tersebut, sedangkan B adalah persegi pada bidang tersebut. Kemudian seseorang dapat mendefinisikan pemetaan kontinu to,from di antara pemetaan tersebut. Hal ini dapat dilakukan dengan dua "loop tertutup", secara longgar, yang dapat dikatakan isomorfik. Sebaliknya lingkaran dan bentuk "delapan" tidak dapat melakukan pemetaan kontinu seperti itu: titik yang berpotongan sendiri dalam "delapan" tidak dapat dipetakan ke titik mana pun dalam lingkaran secara terus menerus (kira-kira, empat "jalan" berangkat darinya , sedangkan titik-titik dalam lingkaran hanya memiliki dua "jalan" seperti itu.

Di Haskell, tipe juga dikatakan isomorfik ketika ada dua fungsi yang dapat ditentukan Haskell from,to di antara keduanya yang memenuhi aturan di atas. Di sini menjadi fungsi yang "bagus" berarti dapat didefinisikan di Haskell. blog web menunjukkan beberapa tipe isomorfik tersebut. Berikut contoh lainnya, menggunakan tipe rekursif:

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

Secara intuitif, yang pertama dibaca sebagai: "daftar adalah daftar kosong, atau pasangan yang terbuat dari elemen dan daftar". Yang kedua dibaca sebagai: "daftar adalah daftar kosong, atau elemen tunggal, atau gabungan tiga elemen, elemen lain, dan daftar". Seseorang dapat mengkonversi keduanya dengan menangani elemen dua sekaligus.

Contoh lain:

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

Anda dapat membuktikan bahwa tipe Tree Unit isomorfik terhadap List1 (Tree Unit) dengan memanfaatkan hukum aljabar yang ada di blog. Di bawah, = adalah singkatan dari isomorfisme.

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

Sketsa bukti di atas menginduksi fungsi to sebagai berikut.

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))))

Perhatikan bagaimana pemanggilan rekursif memainkan peran hipotesis induktif dalam pembuktiannya.

Penulisan from dibiarkan sebagai latihan :-P

person chi    schedule 03.08.2014
comment
Kita dapat membuat argumen yang baik bahwa akan lebih bijaksana untuk memberi label pada pengertian isomorfisme secara berbeda tergantung pada apa yang Anda sebut bagus – dan memang hal ini dilakukan di sebagian besar matematika, misalnya dalam kasus kontinu, hal ini sangat jarang disebut isomorfik tapi homeomorfik; jika Anda menambahkan analitik, itu diffeomorphic dll. - person leftaroundabout; 04.08.2014

arrow_upward
0
arrow_downward

Mengapa dalam tipe data aljabar, jika saya dapat mendefinisikan fungsi khusus from dan to untuk dua tipe, kedua tipe tersebut dapat dianggap sama?

Istilah yang lebih baik untuk digunakan di sini bukanlah "sama", melainkan isomorfik. Masalahnya adalah ketika dua tipe bersifat isomorfik, keduanya pada dasarnya dapat dipertukarkan satu sama lain; program apa pun yang ditulis dalam bentuk A, pada prinsipnya, dapat ditulis dalam bentuk B, tanpa mengubah arti dari program tersebut. Misalkan Anda memiliki:

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

dan kedua fungsi ini merupakan isomorfisme, yaitu:

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

Sekarang, jika Anda memiliki fungsi apa pun yang menggunakan A sebagai argumen, misalnya Anda dapat menulis fungsi yang menggunakan B sebagai argumen:

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

Dan untuk fungsi apa pun yang menghasilkan A, Anda juga dapat melakukan ini:

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

Sekarang Anda telah menyembunyikan semua penggunaan A di dalam subdefinisi where. Anda dapat melanjutkan jalur ini dan secara mekanis menghilangkan semua penggunaan A seluruhnya, dan Anda dijamin program akan bekerja sama seperti saat Anda memulai.

person Luis Casillas    schedule 04.08.2014