순위 3 (또는 그 이상) 다형성의 사용 사례?

Question

순위 2 다형성 (가장 눈에 띄는 예제는 ST monad)에 대한 몇 가지 사용 사례를 보았지만 그보다 높은 순위는 없습니다. 누구나 그런 유스 케이스를 알고 있습니까?

Answer 1

필자는 필연적으로 그러한 짐승이 관련되어 있지만 도움을 줄 수 있습니다. 여기에 바인딩 및 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 

일반적으로, 나는 고어의 최악을 숨기는 타입의 클래스를 사용하려고하지만이 사전 압축을 풀 경우, 이것은 당신이 찾을 것입니다. 용어 트랜스포머로 턴 온 동작 thingies 변수를 매핑 :

포인트 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 패턴 (배포하여 대체를 얻을 두 가지 다른 방법). 다른 예로서

는

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

그래서 그러한 조작은 랭크 2

이십니까

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

IMonad (인덱스 모나드는) 다형성 연산자 구비 일부 m :: (* -> *) -> * -> *이다 형 사업자 사이 다형성 동작을 고려

이제 임의의 색인 된 모나드로 매개 변수화 된 연산은 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 차원 다형성, 큰 문제가 아니야!)