1樓：Jason Hu
了解一下？這個真的略歷害。
2樓：
聽起來像是 Ilya Sergey 早期兩篇工作的想法：A correspondence between type checking via reduction and type checking via evaluation和From type checking by recursive descent to type checking with an abstract machine
3樓：Trebor
（知乎出瀉藥功能了///
我目前的做法是首先寫好ABT和unification w.r.t.
alpha-equivalence。然後，注意到給定乙個（沒有meta-variable的）judgment，並且把其derivation中用到的規則的名稱從下到上，從左到右（depth-first）排列出來，那麼是很容易還原這個推導樹的：用第一條規則的結論去匹配給定的judgment，然後再去推導特化的前提。
那麼，我們只需要用dfs搜尋所有可能的規則序列就行了。
不過，對於設計成bidirectional的規則集合，左半邊是把rule作為pattern，而右半邊則相反。因此一般來說需要推導的judgement右半邊就是乙個pattern。為了統一性，我直接用了unification。
這樣當規則是bidirectional時，一定可以工作（？這還沒有證明）。但是有時候是會卡住的（因為meta-variable可以帶closure），這種情況就直接停止思考。
舉乙個非常簡單的例子。
(for each A primitive, a in Aa synth ~> A
a synth ~> A, b synth ~> Ba, b) synth ~> A * B
那，我們如果把(a, (c, b))丟給直譯器讓它合成型別，這就是相當於讓它自己搜尋(a, (c, b)) synth ~> X的derivation。（這裡有基本型別a : A, b :
B, c : C）
那首先與第一條規則（實際上是一類）合一化，發現(a, (c, b))不與任何基本元素相同。然後去找第二條規則，合一化之後我們需要推導a synth ~> A1和(c, b) synth ~> B1 。這裡需要注意每次用規則的時候都要把裡面的meta-variable重新整理。
接下來第乙個顯然用第一條規則可以得到A1就是A，第二個用第二條規則，我們還需要推導c synth ~> A2和b synth ~> A3。以此類推。
但是目前的問題是如果直接在底層支援ABT的話寫一些東西會比較麻煩。所以我打算把這個支援去掉，然後ABT也用judgement和inference rule的形式呈現。
4樓：Slow Learner
（這個答案口胡的成分比較嚴重，還沒想清楚
偏一下題：乙個最直觀的看法時abstract interpretation可以被看成type checker (interpretation on abstract value，where abstract value is type) 而且這個是可以被systematically derived的
那我開始口胡了 -- 如果我把small-step semantic的inductive形狀的definition比喻成typing rule, 那也就是說我覺得最大的問題是small step semantic距離definitional interpreter/abstract machine transistion有一點距離 -- 因為你要先證明small step semantic是determinstic的，它才有可能能轉成interpreter的形式，然後你才能抽象掉definitional interpreter。。。、同理莫非你也要先證明typing rule有一些較好的性質你才能那麼做？比如每個term只有乙個principal type （或許用錯名詞了，大致是每個term只有乙個type
我又忽然覺得用small-step比喻不太好，因為typing rule裡的sequent from 是把乙個term和乙個type聯絡起來的 -- 哪應該用big-step會好一點，which 把乙個term和最終value連線了起來。。。
但在怎麼說，直覺上來說我覺得這完全有乙個工程上的解決方案 -- 反正typing rule裡面的term都是inductively defined的，你就不斷pattern matching back就行了（沒細想過複雜的typing rule。。。題主這方面比我更清楚）
忽然覺得這個答案一點幫助也沒有 Arend的typing rule肯定高階大氣複雜。。。您加油我就拋磚引玉一下。
口胡完了
哪些學校的型別系統與編譯器方向不錯？
黃二狗 國內不建議往編譯優化這個大坑裡跳，編譯器太過古老，研究的年代和人數太多，就意味著裡面研究成果太多，意味著你可能連前人的東西都沒搞明白太多就糊里糊塗的找了乙個小方向，啃點別人剩下的骨頭渣，只能在一些特殊應用上有點優化效果。當然，如果你的老闆和實驗室能直接把你拎到前沿另說，不過就我校來看，老師們...
什麼樣的型別系統可以支援接收型別作為引數，值作為返回值的函式？
藥罐子千里冰封 自問自答 一年後終於想起並解決了這個問題。只要通過反射操縱一下 type checking monad 去推導表示式的型別，數一下 Maybe 的數量就好了 joinMaybe Maybe Maybe A Maybe A joinMaybe just just x just x jo...
可以簡單解釋一下《心理型別》裡對於「投射」的定義嗎？如下？
投射，就是一種推測，針對有限的事實根據自己本身的經驗作出的判斷，這種判斷過於主觀。所以需要警惕的是它的準確性，但是有時候對錯與否根本不重要，重要的是你要怎麼想。不同的人買了同樣的家具，卻擺出不同的風格，這就是投射的意義。也就是說，客體就像是家具，在不同的人眼裡形態可能不同。 坑太多沒填orz 我口胡...