子型別(subtyping)是不是錯誤(ill defined)的東西?

時間 2021-05-31 16:18:24

1樓:baozii

先支援一下 @閱千人而惜知己 的答案,子型別是一種很自然的想法,而且這個概念是經過嚴格定義的,為什麼子型別經久不衰?我覺得最最核心的原因是 expression problem :

子型別允許函式在變化的資料結構上去工作,因此修改資料結構的代價比較小(儘管這件事的主要貢獻還是OOP本身,乙個方法僅僅對應乙個值,等於把積型別拆開了)

subtyping並不等於subclassing,子型別是一種非常精確具體的技術。oop是乙個非常龐大籠統的體系。不應該把oop發展中的一些問題歸咎於子型別系統

個人認為子型別最大的問題是被濫用,如果能用和型別還是使用和型別,能使用typeclass還是使用typeclass,真正適合子型別的地方實在不多。大多數OOP語言完全是因為沒有和型別和typeclass才「被迫」用子型別來代替

2樓:facetothefate

並不是。

subtyping 本質上是在講子集的問題。

表示子集需要用二階邏輯來表示:

即,存在乙個超類S存在乙個子類T使得屬於每乙個屬於子類T的元素都屬於超類S。

根據柯里霍華德同構,要能表達二階邏輯的lambda運算就是傳說中的system F了,也就是支援多型的lambda運算。

其中支援subtyping的擴充套件叫做system f-subhttps://

en.wikipedia.org/wiki/System_F

System F-sub - Wikipedia那麼system f有個缺點就是不能使用型別推導。為了使用型別推導,要麼別用system f,要麼就用受限的system f,比如Hindley–Milner type system(支援引數多型)。所以你才見到了一堆只支援一部分多型的帶型別推導的語言。

所以這只是個取捨問題。

3樓:Qinxiang Cao

這取決於你是站在type theory的立場看,還是站在set theory的立場看。

Type theory和set theory是兩種不同的建立數學基礎的方法。在程式語言的設計過程中,各自型別系統根據需要會設計為set theory狀的或者type theory狀的。

在set theory中,乙個集合A可以是乙個集合B的子集,那麼任何乙個集合A的元素x都是集合B的元素。

subtype即是按照此思路構建的乙個型別系統。乙個型別A如果是型別B的子類,那麼一切對B型別的操作都能對A型別的元素進行。

基本的Type theory中則沒有類似設定。如果想表達子集的概念往往需要借助單射等概念來表達。

因此,並不能說兩種型別系統哪一種更先進。只是根據程式語言的實際需求進行的選擇而已。題主如果試一試在Coq中處理『子集』、『子集的元素』這些概念,就會發現那是多麼的麻煩和不直觀。

4樓:luikore

它們也有的, 不過是這樣:

資料型別純組合, 不需要子型別

行為型別可以有子型別

都是一種建模手段, 但是考慮下面這些問題:

寫乙個 Point3D 繼承 Point2DBird 和 Plane 引數沒乙個同的但都能 fly我覺得還是資料型別不需要子型別比較好

5樓:

回答問題:子型別不但不是錯誤的東西,還很有價值。

你提到這些語言(haskell, coq, agda, idris)不是因為先進才沒有subtyping,而是因為不夠先進所以才沒有subtyping。不是因為calculus of constructions先進,而是因為我們無知。subtyping對應的curry-howard correspondence研究還很少,同樣,在object-oriented語言中融合full dependent types(而不僅僅是path dependent type)的研究也還很不充分。

6樓:潘敬華

在評價乙個概念是正確還是錯誤,是先進還在落後之前,請先給正確和先進下乙個定義。否則你這個問題就是錯誤(ill-defined)的。

女孩子冬季褲子型別有哪些?

錢多多 我只想上一款我自己新買毛呢闊腿褲,真的是好看爆了,設計感滿滿,質量還好,保暖又親膚,垂墜質感絕了,給你們直觀感受一下 其他褲型不做敘述了,反正也就那麼些,就分享乙個我最近發現的寶藏褲子 阿檬 冬季一定要是有厚度,甚至加絨的!強力推薦闊腿褲,真的好穿不貴,選擇加絨或者有厚度的材質,絕對讓你開啟...

C 怎麼用concept 判斷型別是不是容器呢?

已登出 好問題啊。雖然我很少遇到這樣的需求 除了在某些設計不太好的系統裡面 但也寫過類似的 Concepts 和 SFINAE。很多時候我們希望判斷乙個型別是不是容器,但實際上我們只是想通過 range for 迴圈表示式遍歷而已。另外需要注意,range for 迴圈表示式不僅接受傳統的容器,還接...

學生黨買膝上型電腦哪個牌子型別比較適合?

再見 任何東西任何品牌都有好的產品壞的產品別用品牌來論產品 再來筆記本有三種型別 輕薄本,遊戲本,和全能本 全能本 介於輕薄本和遊戲本之間。可能是很多想買輕薄本可是又要效能的人來說是寶物也可能對想玩遊戲的人來說是全都不能本。比輕薄本重效能比輕薄本強比遊戲本輕效能沒遊戲本強 筆記本一般也有最佳價效比區...