型チェッカーを満足させるために関数型を "ラップする"必要があるのはなぜですか？

Question

プログラムタイプチェックを次

{-# 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と をコンパイルすることは解決しない。）

Answer 1

これはGHCのタイプシステムの問題です。ところで、それは本当にGHCのタイプシステムです。 Haskell/MLのような言語の元の型システムは、ここで使用している擬似多形性だけでなく、上位の多形性もサポートしていません。

問題を確認するには、このタイプをチェックするには、タイプの任意の位置にforallをサポートする必要があります。タイプの正面では、束縛されていない（型推論を可能にする通常の制限）。一旦このエリアを離れると、推論は一般的に決めることができなくなります（ランクnの多形性以上の場合）。我々の場合、[test1, test2]のタイプは[forall a. Num a => a -> a]である必要があり、それは上記のスキームに適合しないと考えると問題である。 aの範囲がforallの型を越えているので、それが使用されている型に置き換えられる可能性があるので、忠実な多型を使用する必要があります。

したがって、問題が完全に解決できないという理由だけで間違いを犯すケースもあるでしょう。 GHCはランクnの多型性と忠実な多型のサポートをいくらかサポートしていますが、新しいタイプのラッパーを使用して信頼性の高い動作を得るのが一般的には良い方法です。私の知る限りでは、GHCはタイプ推論アルゴリズムが何を処理するかを正確に把握することが難しいため、この機能を正確に使用するのをやめてしまいます。

要約すると、mathには、薄片状のケースがあり、それに対処するには多少不満がある場合はラップトップが最適です。

Answer 2

型推論アルゴリズムは上位タイプ（->の左側に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とは異なり、多形型が割り当てられ、と明示されています。 fooに署名を付けることによって。

Funのようなラッパーnewtypeも同様の方法でGHCに指示し、fの多型を提供します。