ランク3（またはそれ以上）の多型の使用例？

Question

ランク2の多型（最も顕著な例はST monad）にはいくつかの使用例がありますが、それより上位のものはありません。誰もそのようなユースケースを知っていますか？

Answer 1

私は助けることができるかもしれませんが、そのような獣は必然的に少し複雑です。ここでは、バインディングと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つの異なる方法）。別の例として

、IMonad（インデックス付けモナド）

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

型事業者間の多型の動作を考える一部 m :: (* -> *) -> * -> *が多型演算子が装備されている

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

ので、これらの操作は、2

ランクであります

任意のインデックス付きモナドによってパラメータ化された操作はすべてランク3です。あなたがIMonadの定義を解凍した後の例では、通常のモナド構図を構築し、

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

は、ランク3定量化に依存しています。

多言語/索引付き概念で高次プログラミングをしたら、有用なキットの辞書はランク2になり、ジェネリックプログラムはランク3になります。これはもちろん起こりうるエスカレーションです再び。

Answer 2

おそらく、私がまだ読んでいる抽象的なものの中で最高の終わり："Multiplate only requires rank 3 polymorphism in addition to the normal type class mechanism of Haskell."。 （ああ、ランク3の多型のみ、大したことではありません）