12

顯然有點心不在焉,我寫了something like如下:何時(如果曾經)可以部分應用類型同義詞?

{-# LANGUAGE ConstraintKinds  #-} 
{-# LANGUAGE TypeFamilies  #-} 

class Foo f where 
    type Bar f :: * 
    retbar :: Bar f -> IO f 

type Baz f = (Foo f, Eq f) 

    -- WithBar :: * -> (*->Constraint) -> * -> Constraint 
type WithBar b c f = (c f, Bar f ~ b) 

instance Foo() where 
    type Bar() =() 
    retbar = return 

naim :: WithBar() Baz u => IO u -- why can I do this? 
naim = retbar() 

main = naim :: IO() 

只有在編譯成功,我意識到這不是應該實際工作:Baz被定義爲一個參數一個類型的同義詞,但我在這裏沒有直接的論據。當我嘗試類似的時候,通常GHC會吼我Type synonym ‘Baz’ should have 1 argument, but has been given none

現在,不要誤解我的意思:我真的很想寫這個,很容易看到它在這個特定的例子中如何工作(簡單的內聯WithBar會產生簽名naim :: (Foo u, Bar u ~()) => IO u,這當然罰款),但我不明白爲什麼它實際上就像這樣工作。這可能只是ghc-7.8.2中的一個漏洞,允許這麼做嗎?

+0

此行爲由[LiberalTypeSynonyms](https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/data-type-extensions.html#type-synonyms)啓用。特別是,在啓用它的情況下,編譯器會在檢查部分應用的類型同義詞之前展開所有類型同義詞。我猜猜,TypeFamilies或ContraintKinds中的一個意味着LiberalTypeSynonyms。 – user2407038 2015-04-05 22:36:43

+0

@ user2407038奇怪的是,它們並不意味着它。 – 2015-04-05 22:39:31

回答

4

我不知道官方的規則是什麼,但這種事情似乎是合理的,在最左邊最外層的同義詞擴展策略的基礎上工作。唯一重要的是,類型同義詞可以在其他類型檢測發生之前以單獨的終止階段處理。我不知道是否有意將部分應用類型同義詞F用作另一個類型同義詞G的參數,只要G確保F接收其缺少的參數,但這肯定與類型同義詞的想法一致是一個淺顯的方便。

3

部分申請應該LiberalTypeSynonyms擴展啓用。

基本上這推遲了類型同義詞的大多數一致性檢查,直到它們被擴展,所以你的「內聯」解釋本質上是正確的想法。

這裏的奇怪之處在於,這個擴展名是而不是在模塊中隱含的意思。我剛剛測試過,部分應用程序通常不起作用,只有ConstraintKinds,TypeFamiliesPolyKinds。 (我加了後者,因爲種類在擴展前檢查過,否則我的測試類型推斷出錯誤的類型)。

儘管如此,GHCi 7.8.3中的文件加載正常。也許這某種錯誤,即使有一個擴展使其合法。

8

你的文件編譯的GHC 7.8,但在GHC 7.10我得到一個錯誤:

Type synonym ‘Baz’ should have 1 argument, but has been given none

In the type signature for ‘naim’: naim :: WithBar() Baz u => IO u

添加-XLiberalTypeSynonyms修正錯誤。因此,這是7.8中的一個錯誤。

相關問題