9

私は、Rank2Types と RankNTypes を調べて、それらに慣れようとしてきました。しかし、以下が機能しない理由がわかりません。

g :: (forall a. forall b. a -> b) -> x -> y -> (u,v)
g p x y = (p x, p y)

この定義はコンパイラによって受け入れられますが、使用しようとすると失敗します。

ghci> g id 1 2

<interactive>:35:3:
    Couldn't match type `a' with `b'
      `a' is a rigid type variable bound by
          a type expected by the context: a -> b at <interactive>:35:1
      `b' is a rigid type variable bound by
          a type expected by the context: a -> b at <interactive>:35:1
    Expected type: a -> b
      Actual type: a -> a
    In the first argument of `g', namely `id'
    In the expression: g id 1 2

a->a期待される のタイプが受け入れられない理由を理解するのに苦労していa->bます。

4

2 に答える 2

10

すべてのタイプaとタイプbの関数は、タイプforall a. forall b. a -> bの値を取り、タイプaの値を生成できる必要がありますb。したがって、たとえば、を入れIntたり取り出したりできる必要がありStringます。

あなたが入れた場合、あなたはString抜け出すことができません-あなたはあなたが入れたのと同じタイプを取り戻すだけです。したがって、タイプではありません。実際、型クラスの制約がなければ、その型の完全な関数はあり得ません。idIntidforall a. forall b. a -> b

結局のところ、ConstraintKindsを使用して、やりたいことに近いことをすることができますが、書くのも使うのもきれいではありません。

アイデアは、、、gによって満たされる必要のある条件、およびとの間の関係、およびとの間の関係を指定する制約を使用xしてパラメーターy化することです。すべての場合にこれらすべての制約が必要なわけではないため、2つのダミー型クラス（1つは個々のパラメーターの制約用、もう1つは「関係制約」用）も導入し、制約が不要な制約として使用できるようにします（制約を自分で指定しないと、GHCは制約を推測できません）。uvxuyv

これをより明確にするためのいくつかの制約例：

  • id関数として渡す場合は、xと等しくなければならず、と等しくuなけれyばなりませんv。x、、または個別yに制約はありません。uv
  • を渡す場合show、xおよびyはとのインスタンスである必要がありShow、uとvはに等しくなければなりませんString。xanduまたはyandとの関係に制約はありませんv。
  • を渡すとread . show、xとyのインスタンスである必要がShowありu、のインスタンスでvある必要がありますRead。ここでも、それらの間の関係に制約はありません。
  • 型クラスがConvert a b where convert :: a -> bあり、を渡す場合、個々のパラメーターに制約convertは必要Convert x uありません。Convert y v

したがって、これを実装するコードは次のとおりです。

{-# LANGUAGE Rank2Types, ConstraintKinds, FlexibleInstances, MultiParamTypeClasses #-}

class Dummy a
instance Dummy a

class Dummy2 a b
instance Dummy2 a b

g :: forall c. forall d. forall e. forall x. forall y. forall u. forall v.
     (c x, c y, d u, d v, e x u, e y v) =>
     (forall a. forall b. (c a, d b, e a b) => a -> b) -> x -> y -> (u,v)
g p x y = (p x, p y)

そして、これがそれを使用する方法です：

show . read異なるタイプの数値を変換するために使用する：

> (g :: (Show x, Show y, Read u, Read v, Dummy2 x u, Dummy2 y v) => (forall a. forall b. (Show a, Read b, Dummy2 a b) => a -> b) -> x -> y -> (u,v)) (read . show) 1 2 :: (Double, Int)
(1.0,2)

使用id：

> (g :: (Dummy x, Dummy y, x~u, y~v) => (forall a. forall b. (Dummy a, Dummy b, a~b) => a -> b) -> x -> y -> (u,v)) id 1 2.0
(1,2.0)

使用show：

> (g :: (Show x, Show y, String~u, String~v, Dummy2 x u, Dummy2 x y) => (forall a. forall b. (Show a, String~b, Dummy2 a b) => a -> b) -> x -> y -> (u,v)) show 1 2.0
("1","2.0")

ご覧のとおり、g使用するたびに署名を指定する必要があるため、これはひどく冗長で読みにくいものです。これがないと、GHCに制約を正しく推測させることはできないと思います（または少なくとも方法がわかりません）。

于 2012-10-16T10:45:08.050 に答える
4

関数を見ると、forall a. forall b. a -> bそれは任意の型の値を取り、任意の型の値を返すことができることを意味します。そのような関数がそのような関数であると仮定すると、 f の戻り値の型は依然として多態的であるため、任意の関数または任意の関数にfフィードすることができますが、一方、戻り値の型に値を指定すると固定されます (同じ型になります)入力値）、したがってエラー。 f 1f "hello"id

于 2012-10-16T10:50:14.053 に答える