Terminologi yang benar dalam teori tipe: tipe, konstruktor tipe, macam / macam dan nilai

Dalam jawaban untuk pertanyaan sebelumnya , debat kecil dimulai tentang terminologi yang benar untuk konstruksi tertentu. Karena saya tidak menemukan pertanyaan (selain ini atau itu , yang bukan hal yang benar) untuk mengatasinya dengan jelas, saya membuat yang baru ini.

Istilah yang dipertanyakan dan hubungannya adalah: tipe, tipe konstruktor, tipe parameter, jenis atau jenis, dan nilai .

Saya juga memeriksa wikipedia untuk jenis teori, tapi itu juga tidak banyak menjelaskan.

Jadi demi memiliki jawaban referensi yang bagus dan untuk memeriksa pemahaman saya sendiri:

• Bagaimana hal-hal ini didefinisikan dengan benar?
• Apa perbedaan antara masing-masing hal ini?
• Bagaimana mereka terkait satu sama lain?

Baiklah, mari kita pergi satu per satu.

Nilai-nilai

Nilai adalah bagian konkret dari data yang dievaluasi dan disulap oleh program. Tidak ada yang mewah, beberapa contoh mungkin

• 1
• true
• "fizz buzz foo bar"

Jenis

Deskripsi yang bagus untuk suatu tipe adalah "classifier for a value". Tipe adalah sedikit informasi tentang nilai tersebut pada saat runtime, tetapi ditunjukkan pada waktu kompilasi.

Sebagai contoh jika Anda memberi tahu saya bahwa e : boolpada waktu kompilasi, dan saya akan tahu itu ebaik trueatau falseselama runtime, tidak ada yang lain! Karena tipe mengklasifikasikan nilai dengan baik seperti ini, kami dapat menggunakan informasi ini untuk menentukan beberapa properti dasar dari program Anda.

Misalnya, jika saya melihat Anda menambahkan edan e'kapan e : intdan e' : String, maka saya tahu ada sesuatu yang salah! Sebenarnya saya bisa menandai ini dan melemparkan kesalahan pada waktu kompilasi, mengatakan "Hei, itu tidak masuk akal sama sekali!".

Sistem tipe yang lebih kuat memungkinkan tipe yang lebih menarik yang mengklasifikasikan nilai yang lebih menarik. Sebagai contoh, mari kita pertimbangkan beberapa fungsi

f = fun x -> x

Sudah cukup jelas f : Something -> Something, tetapi apa yang seharusnya Something? Dalam sistem tipe yang membosankan, kita harus menentukan sesuatu yang sewenang-wenang Something = int. Dalam sistem tipe yang lebih fleksibel, bisa dikatakan

f : forall a. a -> a

Artinya "untuk apa pun a, fmemetakan suatu ake a". Ini mari kita gunakan secara flebih umum dan menulis program yang lebih menarik.

Selain itu, kompiler akan memeriksa benar-benar memuaskan penggolong yang telah kita berikan, jika f = fun x -> truekemudian kita memiliki bug dan kompiler akan berkata begitu!

Jadi sebagai tldr; tipe adalah batasan waktu kompilasi pada nilai-nilai yang bisa diekspresikan saat runtime.

Tipe Pembuat

Beberapa jenis terkait. Misalnya daftar bilangan bulat sangat mirip dengan daftar string. Ini hampir seperti bagaimana sortuntuk bilangan bulat hampir seperti sortuntuk string. Kita dapat membayangkan semacam pabrik yang membangun jenis yang hampir sama dengan menggeneralisasi perbedaan mereka dan membangunnya berdasarkan permintaan. Itulah tipe konstruktor. Ini semacam fungsi dari tipe ke tipe, tetapi sedikit lebih terbatas.

Contoh klasik adalah daftar generik. Konstruktor tipe hanya definisi generik

 data List a = Cons a (List a) | Nil

Sekarang Listadalah fungsi yang memetakan suatu tipe ake daftar nilai dari tipe itu! Di Jawa-tanah saya pikir ini mungkin disebut "kelas generik"

Ketik Parameter

Parameter tipe hanyalah tipe yang diteruskan ke konstruktor tipe (atau fungsi). Sama seperti di level nilai kita akan mengatakan foo(a)memiliki parameter asama seperti bagaimana List amemiliki parameter tipe a.

Jenis

Jenisnya agak rumit. Ide dasarnya adalah jenis-jenis tertentu serupa. Sebagai contoh, kita memiliki semua jenis primitif di java int, char, float... yang semua berperilaku seolah-olah mereka memiliki "tipe" yang sama. Kecuali, ketika kita berbicara tentang pengklasifikasi untuk tipe itu sendiri, kita menyebut jenis pengklasifikasi. Jadi int : Prim, String : Box, List : Boxed -> Boxed.

Sistem ini memberikan aturan konkret yang bagus tentang jenis apa yang bisa kita gunakan di mana, seperti bagaimana jenis mengatur nilai. Jelas tidak masuk akal untuk mengatakan

 List<List>

atau

 List<int>

Di Jawa karena Listperlu diterapkan pada jenis beton untuk digunakan seperti itu! Jika kita melihat jenis mereka List : Boxed -> Boxeddan karena itu Boxed -> Boxed /= Boxed, di atas adalah kesalahan jenis!

Sebagian besar waktu kita tidak benar-benar berpikir tentang jenis dan hanya memperlakukan mereka sebagai "akal sehat", tetapi dengan sistem tipe yang lebih bagus itu adalah sesuatu yang penting untuk dipikirkan.

Sedikit ilustrasi tentang apa yang telah saya katakan sejauh ini

 value   : type : kind  : ...
 true    : bool : Prim  : ...
 new F() : Foo  : Boxed : ...

