What's the theoretical basis for existential types?
The Haskell Wiki does a good job of explaining how to use existential types, but I don't quite grok the theory behind them.
Consider this example of an existential type:
data S = forall a. Show a => S a -- (1)
to define a type wrapper for things that we can convert to a String . The wiki mentions that what we really want to define is a type like
data S = S (exists a. Show a => a) -- (2)
ie a true "existential" type - loosely I think of this as saying "the data constructor S takes any type for which a Show instance exists and wraps it". In fact, you could probably write a GADT as follows:
data S where -- (3)
S :: Show a => a -> S
I haven't tried compiling that, but it seems as though it should work. To me, the GADT is obviously equivalent to the code (2) that we'd like to write.
However, it's completely not obvious to me why (1) is equivalent to (2). Why does moving the data constructor to the outside turn the forall into an exists ?
The closest thing I can think of are De Morgan's Laws in logic, where interchanging the order of a negation and a quantifier turns existential quantifiers into universal quantifiers, and vice-versa:
¬(∀x. px) ⇔ ∃x. ¬(px)
but data constructors seem to be a totally different beast to the negation operator.
What is the theory that lies behind the ability to define existential types using forall instead of the non-existent exists ?
First of all, take a look at the "Curry Howard correspondence" which states that the types in a computer program correspond to formulas in intuitionistic logic. Intuitionistic logic is just like the "regular" logic you learned in school but without the law of the excluded middle or double negation elimination:
Not an axiom: P ⇔ ¬¬P (but P ⇒ ¬¬P is fine)
Not an axiom: P ∨ ¬P
Laws of logic
You are on the right track with DeMorgan's laws, but first we are going to use them to derive some new ones. The relevant version of DeMorgan's laws are:
We can derive (∀x. P ⇒ Q(x)) = P ⇒ (∀x. Q(x)):
And (∀x. Q(x) ⇒ P) = (∃x. Q(x)) ⇒ P (this one is used below):
Note that these laws hold in intuitionistic logic as well. The two laws we derived are cited in the paper below.
Simple Types
The simplest types are easy to work with. For example:
data T = Con Int | Nil
The constructors and accessors have the following type signatures:
Con :: Int -> T
Nil :: T
unCon :: T -> Int
unCon (Con x) = x
Type Constructors
Now let's tackle type constructors. Take the following data definition:
data T a = Con a | Nil
This creates two constructors,
Con :: a -> T a
Nil :: T a
Of course, in Haskell, type variables are implicitly universally quantified, so these are really:
Con :: ∀a. a -> T a
Nil :: ∀a. T a
And the accessor is similarly easy:
unCon :: ∀a. T a -> a
unCon (Con x) = x
Quantified types
Let's add the existential quantifier, ∃, to our original type (the first one, without the type constructor). Rather than introducing it in the type definition, which doesn't look like logic, introduce it in the constructor / accessor definitions, which do look like logic. We'll fix the data definition later to match.
Instead of Int , we will now use ∃x. t ∃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 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 (eg 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.
链接地址: http://www.djcxy.com/p/43442.html上一篇: 为什么GHC不能为Monoid派生实例？
下一篇: 存在类型的理论基础是什么？