Rank2Types의 목적은 무엇입니까?

Rank2Types의 목적은 무엇입니까?

---

저는 Haskell에 능숙하지 않으므로 이것은 매우 쉬운 질문 일 수 있습니다.

Rank2Types 는 어떤 언어 제한을 해결합니까? Haskell의 함수가 이미 다형성 인수를 지원하지 않습니까?

---

Haskell의 함수가 이미 다형성 인수를 지원하지 않습니까?

이 확장 기능없이 다른 유형의 인수를 취하는 함수를 작성할 수는 있지만 동일한 호출에서 인수를 다른 유형으로 사용하는 함수를 작성할 수는 없습니다.

예를 들어 다음 함수는 g의 정의에서 다른 인수 유형과 함께 사용 되기 때문에이 확장없이 입력 할 수 없습니다 f.

f g = g 1 + g "lala"

다형성 함수를 다른 함수의 인수로 전달하는 것은 완벽하게 가능합니다. 그래서 같은 map id ["a","b","c"]것은 완벽하게 합법적입니다. 그러나 함수는 단형으로 만 사용할 수 있습니다. 예제 map에서는 id유형이있는 것처럼 사용 합니다 String -> String. 물론 id. 대신 주어진 유형의 단순한 단 형성 함수를 전달할 수도 있습니다 . rank2types가 없으면 함수가 인수가 다형성 함수 여야하므로 다형성 함수로 사용할 방법이 없습니다.

---

시스템 F를 직접 공부하지 않으면 상위 다형성을 이해하기 어렵습니다. 하스켈은 단순성을 위해 세부 사항을 숨기도록 설계 되었기 때문입니다.

하지만 기본적으로 대략적인 생각은 다형성 유형이 a -> bHaskell에서하는 것과 같은 형태가 아니라는 것입니다. 실제로는 다음과 같이 항상 명시 적 수량자를 사용합니다.

id :: ∀a.a → a
id = Λt.λx:t.x

"∀"기호를 모르면 "for all"로 읽습니다. ∀x.dog(x)"모든 x에 대해 x는 개"를 의미합니다. "Λ"는 대문자 람다로, 유형 매개 변수를 추상화하는 데 사용됩니다. 두 번째 줄이 말하는 것은 id는 type을 취한 t다음 해당 유형에 의해 매개 변수화 된 함수를 반환하는 함수라는 것입니다.

시스템 F에서는 이와 같은 함수 id를 값에 바로 적용 할 수 없습니다 . 먼저 값에 적용하는 λ- 함수를 얻으려면 Λ- 함수를 유형에 적용해야합니다. 예를 들면 :

(Λt.λx:t.x) Int 5 = (λx:Int.x) 5
                  = 5

Standard Haskell (즉, Haskell 98 및 2010)은 이러한 유형 한정자, 대문자 람다 및 유형 응용 프로그램을 사용하지 않음으로써이를 단순화하지만 GHC는 컴파일을 위해 프로그램을 분석 할 때이를 적용합니다. (이것은 런타임 오버 헤드가없는 모든 컴파일 타임 항목입니다.)

그러나 Haskell의 자동 처리는 "∀"이 함수 ( "→") 유형의 왼쪽 분기에 나타나지 않는다고 가정 함을 의미합니다. Rank2Types및 RankNTypes그 제한을 해제하고 삽입하는 위치에 대한 하스켈의 기본 규칙을 재정의 할 수 있습니다 forall.

왜 이렇게 하시겠습니까? 완전하고 제한되지 않은 System F는 정말 강력하고 멋진 일을 많이 할 수 있기 때문입니다. 예를 들어, 유형 숨김 및 모듈성은 상위 유형을 사용하여 구현할 수 있습니다. 예를 들어 다음 랭크 -1 유형 (장면을 설정하기 위해)의 평범한 이전 함수를 살펴보십시오.

f :: ∀r.∀a.((a → r) → a → r) → r

를 사용하려면 f먼저 호출자가 r및 에 사용할 유형을 a선택한 다음 결과 유형의 인수를 제공해야합니다. 그래서 당신은 선택할 수 r = Int및 a = String:

f Int String :: ((String → Int) → String → Int) → Int

그러나 이제 다음과 같은 상위 유형과 비교하십시오.

f' :: ∀r.(∀a.(a → r) → a → r) → r

이 유형의 기능은 어떻게 작동합니까? 글쎄, 그것을 사용하려면 먼저 사용할 유형을 지정하십시오 r. 우리가 선택 말 Int:

f' Int :: (∀a.(a → Int) → a → Int) → Int

하지만 지금은이 ∀a입니다 내부 는 어떤 유형에 사용할 선택할 수 있도록 기능 화살표 a; f' Int적절한 유형의 Λ- 기능에 지원해야합니다 . 이는 의 구현이 의 호출자가 아닌 f'사용할 유형을 선택해야af' 함을 의미합니다 . 상위 유형이 없으면 반대로 호출자는 항상 유형을 선택합니다.

이것은 무엇에 유용합니까? 글쎄요, 실제로 많은 것들에 대해,하지만 한 가지 아이디어는 이것을 사용하여 객체 지향 프로그래밍과 같은 것을 모델링 할 수 있다는 것입니다. 여기서 "객체"는 숨겨진 데이터에 대해 작동하는 몇 가지 방법과 함께 숨겨진 데이터를 묶습니다. 예를 들어, 하나는 an을 반환 Int하고 다른 하나 는 a를 반환하는 두 개의 메서드가있는 객체 String를 다음 유형으로 구현할 수 있습니다.

myObject :: ∀r.(∀a.(a → Int, a -> String) → a → r) → r

어떻게 작동합니까? 개체는 숨겨진 유형의 내부 데이터가있는 함수로 구현됩니다 a. 객체를 실제로 사용하기 위해 클라이언트는 객체가 두 메서드로 호출 할 "콜백"함수를 전달합니다. 예를 들면 :

myObject String (Λa. λ(length, name):(a → Int, a → String). λobjData:a. name objData)

여기서 우리는 기본적으로 객체의 두 번째 메소드를 호출합니다 . 유형은 a → Stringunknown에 대한 것 a입니다. myObject의 고객 에게는 알려지지 않았습니다 . 그러나 이러한 클라이언트는 서명을 통해 두 가지 기능 중 하나를 적용 할 수 Int있고 String.

실제 Haskell 예제를 위해 아래는 제가 스스로 가르쳤을 때 작성한 코드입니다 RankNTypes. 이것은 ShowBox숨겨진 유형의 값을 Show클래스 인스턴스 와 함께 묶는 라는 유형을 구현 합니다. 맨 아래의 예에서 ShowBox첫 번째 요소는 숫자로, 두 번째 요소는 문자열로 만든 목록을 만듭니다 . 상위 유형을 사용하여 유형을 숨기므로 유형 검사를 위반하지 않습니다.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}

type ShowBox = forall b. (forall a. Show a => a -> b) -> b

mkShowBox :: Show a => a -> ShowBox
mkShowBox x = \k -> k x

-- | This is the key function for using a 'ShowBox'.  You pass in
-- a function @k@ that will be applied to the contents of the 
-- ShowBox.  But you don't pick the type of @k@'s argument--the 
-- ShowBox does.  However, it's restricted to picking a type that
-- implements @Show@, so you know that whatever type it picks, you
-- can use the 'show' function.
runShowBox :: forall b. (forall a. Show a => a -> b) -> ShowBox -> b
-- Expanded type:
--
--     runShowBox 
--         :: forall b. (forall a. Show a => a -> b) 
--                   -> (forall b. (forall a. Show a => a -> b) -> b)
--                   -> b
--
runShowBox k box = box k


example :: [ShowBox] 
-- example :: [ShowBox] expands to this:
--
--     example :: [forall b. (forall a. Show a => a -> b) -> b]
--
-- Without the annotation the compiler infers the following, which
-- breaks in the definition of 'result' below:
--
--     example :: forall b. [(forall a. Show a => a -> b) -> b]
--
example = [mkShowBox 5, mkShowBox "foo"]

result :: [String]
result = map (runShowBox show) example