Bacaan Lebih Baik Dari Wikipedia

Jika Anda tertarik dengan hal semacam ini, saya akan sangat menyarankan berinvestasi buku teks yang bagus. Teori tipe dan PLT secara umum cukup luas dan tanpa dasar pengetahuan yang koheren, Anda (atau setidaknya saya) bisa berkeliaran tanpa harus berbulan-bulan.

Dua buku favorit saya adalah

• Jenis dan Bahasa Pemrograman - Ben Pierce
• Yayasan Praktis Bahasa Pemrograman - Bob Harper

Keduanya adalah buku-buku bagus yang memperkenalkan apa yang baru saja saya bicarakan dan banyak lagi detail yang indah dan dijelaskan dengan baik.

Bagaimana hal-hal ini didefinisikan dengan benar?

Mereka didefinisikan dengan benar oleh dukungan matematika yang kaku, akademis, memberikan pernyataan yang kuat tentang apa mereka, bagaimana mereka bekerja, dan apa yang dijamin.

Tetapi programmer sebagian besar tidak perlu tahu itu. Mereka perlu memahami konsepnya.

Nilai-nilai

Mari kita mulai dengan nilai, karena semuanya dibangun dari sana. Nilai adalah data yang digunakan dalam komputasi. Bergantung pada pendekatannya, itu adalah nilai-nilai yang dikenal semua orang: 42, 3.14, "Bagaimana sekarang sapi coklat", catatan personil untuk Jenny di bidang Akuntansi, dll.

Interpretasi lain dari nilai adalah simbol . Kebanyakan programmer memahami simbol-simbol ini sebagai "nilai" dari sebuah enumerasi. Leftdan Rightmerupakan simbol untuk enum Handedness(mengabaikan orang dan ikan ambidextrous).

Terlepas dari implementasinya, nilai adalah hal-hal berbeda yang digunakan oleh bahasa untuk melakukan perhitungan.

Jenis

Masalah dengan nilai adalah bahwa tidak semua perhitungan legal untuk semua nilai. 42 + goattidak masuk akal.

Di sinilah tipe ikut bermain. Tipe adalah metadata yang menentukan himpunan bagian dari nilai. The Handednessenum di atas adalah contoh yang baik. Jenis ini mengatakan "hanya Leftdan Rightdapat digunakan di sini". Ini memungkinkan program untuk menentukan sangat awal bahwa operasi tertentu akan menghasilkan kesalahan.

Penggunaan praktis lain yang perlu dipertimbangkan adalah bahwa di bawah tenda, komputer bekerja dengan byte. Byte 42 mungkin berarti angka 42, atau mungkin berarti karakter *, atau itu mungkin berarti Jenny dari Akuntansi. Jenis juga (dalam penggunaan praktis, tidak banyak teoritis) membantu mendefinisikan pengkodean untuk koleksi byte yang digunakan oleh komputer.

Jenis

Dan di sinilah kita mulai sedikit keluar. Jadi, ketika sebuah bahasa pemrograman memiliki variabel yang mengacu pada tipe, jenis apa itu memiliki?

Dalam Java dan C # misalnya, ia memiliki tipe Type(yang memiliki tipe Type, yang memiliki ... dan seterusnya). Ini adalah konsep di balik jenis . Dalam beberapa bahasa, Anda dapat melakukan sedikit hal yang lebih berguna dengan variabel Type daripada Java dan C #. Setelah itu terjadi menjadi berguna untuk mengatakan "Aku ingin nilai yang Type, tetapi juga beberapa jenis dari IEnumerable<int>". Ta-da! Jenis.

Sebagian besar programmer dapat memikirkan jenis-jenis seperti Java dan batasan generik C #. Pertimbangkan public class Foo<T> where T: IComparable{}. Dalam bahasa dengan jenis, T: kindOf(IComparable)deklarasi variabel menjadi sah; bukan hanya hal khusus yang dapat Anda lakukan di deklarasi kelas dan fungsi.

Tipe Konstruktor

Mungkin tidak mengejutkan, konstruktor tipe hanyalah konstruktor untuk tipe . "Tapi bagaimana Anda membangun suatu tipe? Tipe apa adanya ." Eh ... tidak banyak.

Juga tidak mengherankan, cukup sulit untuk membangun semua subset nilai berguna yang berbeda yang akan digunakan oleh program komputer. Ketik konstruktor berfungsi untuk membantu memungkinkan programmer untuk "membangun" subset tersebut dengan cara yang bermakna.

Contoh yang paling mana-mana dari tipe konstruktor adalah definisi array yang: int[4]. Di sini Anda menentukan 4konstruktor tipe, yang menggunakan nilai untuk membangun Anda sebuah array intdengan 4 entri. Jika Anda menentukan jenis input yang berbeda, Anda akan mendapatkan tipe output yang berbeda.

Generik adalah bentuk lain dari konstruktor tipe, menggunakan tipe lain sebagai inputnya.

Dalam banyak bahasa ada konstruktor tipe suka P -> Rmembangun tipe yang mewakili fungsi yang mengambil tipe Pdan mengembalikan tipe R.

Sekarang, konteksnya akan menentukan apakah "fungsi yang mengembalikan tipe" adalah konstruktor tipe atau tidak. Dalam pengalaman saya (memang terbatas), barisnya adalah "bisakah Anda menggunakan jenis ini pada waktu kompilasi?". Iya? Ketik konstruktor. Tidak? Hanya sebuah fungsi.

Ketikkan Parameter

Jadi Anda ingat parameter yang diteruskan ke Tipe Konstruktor? Mereka umumnya dikenal sebagai Type Parameters, karena bentuk umum dari Type Constructor adalah Type[param]atau Type<param>.