fun g x = ys where ys = [x] ++ filter (curry g x) ysの型が である理由を理解しようとしてい((a, a) -> Bool) -> a -> [a]ます。
という事は承知しています：
filter :: (a -> Bool) -> [a] -> [a]そしてそれcurry :: ((a, b) -> c) -> a -> b -> c
しかし、私は続行する方法を理解していません。
2 に答える
7
以下のアプローチは、必ずしも最も簡単または最速というわけではありませんが、比較的体系的です。
厳密に言えば、あなたはのタイプを探しています
\g -> (\ x -> let ys = (++) [x] (filter (curry g x) ys) in ys)
(letとwhereは同等ですが、 を使用した方が推論しやすい場合がありletます)、型を考えると
filter :: (a -> Bool) -> [a] -> [a]
curry :: ((a, b) -> c) -> a -> b -> c
も使用していることを忘れないでください
(++) :: [a] -> [a] -> [a]
まず、構文ツリーの「最も深い」部分を見てみましょう。
curry g x
と がgありxますが、これまでに見たことがないので、何らかの型があると仮定します。
g :: t1
x :: t2
もありますcurry。これらの関数が発生するすべてのポイントで、型変数 ( a、b、c) を異なる方法で特殊化できるため、これらの関数を使用するたびに新しい名前に置き換えることをお勧めします。この時点でcurry、次の型があります。
curry :: ((a1, b1) -> c1) -> a1 -> b1 -> c1
curry g xその場合、次のタイプを統合できるかどうかしかわかりません。
t1 ~ ((a1, b1) -> c1) -- because we apply curry to g
t2 ~ a1 -- because we apply (curry g) to x
その場合、次のように仮定しても安全です。
g :: ((a1, b1) -> c1)
x :: a1
---
curry g x :: b1 -> c1
続けましょう：
filter (curry g x) ys
ys初めて見るので、とりあえずそのままにしておきましょうys :: t3。もインスタンス化する必要がありますfilter。この時点で、
filter :: (a2 -> Bool) -> [a2] -> [a2]
ys :: t3
ここで、filterの引数の型を一致させる必要があります。
b1 -> c1 ~ a2 -> Bool
t3 ~ [a2]
最初の制約は次のように分解できます。
b1 ~ a2
c1 ~ Bool
現在、次のことがわかっています。
g :: ((a1, a2) -> Bool)
x :: a1
ys :: [a2]
---
filter (curry g x) ys :: [a2]
続けましょう。
(++) [x] (filter (curry g x) ys)
の説明にはあまり時間をかけません。[x] :: [a1]のタイプを見てみましょう(++)。
(++) :: [a3] -> [a3] -> [a3]
次の制約が得られます。
[a1] ~ [a3] -- [x]
[a2] ~ [a3] -- filter (curry g x) ys
これらの制約は次のように削減できるため、
a1 ~ a3
a2 ~ a2
aこれらすべてをと呼びますa1:
g :: ((a1, a1) -> Bool)
x :: a1
ys :: [a1]
---
(++) [x] (filter (curry g x) ys) :: [a1]
ys今のところ、型が一般化されることは無視して、
\x -> let { {- ... -} } in ys
に必要な型とxの型がわかっているysので、これでわかります
g :: ((a1, a1) -> Bool)
ys :: [a1]
---
(\x -> let { {- ... -} } in ys) :: a1 -> [a1]
同様に、次のように結論付けることができます。
(\g -> (\x -> let { {- ... -} } in ys)) :: ((a1, a1) -> Bool) -> a1 -> [a1]
この時点で、型変数の名前を変更するだけで (実際には、バインドしたいので一般化しますfun)、答えが得られます。
于 2014-04-26T20:41:28.317 に答える
4
次の一般的なスキームを使用して、多かれ少なかれ機械的な方法で Haskell の型を派生させることができます。
foo x = y -- is the same as
foo = \x -> y -- so the types are
foo :: a -> b , x :: a , y :: b -- so that
foo x :: b
つまり、例えば
f x y z :: d , x :: a , y :: b, z :: c
伴う
f x y :: c -> d
f x :: b -> c -> d
f :: a -> b -> c -> d
これらの単純なトリックを使用すると、型の派生は簡単になります。ここで、
filter :: (a -> Bool) -> [a] -> [a]
curry :: ((a, b) -> c) -> a -> b -> c
(++) :: [a] -> [a] -> [a]
慎重に並べたものを書き留め、トップダウン方式で処理し、一貫して型変数の名前を変更して置換し、型の等価性を横に記録します。
fun g x = ys where ys = [x] ++ filter (curry g x) ys
fun g x :: c , ys :: c
fun g :: b -> c , x :: b
fun :: a -> b -> c , g :: a
ys = [x] ++ フィルター (カレー gx) ys c ~ c (++) [x] (フィルター (カレー gx) ys) :: c (++) :: [a1] -> [a1] -> [a1] ----------------------------------------------- (++) :: [b] -> [b] -> [b] , a1 ~ b , c ~ [b] filter (カレー gx ) ys :: [b] filter :: (a2 -> Bool) -> [a2] -> [a2] , a2 ~ b -------------------------------------- フィルター :: (b -> ブール) -> [b] -> [b] カレー g x :: b -> ブール カレー :: ((a3, b) -> c3 ) -> a3 -> b -> c3 , c3 ~ Bool , a3 ~ b ------------------------------------------- カレー :: ((b , b) -> Bool) -> b -> b -> Bool , a ~ ((b,b) -> Bool)
とがa ~ ((b,b) -> Bool)ありc ~ [b]、したがって
fun :: a -> b -> c
fun :: ((b,b) -> Bool) -> b -> [b]
((a,a) -> Bool) -> a -> [a]これは、型変数の一貫した名前変更までは と同じです。
于 2014-04-26T21:40:14.207 に答える