如何實現typeOf函數？

Question

由於類型是伊德里斯一流的，好像我應該能夠編寫一個typeOf函數返回其參數的類型：

typeOf : a => a -> Type 
typeOf x = a 

然而，當我試圖調用這個函數，我得到看起來像一個錯誤：

*example> typeOf 42 
Can't find implementation for Integer 

我怎樣才能正確地實現這個功能typeOf？或者是否存在一些我錯過的「獲得某種價值類型」的想法，這會阻止這種功能的存在？

Answer 1

寫這樣說：

typeOf : {a : Type} -> a -> Type 
typeOf {a} _ = a 

a => b是由具有界面分辨率填寫一個隱含參數的函數。 {a : b} -> c是一個由統一填充的隱含參數的函數。

這裏沒有必要引用接口。每個術語都有一個類型。如果你寫typeOf 42，隱含的a通過統一被推斷爲Integer。