射型家庭和約束

Question

比方說我們有一些現有的類或約束C，並執行以下操作：

{-# TypeFamilyDependencies #-} 

type family F t = s | s -> t 

type D s = (s ~ T t, C t) 

當然type D s ...中失敗，因爲未知變量t的編譯，但我怎麼能寫像D s？我基本上想寫：

type D s = (C (T_Inverse s)) 

我想這應該是有效的，因爲作爲注入的T_Inverse存在。我只是不知道如何表達它。

Answer 1

最好的，我知道怎麼做纔是

type family FI a 
type D s = (s ~ F (FI s), C (FI s)) 

你必須形成（可能部分）部分FI自己，所以我不認爲射型家庭確實有幫助。內射型家庭在這一點上看起來非常有限和不自然。舉一個明顯的例子，GHC甚至不會接受它們是內射的！

blah :: F a ~ F b => a :~: b 
blah = Refl 

不通過類型檢查器。