At 2000-11-24 02:02, Bernd =?iso-8859-2?Q?Holzm=FCller?= wrote:
When I got to know Haskell, I was expecting a construct for union types like:
data B = ... data C = ... type A = B | C | D -- A accepts values of either B or C or D (cf. the "Either a" type in the Prelude)
but this is not valid Haskell. Is there any reason for this restriction in the Haskell type system?
My understanding is that every value in Haskell is a member of exactly one type. Well, that's not exactly true: it might be better to say that every Haskell value represents a set of 'items', each of which has exactly one fully-specified type (i.e. a type with no free type-variables). For instance, in such definitions as data Maybe a = Nothing | Just a the value that the constructor 'Nothing' gives has type 'Maybe a', which represents a set of 'items' that have such types as 'Maybe Boolean', 'Maybe String' etc. This rules out union types and OOP-style polymorphism. It also makes it difficult to make arrays of values of mixed type.
Does this lead to losing the principal type property?
Yes.
And, if so, would you please give me an example where the principal type does not exist any more when introducing union types in the form above?
Certainly. Consider, in your extended Haskell: data B = B1 | B2 data C = ... type A = B | C | D -- A accepts values of either B or C or D Both A and B are types for B1, but neither is a substitution-instance of the other. This violates the principal type property whereby for every term x, either x is not typable or there exists a type T such that every type assignable to x is a substitution-instance of T. A better question might be, having extended the type system (and indeed the notion of 'type') in this way, how do I need to modify the concept of 'principal type'?
Do any papers exist about this topic? Is there any Haskell compiler supporting union types?
You might look at O'Haskell, which I understand has some kind of OOP-style polymorphism. I don't know if it has union types though. -- Ashley Yakeley, Seattle WA
Ashley Yakeley writes:
At 2000-11-24 02:02, Bernd =?iso-8859-2?Q?Holzm=FCller?= wrote:
When I got to know Haskell, I was expecting a construct for union types like:
data B = ... data C = ... type A = B | C | D -- A accepts values of either B or C or D (cf. the "Either a" type in the Prelude)
but this is not valid Haskell. Is there any reason for this restriction in the Haskell type system?
[...]
Does this lead to losing the principal type property?
Yes.
No, not if you update your notion of an instance to reflect the extended type system. [Whether one really wants complete type inference in this setting is another question, though.]
And, if so, would you please give me an example where the principal type does not exist any more when introducing union types in the form above?
Certainly. Consider, in your extended Haskell:
data B = B1 | B2 data C = ... type A = B | C | D -- A accepts values of either B or C or D
Both A and B are types for B1, but neither is a substitution-instance of the other. This violates the principal type property whereby for every term x, either x is not typable or there exists a type T such that every type assignable to x is a substitution-instance of T.
A better question might be, having extended the type system (and indeed the notion of 'type') in this way, how do I need to modify the concept of 'principal type'?
Polymorphic subtyping systems provide an answer to this question. My favourite reference in this field is @techreport{henglein:polysub, AUTHOR = {Henglein, Fritz}, YEAR = {1996}, TITLE = {Syntactic Properties of Polymorphic Subtyping}, INSTITUTION = {DIKU, University of Copenhagen}, type = {TOPPS Technical Report (D-report series)}, number = {D-293}, month = {May} }
Do any papers exist about this topic? Is there any Haskell compiler supporting union types?
You might look at O'Haskell, which I understand has some kind of OOP-style polymorphism. I don't know if it has union types though.
Indeed, O'Haskell is able to express the desired type structure rather directly: data B = B1 | B2 data C = ... data D = ... data A > B, C, D -- A accepts values of either B or C or D. The principal type for B1 is B, reflecting the fact that we can obtain every other valid type for B1 from B using either substitution (not needed here) or subtyping (since only supertypes of B are allowed to contain B1). For more info on O'Haskell, please consult http://www.cs.chalmers.se/~nordland/ohaskell/ -- Johan
participants (2)
-
Ashley Yakeley -
Johan Nordlander