1樓：Jason Hu
含有dependent type的系統至少可以表達first order logic，這種系統往上走全都是邏輯或者數學系統了，我自己的標準是這種系統更屬於type theory而不是type system。
dependent type是一種現象，說得是types depend on values，所以你這個問題很難界定。如果你說的是實現lambda cube三個方向的type theory，如CIC，ITT等，那麼這些type theory當然可以被發展了。不過他們的發展和數學和邏輯的發展息息相關。
另外值得指出的是，type theory諸如CoC, CIC, pCIC, ITT, ETT, HoTT, CTT等，他們都是dependent type，因為他們的表達力都嚴格強於first order logic。
2樓：
支援 type as first class citizen。
然後實現 untyped lambda 和 typed lambda，functional 和 objective-oriented，logic 和 algebra 的大一統。
什麼 reflection，polymorphism，dependent type，subtyping 都是自然而然就會有的了。
3樓：咖啡忘了加糖
可以考慮一下cubical的東西，畢竟hott下面ua沒有computational content這點很煩人。今年icfp好像又有乙個新的cubical type thoery的語言叫redprl出來。可以去看看。
4樓：Anqur
Homotopy type theory.
Martin-Lf』s type theory 沒有很好解決的乙個問題就是 intensional type theory 中的 identity types, 而引入的同倫 (homotopy) 的概念主要就是解決這個問題. Per Martin-Lf 其實也是其發展的參與者.
Dependent Type語言都是怎樣處理Sigma的歧義的
如果是指語法上的歧義，coq中有多種sigma type，但用的是不同的notation，包括 prod Type Type Type.Notation是A B,用於非dependent type的計算.ex forall A Type A Prop Prop.Notation是exists x,P...
善惡之上是什麼？
有沒有考慮過，沒有善惡。善惡只是人在不單一角度對事情的定義。思辨多角度看問題，你會發現善惡其實很模糊，或者是某種意義上善惡沒有意義。之所以能感受到善惡存在，說明有乙個辨別他的標準。那這個可以辨別善惡的標準就是 善惡之上 那這個 標準 是什麼，就是另外乙個問題了。數學性理性。理性超脫善惡，可以評價善惡...
如何理解《懸崖之上》的結局？
修煉中 我覺得這結局太突兀，太藝術化了。我覺得在找到小蘭後直接以黑色背景白色文字寫結局，然後再切換到送出鏡，能將想要表達的思想感情表達的更強烈，而且劇情會流暢不少 ABCDEFG 拿走藥片還挺迷的，如果女孩被俘，那麼見不到黎明，還吃不了藥片，如果沒有被俘或犧牲，那必然會見到黎明。拿走藥片只會可能造成...