[haskell] 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

표준 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그 이유가이면에서 이런 종류의 기술을 사용하기 때문이라고 생각합니다.

답변

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

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

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

f (\_ -> BestAlly)

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

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

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

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

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);
    }
}

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

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

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