型アノテーションブレーク関数型

Question

Framesライブラリ（UnColumnとAllAreを定義する）でシングルトンを使用する関数f 'とwithSingを使用するラッパー関数について、次の宣言を考えてみましょう。

{-# LANGUAGE AllowAmbiguousTypes -#} 
import Frames 
import Data.Singletons.Prelude 

f' :: forall rs1 rs2 a. (AllAre a (UnColumn rs1), AllAre a (UnColumn rs2), Num a) 
     => SList rs1 -> SList rs2 -> Frame (Record rs1) -> Frame (Record rs2) -> Int 
f' = undefined 

f df1 df2 = withSing (withSing f') df1 df2 

これはうまくいくようです。しかし、型の注釈を追加すると、型のチェックに失敗し、エラーが推測できませんでした：(AllAre a0 (UnColumn rs1), AllAre a0 (UnColumn rs2))。

f :: (SingI rs1, SingI rs2, AllAre a (UnColumn rs2), AllAre a (UnColumn rs1), Num a) 
=> Frame (Record rs1) -> Frame (Record rs2) -> Int 
f df1 df2 = withSing (withSing f') df1 df2 

ことは、これがGHCiの（ウェル、Intero）によれば、正確推論型署名です。推測されたシグネチャに一致する明示的なシグネチャを追加することは、コードのセマンティクスには影響しません。親指の一般的なルールとして

Answer 1

、Haskellのプログラムに推論さ種類は、その意味を変更しない一致しますが、それは実際には一般的なケースでは保証されていない、明示的な型シグネチャを追加します。 （私はそれはしかし、Haskell98のトップレベルの定義のための保証であると信じています。）

最終的に、あなたの問題はHaskell98内のローカルな定義で発生することができますタイプの変数のスコープの問題の一種と大差ありません：

import Data.List 
sortImage :: Ord b => (a -> b) -> [a] -> [a] 
sortImage f = sortBy cmp 
    where cmp x y = compare (f x) (f y) 

cmpの推定タイプは、実質的に(Ord b) => a -> a -> Orderingです。あなたが書くことができ、その場合にはScopedTypeVariablesを、使用しない限り、あなたが戻って、外側の署名（特にfの種類）にaとbを結ぶことができないので、あなたは、しかし、この署名が明示することはできません。

sortImage :: forall a b . Ord b => (a -> b) -> [a] -> [a] 
sortImage f = sortBy cmp 
    where cmp :: a -> a -> Ordering 
     cmp x y = compare (f x) (f y) 

あなたが発見したように、この種の変数スコープの問題は、少なくともAllowAmbiguousTypesを有効にしてトップレベルの定義でも発生する可能性があります。

{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE AllowAmbiguousTypes #-} 

class D a b 
instance D Bool b 
instance D Int b 

strange :: D a b => a -> a 
strange = undefined 

-- stranger :: (D a b1, D a b) => a -> a 
stranger x = strange (strange x) 

私はコメントとしてstrangerの推論されたタイプを示している：ここで

は、私がAllowAmbiguousTypes延長上GHCのドキュメントから適応、同じ問題であると考えているものを示してシンプルな例です。あなたはそれが明示的に作るしようとすると、エラーになります：

• Could not deduce (D a b0) arising from a use of ‘strange’ from the context: (D a b2, D a b)

問題は、GHCがstrangerが外側strange :: D a b1 => a -> aためD a b1を満たす任意のa上と呼ばれ、またためD a bを満たすことができることを推測することができるということです内側strange :: D a b => a -> a。 a関係限りしかし

、あなたは、明示的にこのタイプの署名を作るためにstrangerの明示的な署名でb1とb変数間のリンクをしようとstrange通話の種類との関係が失われた場合、 bの仮説ではcmpの署名であり、sortImageの署名のaとbの署名は失われます。制約はさておき、strangeの種類がちょうどa -> aで、直接bを参照していない、ので、一人でScopedTypeVariablesを使用して

は、ここで問題を解決するには十分ではありません。

stranger :: forall a b1 b2 . (D a b1, D a b2) => a -> a 
stranger x = (strange :: a -> a) ((strange :: a -> a) x) 

をしかし、あなたはstrange通話の種類にb1とb2を結ぶことができません：だから、あなたが書くことができます。あなたはそれを行うにはTypeApplicationsが必要：

{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE AllowAmbiguousTypes #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TypeApplications #-} 

class D a b 
instance D Bool b 

strange :: forall a b . D a b => a -> a 
strange = id 

stranger :: forall a b1 b2 . (D a b1, D a b2) => a -> a 
stranger x = (strange @a @b1) (strange @a @b2 x) 

し、それは大丈夫チェックを入力して、あなたも呼び出すことができます。

> stranger False 
False 

を（やや驚くべきことである）任意の型注釈なし。あなたは、インスタンスを持っていた場合：

instance D Int Double 

しかし、その後、あなたはIntの上strangerに使用して明示的に指定する必要があるでしょう：

> stranger @_ @Double @Double (1 :: Int)