추신 : ExistentialTypesGHC가 어떻게 사용 하는지 궁금해하는이 글을 읽는 모든 사람에게 forall그 이유는이면에서 이런 종류의 기술을 사용하기 때문이라고 생각합니다.

---

Luis Casillas's answer gives a lot of great info about what rank 2 types mean, but I'll just expand on one point he didn't cover. Requiring an argument to be polymorphic doesn't just allow it to be used with multiple types; it also restricts what that function can do with its argument(s) and how it can produce its result. That is, it gives the caller less flexibility. Why would you want to do that? I'll start with a simple example:

Suppose we have a data type

data Country = BigEnemy | MediumEnemy | PunyEnemy | TradePartner | Ally | BestAlly

and we want to write a function

f g = launchMissilesAt $ g [BigEnemy, MediumEnemy, PunyEnemy]

that takes a function that's supposed to choose one of the elements of the list it's given and return an IO action launching missiles at that target. We could give f a simple type:

f :: ([Country] -> Country) -> IO ()

The problem is that we could accidentally run

f (\_ -> BestAlly)

and then we'd be in big trouble! Giving f a rank 1 polymorphic type

f :: ([a] -> a) -> IO ()

doesn't help at all, because we choose the type a when we call f, and we just specialize it to Country and use our malicious \_ -> BestAlly again. The solution is to use a rank 2 type:

f :: (forall a . [a] -> a) -> IO ()

Now the function we pass in is required to be polymorphic, so \_ -> BestAlly won't type check! In fact, no function returning an element not in the list it is given will typecheck (although some functions that go into infinite loops or produce errors and therefore never return will do so).

The above is contrived, of course, but a variation on this technique is key to making the ST monad safe.

---

Higher-rank types aren't as exotic as the other answers have made out. Believe it or not, many object-oriented languages (including Java and C#!) feature them. (Of course, no one in those communities knows them by the scary-sounding name "higher-rank types".)

The example I'm going to give is a textbook implementation of the Visitor pattern, which I use all the time in my daily work. This answer is not intended as an introduction to the visitor pattern; that knowledge is readily available elsewhere.

In this fatuous imaginary HR application, we wish to operate on employees who may be full-time permanent staff or temporary contractors. My preferred variant of the Visitor pattern (and indeed the one which is relevant to RankNTypes) parameterises the visitor's return type.

interface IEmployeeVisitor<T>
{
    T Visit(PermanentEmployee e);
    T Visit(Contractor c);
}

class XmlVisitor : IEmployeeVisitor<string> { /* ... */ }
class PaymentCalculator : IEmployeeVisitor<int> { /* ... */ }

The point is that a number of visitors with different return types can all operate on the same data. This means IEmployee must express no opinion as to what T ought to be.

interface IEmployee
{
    T Accept<T>(IEmployeeVisitor<T> v);
}
class PermanentEmployee : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}
class Contractor : IEmployee
{
    // ...
    public T Accept<T>(IEmployeeVisitor<T> v)
    {
        return v.Visit(this);
    }
}

I wish to draw your attention to the types. Observe that IEmployeeVisitor universally quantifies its return type, whereas IEmployee quantifies it inside its Accept method - that is to say, at a higher rank. Translating clunkily from C# to Haskell:

data IEmployeeVisitor r = IEmployeeVisitor {
    visitPermanent :: PermanentEmployee -> r,
    visitContractor :: Contractor -> r
}

newtype IEmployee = IEmployee {
    accept :: forall r. IEmployeeVisitor r -> r
}

So there you have it. Higher-rank types show up in C# when you write types containing generic methods.

---

Slides from Bryan O'Sullivan's Haskell course at Stanford helped me understand Rank2Types.

---

For those familiar with object oriented languages, a higher-rank function is simply a generic function that expects as its argument another generic function.

E.g. in TypeScript you could write:

type WithId<T> = T & { id: number }
type Identifier = <T>(obj: T) => WithId<T>
type Identify = <TObj>(obj: TObj, f: Identifier) => WithId<TObj>

See how the generic function type Identify demands a generic function of the type Identifier? This makes Identify a higher-rank function.

참고URL : https://stackoverflow.com/questions/12031878/what-is-the-purpose-of-rank2types