27

ランク2のポリモーフィズム（最も顕著な例はSTモナド）のユースケースをいくつか見てきましたが、それより高いランクのユースケースはありません。誰かがそのようなユースケースを知っていますか？

4

2 に答える 2

30

そのような獣は必然的に少し関与していますが、私は助けることができるかもしれません。これは、バインディングとde Bruijnインデックスを使用して、範囲の広い構文を開発する際に時々使用するパターンです。

mkRenSub ::
  forall v t x y.                      -- variables represented by v, terms by t
    (forall x. v x -> t x) ->            -- how to embed variables into terms
    (forall x. v x -> v (Maybe x)) ->    -- how to shift variables
    (forall i x y.                       -- for thingies, i, how to traverse terms...
      (forall z. v z -> i z) ->              -- how to make a thingy from a variable
      (forall z. i z -> t z) ->              -- how to make a term from a thingy
      (forall z. i z -> i (Maybe z)) ->      -- how to weaken a thingy
      (v x -> i y) ->                    -- ...turning variables into thingies
      t x -> t y) ->                     -- wherever they appear
    ((v x -> v y) -> t x -> t y, (v x -> t y) -> t x -> t y)
                                                 -- acquire renaming and substitution
mkRenSub var weak mangle = (ren, sub) where
  ren = mangle id var weak         -- take thingies to be vars to get renaming
  sub = mangle var id (ren weak)   -- take thingies to be terms to get substitution

通常、私は型クラスを使用して最悪のマチを隠しますが、辞書を解凍すると、これが見つかります。

重要なのはmangle、ランク2の操作であり、それらが機能する変数セットに多形性の適切な操作を備えたものの概念を取ります。変数を物にマップする操作は、項変換器に変換されます。全体はmangle、名前変更と置換の両方を生成するために使用する方法を示しています。

そのパターンの具体的な例を次に示します。

data Id x = Id x

data Tm x
  = Var (Id x)
  | App (Tm x) (Tm x)
  | Lam (Tm (Maybe x))

tmMangle :: forall i x y.
             (forall z. Id z -> i z) ->
             (forall z. i z -> Tm z) ->
             (forall z. i z -> i (Maybe z)) ->
             (Id x -> i y) -> Tm x -> Tm y
tmMangle v t w f (Var i) = t (f i)
tmMangle v t w f (App m n) = App (tmMangle v t w f m) (tmMangle v t w f n)
tmMangle v t w f (Lam m) = Lam (tmMangle v t w g m) where
  g (Id Nothing) = v (Id Nothing)
  g (Id (Just x)) = w (f (Id x))

subst :: (Id x -> Tm y) -> Tm x -> Tm y
subst = snd (mkRenSub Var (\ (Id x) -> Id (Just x)) tmMangle)

トラバーサルという用語を一度だけ実装しますが、非常に一般的な方法で、mkRenSubパターン（2つの異なる方法で一般的なトラバーサルを使用する）をデプロイすることで置換を取得します。

別の例として、型演算子間の多項演算について考えてみます。

type (f :-> g) = forall x. f x -> g x

（IMonadインデックス付きモナド）はm :: (* -> *) -> * -> *、多形演算子を備えたものです

ireturn :: forall p. p :-> m p
iextend :: forall p q. (p :-> m q) -> m p :-> m q

したがって、これらの操作はランク2です。

これで、任意のインデックス付きモナドによってパラメーター化された操作はランク3になります。したがって、たとえば、通常のモナド構成を構築すると、

compose :: forall m p q r. IMonad m => (q :-> m r) -> (p :-> m q) -> p :-> m r
compose qr pq = iextend qr . pq

の定義をアンパックすると、ランク3の定量化に依存しますIMonad。

話の教訓：ポリモーフィック/インデックス付きの概念に対して高次のプログラミングを行うと、有用なキットの辞書はランク2になり、ジェネリックプログラムはランク3になります。もちろん、これは再び発生する可能性のあるエスカレーションです。

于 2011-12-06T21:10:18.573 に答える
9

おそらく、私がこれまで読んだ要約の最良の結末は、「マルチプレートは、Haskellの通常の型クラスメカニズムに加えて、ランク3のポリモーフィズムのみを必要とする」というものです。。（ああ、ランク3のポリモーフィズムだけで、大したことはありません！）

于 2011-12-07T01:08:43.793 に答える