爲什麼函數類型需要被「包裝」才能滿足類型檢查器？

下面的程序類型檢查：爲什麼函數類型需要被「包裝」才能滿足類型檢查器？

{-# LANGUAGE RankNTypes #-} 

import Numeric.AD (grad) 

newtype Fun = Fun (forall a. Num a => [a] -> a) 

test1 [u, v] = (v - (u * u * u)) 
test2 [u, v] = ((u * u) + (v * v) - 1) 

main = print $ fmap (\(Fun f) -> grad f [1,1]) [Fun test1, Fun test2]

但這個方案失敗：

main = print $ fmap (\f -> grad f [1,1]) [test1, test2]

隨着錯誤類型：

Grad.hs:13:33: error: 
    • Couldn't match type ‘Integer’ 
        with ‘Numeric.AD.Internal.Reverse.Reverse s Integer’ 
     Expected type: [Numeric.AD.Internal.Reverse.Reverse s Integer] 
        -> Numeric.AD.Internal.Reverse.Reverse s Integer 
     Actual type: [Integer] -> Integer 
    • In the first argument of ‘grad’, namely ‘f’ 
     In the expression: grad f [1, 1] 
     In the first argument of ‘fmap’, namely ‘(\ f -> grad f [1, 1])’

直觀，後者計劃看起來是正確的。畢竟，以下，表面上看似乎等價程序做的工作：

main = print $ [grad test1 [1,1], grad test2 [1,1]]

它看起來像在GHC的類型系統的限制。我想知道是什麼原因導致失敗，爲什麼存在此限制，以及除包裝函數（上面的每個Fun）之外的任何可能的解決方法。

（注：這是不是由單態的限制造成的;編譯與NoMonomorphismRestriction沒有幫助）

來源

2017-08-08 frasertweedale

難道這是可怕的單態嗎？ –

這不是單態限制。 – frasertweedale

這實際上是類型系統中的一個限制。失敗的程序需要對意想不到的類型進行正確的類型檢查（'[test1，test2] :: [forall a。...]'是不可預測的），這是[docs]（https：//downloads.haskell。 org /〜ghc/latest/docs/html/users_guide/glasgow_exts.html＃impredicative-polymorphism）聲稱，GHC只有「非常片狀的支持」。最好的解決方法是'newtype'包裝。或者，打開ImpredicativeTypes併爲程序的每個子項添加類型註釋，直到它被敲入。 – user2407038

這是GHC的類型系統的問題。順便說一下，它確實是GHC的類型系統; Haskell/ML like語言的原始類型系統不支持更高等級的多態性，更不用說impurious多態性，這正是我們在這裏使用的。

問題是，爲了打字檢查，我們需要在類型的任何位置支持forall。不僅在類型前面一直束縛（允許類型推斷的正常限制）。一旦你離開這個區域，類型推斷通常會變得不可判定（對於n級多態性和超越）。在我們的例子中，[test1, test2]的類型需要是[forall a. Num a => a -> a]，考慮到它不適合上面討論的方案，這是一個問題。這將需要我們使用impredicative多態性，所謂的，因爲a範圍內的類型與forall s在其中，因此a可以被它所使用的類型所取代。

因此，會出現一些不正當的情況，因爲問題不能完全解決。 GHC確實對rank n多態性有一定的支持，並且對implicitic polymorphism有點支持，但通常使用newtype包裝來獲得可靠的行爲通常會更好。據我所知，GHC也不贊成使用這個特性，因爲很難弄清楚類型推理算法會處理什麼。

綜上所述，math表示會有片狀的情況，newtype包裝紙是最好的，如果有些不滿意的方式，以應付它。

來源

2017-08-08 08:57:33 jozefg

「ImpredicativeTypes」實際上並未得到任何有意義的支持。 – dfeuer

類型推理算法（在->左邊那些forall）將不能推斷更高級別的類型。如果我沒有記錯的話，它就成爲不可判定的。無論如何，考慮這個代碼

foo f = (f True, f 'a')

它應該是什麼類型？我們可以有

foo :: (forall a. a -> a) -> (Bool, Char)

但是我們也可以有

foo :: (forall a. a -> Int) -> (Int, Int)

，或者對於任何類型的構造F :: * -> *

foo :: (forall a. a -> F a) -> (F Bool, F Char)

這裏，就我所看到的，我們無法找到一個主體類型 - 這是我們可以指定給foo的最普通類型。

如果不存在主體類型，類型推斷機制只能爲foo選擇次優類型，這可能會在稍後導致類型錯誤。這不好。相反，GHC依賴於一個Hindley-Milner風格類型推理引擎，它被大大擴展以覆蓋更高級的Haskell類型。與普通的Hindley-Milner不同，這種機制將分配f多態性類型，如果用戶明確要求，例如，通過給foo簽名。

使用像Fun這樣的包裝類型也會以類似的方式指示GHC，爲f提供多態類型。

來源

2017-08-08 08:56:27 chi

爲什麼函數類型需要被「包裝」才能滿足類型檢查器？

回答

相關問題