실존 적 유형의 이론적 근거는 무엇입니까?

실존 적 유형의 이론적 근거는 무엇입니까?

---

하스켈 위키는 어떻게 존재 형식을 사용하는 설명의 좋은 일을하지만, 꽤 그들 뒤에 이론을 grok 수 없습니다.

다음 실존 유형의 예를 고려하십시오.

data S = forall a. Show a => S a      -- (1)

로 변환 할 수있는 것에 대한 유형 래퍼를 정의합니다 String. 위키는 우리가 정말로 정의하고 싶은 것이 다음과 같은 유형 이라고 언급합니다.

data S = S (exists a. Show a => a)    -- (2)

즉, 진정한 "존재 적"유형-느슨하게 "데이터 생성자 S는 Show인스턴스 가 존재 하는 모든 유형을 가져와 이를 래핑"한다고 생각합니다. 실제로 다음과 같이 GADT를 작성할 수 있습니다.

data S where                          -- (3)
    S :: Show a => a -> S

나는 그것을 컴파일하려고 시도하지 않았지만 작동 해야하는 것처럼 보입니다. 나에게 GADT는 분명히 우리가 작성하려는 코드 (2)와 동일합니다.

그러나 (1)이 (2)와 동등한 이유는 나에게 완전히 분명하지 않습니다. 데이터 생성자를 외부로 이동하면 왜 forall으로 바뀝니 exists까?

내가 생각할 수있는 가장 가까운 것은 논리에서 De Morgan의 법칙 입니다. 여기서 부정과 수량 자의 순서를 바꾸면 실존 적 수량자를 보편적 수량 자로 바꾸고 그 반대도 마찬가지입니다.

¬(∀x. px) ⇔ ∃x. ¬(px)

그러나 데이터 생성자는 부정 연산자와는 완전히 다른 짐승처럼 보입니다.

존재하지 않는 forall대신 사용하여 존재 유형을 정의하는 능력 뒤에 놓여있는 이론은 무엇입니까 exists?

---

우선, 컴퓨터 프로그램의 유형이 직관 논리의 공식과 일치 함을 나타내는 "Curry Howard 대응"을 살펴보십시오. 직관적 논리는 학교에서 배운 "일반적인"논리와 같지만 중간 또는 이중 부정 제거의 법칙이 없습니다.

• 공리 아님 : P ⇔ ¬¬P (그러나 P ⇒ ¬¬P는 괜찮음)

• 공리가 아님 : P ∨ ¬P

논리의 법칙

당신은 DeMorgan의 법칙에 따라 올바른 길을 가고 있지만 먼저 우리는 그것들을 사용하여 새로운 법칙을 도출 할 것입니다. DeMorgan 법률의 관련 버전은 다음과 같습니다.

• ∀x. P (x) = ¬∃x. ¬P (x)
• ∃x. P (x) = ¬∀x. ¬P (x)

(∀x. P ⇒ Q (x)) = P ⇒ (∀x. Q (x)) :

1. (∀x. P ⇒ Q (x))
2. (∀x. ¬P ∨ Q (x))
3. ¬P ∨ (∀x. Q (x))
4. P ⇒ (∀x. Q)

그리고 (∀x. Q (x) ⇒ P) = (∃x. Q (x)) ⇒ P (이것은 아래에서 사용됩니다) :

1. (∀x. Q (x) ⇒ P)
2. (∀x. ¬Q (x) ∨ P)
3. (¬¬∀x.¬Q (x)) ∨P
4. (¬∃x.Q (x)) ∨P
5. (∃x. Q (x)) ⇒ P

이러한 법칙은 직관적 논리에도 적용됩니다. 우리가 도출 한 두 가지 법칙은 아래 논문에 인용되어 있습니다.

간단한 유형

가장 간단한 유형은 작업하기 쉽습니다. 예를 들면 :

data T = Con Int | Nil

생성자 및 접근 자에는 다음과 같은 형식 서명이 있습니다.

Con :: Int -> T
Nil :: T

unCon :: T -> Int
unCon (Con x) = x

유형 생성자

이제 유형 생성자를 다루겠습니다. 다음 데이터 정의를 사용하십시오.

data T a = Con a | Nil

이렇게하면 두 개의 생성자가 생성됩니다.

Con :: a -> T a
Nil :: T a

물론 Haskell에서 형식 변수는 암시 적으로 보편적으로 정량화되므로 실제로는 다음과 같습니다.

Con :: ∀a. a -> T a
Nil :: ∀a. T a

접근자는 비슷하게 쉽습니다.

unCon :: ∀a. T a -> a
unCon (Con x) = x

정량화 된 유형

원래 유형 (유형 생성자가없는 첫 번째 유형)에 존재 한정자 ∃를 추가해 보겠습니다. 로직처럼 보이지 않는 타입 정의에 도입하는 대신 로직처럼 보이는 생성자 / 접근 자 정의에 도입하십시오. 나중에 일치하도록 데이터 정의를 수정합니다.

Instead of Int, we will now use ∃x. t. Here, t is some kind of type expression.

Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)

Based on the rules of logic (the second rule above), we can rewrite the type of Con to:

Con :: ∀x. t -> T

When we moved the existential quantifier to the outside (prenex form), it turned into a universal quantifier.

So the following are theoretically equivalent:

data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil

Except there is no syntax for exists in Haskell.

In non-intuitionistic logic, it is permissible to derive the following from the type of unCon:

unCon :: ∃ T -> t -- invalid!

The reason this is invalid is because such a transformation is not permitted in intuitionistic logic. So it is impossible to write the type for unCon without an exists keyword, and it is impossible to put the type signature in prenex form. It's hard to make a type checker guaranteed to terminate in such conditions, which is why Haskell doesn't support arbitrary existential quantifiers.

Sources

"First-class Polymorphism with Type Inference", Mark P. Jones, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (web)

---

Plotkin and Mitchell established a semantics for existential types, in their famous paper, which made the connection between abstract types in programming languages and existential types in logic,

Mitchell, John C.; Plotkin, Gordon D.; Abstract Types Have Existential Type, ACM Transactions on Programming Languages and Systems, Vol. 10, No. 3, July 1988, pp. 470–502

At a high level,

Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite “value” we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.

---

It's stated in the haskell wiki article you linked. I'll borrow some lines of code and comments from it and try to explain.

data T = forall a. MkT a

Here you have a type T with a type constructor MkT :: forall a. a -> T, right? MkT is (roughly) a function, so for every possible type a, the function MkT have type a -> T. So, we agree that by using that constructor we may build values like [MkT 1, MkT 'c', MkT "hello"], all of them of type T.

foo (MkT x) = ... -- what is the type of x?

But what does happen when you try to extract (e.g. via pattern matching) the value wrapped within a T? Its type annotation only says T, without any reference to the type of the value actually contained in it. We can only agree on the fact that, whatever it is, it will have one (and only one) type; how can we state this in Haskell?

x :: exists a. a

This simply says that there exists a type a to which x belongs. At this point it should be clear that, by removing the forall a from MkT's definition and by explicitly specifying the type of the wrapped value (that is exists a. a), we are able to achieve the same result.

data T = MkT (exists a. a)

The bottom line is the same also if you add conditions on implemented typeclasses as in your examples.

참고URL : https://stackoverflow.com/questions/10753073/whats-the-theoretical-basis-for-existential-types