I am about to finish my PhD, where I used the Vienna Definition Language (VDL) to specify the semantics of some programming language constructs. In order to verify this semantics description using a type checker and by dynamic execution, I found and used Haskell as the language of choice to map the VDL description to Haskell. I was quite impressed about the expressive power of Haskell (e.g. the list comprehension syntax and the use of the functions "any" and "all" together with ad-hoc definable lambda-abstractions) and the flexible type system, which together allowed me to almost literally transcribe the VDL description into Haskell. Since then, I have used Haskell to build several parsers and compilers for simple script languages as well as for other purposes. There is one thing I was really missing in all these projects: the existence of union types (i.e. the union of value sets of two existing data types), for two reasons: - Firstly, to map VDL union types to Haskell, I needed to introduce one further indirection, using another data type with one special type constructor for each former variant. This was actually the biggest inconvenience in transforming VDL to Haskell. - Secondly, after having built abstract tree representations of languages while parsing, I did want to traverse and manipulate such trees (consisting of nodes belonging to several different data types) for semantic analysis and code generation several times. Unfortunately, I was not able to use a single function to map over the different nodes of the abstract syntax tree. The only viable solution I found was to use a set of functions, one for each node type, and to pass the whole set down the tree, extracting and applying the appropriate function for each node (type). To define one Haskell data type that defines each of the different nodes as one variant would of course lead to much less type safety, because each reference to a node would be much less precise/less informative. 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? 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? Do any papers exist about this topic? Is there any Haskell compiler supporting union types? Are there any considerations of integrating union types into the Haskell type system, at least for explicit type annotations (if type inference using union types should in any way be problematic)? I find the existence of union types very attractive. Apart from enhanced flexibility in modelling, type error messages would possibly be more traceable, because different branches in if- or case-expressions would have the *same* relevance, rather than the first branch being type-checked becoming normative for all other branches. Thanks in advance, Bernd Holzmüller ICS AG Sonnenbergstraße 13 70184 Stuttgart ++49 711 21037 0 holzmueller@ics-ag.de
On 24-Nov-2000, Bernd Holzmüller <holzmueller@ics-ag.de> wrote:
There is one thing I was really missing in all these projects: the existence of union types (i.e. the union of value sets of two existing data types)
Mercury has a similar type system to Haskell. This question came up a lot during the early days of Mercury, since many Prolog programmers were used to a programming style that made significant use of undiscriminated union types. What operations would you allow on union types? There's a number of possible choices. Here's some of them: (1) The only operation allowed on a union type is calling a type class method of a type class for which all the types in the union are instances. (2) Allow pattern matching on values of particular types, using `case'. (3) Allow both (1) and (2) If we allow (2), then some programming mistakes that previously were type errors would instead become just inexhaustive pattern matches for which you get a run-time error. For example: foo :: Maybe a -> b -> Maybe b foo x y = case list of [] -> Nothing (x:xs) -> Just x where list = case x of Nothing -> 0 -- oops, meant [] instead of 0 Just foo -> [y] If union types were allowed, with (2) above, this example would be legal, with `list' having the union type { [a], Integer }. But `foo Nothing 42' would evaluate to bottom, since the `case list' expression has no case with a pattern of type Integer. So allowing union types in this way would reduce static type safety, at least unless we also forbid inexhaustive pattern matches. If instead you only allow (1), then probably union types would not be suitable for expressing the kinds of things that you want to express with them.
Is there any reason for this restriction in the Haskell type system? Does this lead to losing the principal type property?
If you allow (2) above, there may be serious problems for principal types. For example, consider f x = case x of Nothing -> False Just _ -> True What's the most general type for `f'? The type `f :: Maybe a -> Bool' is less general than e.g. `f :: Union { Maybe a, ... } -> Bool', but you certainly don't want to infer the latter type. So (2) is definitely out. I guess we could use a separate `typecase' rather than `case', and require that `typecase' always be exhaustive. That might solve some of the problems. But even then, there may be some tricky problems remaining. Union types introduce subtyping, and type inference with subtypes and polymorphism is tricky -- in fact undecidable, if I recall correctly. However, there have been some pragmatic attempts to solve this problem in practice, even though the general case may be undecidable. I think there was a paper at the Industrial Applications of Prolog conference in 1996 on a system called PAN (for "Prolog Analyzer") that had a type checker that supported undiscriminated unions and/or subtypes. There were some cases that it didn't handle, but the authors claimed that this wasn't a problem since those cases didn't arise in practice.
I find the existence of union types very attractive. Apart from enhanced flexibility in modelling, type error messages would possibly be more traceable, because different branches in if- or case-expressions would have the *same* relevance, rather than the first branch being type-checked becoming normative for all other branches.
A type checker could easily generate better error messages in that sense simply by checking each case seperately first, and then merging the results, complaining if the types inferred in any two branches were not unifiable. But if you allow union types, the type checker couldn't report an error at the point where the two branches have types that are not unifiable; instead, it would have to infer a union type there, and the point where the types become inconsistent is only when the union type is later used in a context that requires one particular type. Reporting the error at that point of use is likely to make it harder to find the problem, since it is further away from the place where the error occurred. So I think allowing union types would most likely lead to *worse* error messages. -- Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit | of excellence is a lethal habit" WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
Ashley Yakeley wrote: 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'? ... There are two different kinds of 'general' here. Informally, you want the type most general in the type-substitution sense, but probably most specific in the subtype sense.
I think that's the point. It seems that for union types a different approach for type inference might be used to avoid the problems Fergus Henderson and others noted. The following typing rule could serve as a basis for further discussion: (1) Union types are used in type inference only if necessary to successfully type the expression. In other words, the type checker should try to use the most general type using parametric polymorphism, but at the same time the *smallest* possible type regarding the use of union types. That is, there is usually more than one most general type in case union types are used with type inference, but there is only one most specific type amongst those type expressions using union types (which is still equally or more general than the most general type in a type system without union types). The following picture illustrates this idea graphically: t1 t2 t3 possible types that correctly type e, using union types \ | / \|/ t most specific type of all types for e using union types | (is equally or more general than t0) | e :: t0 Haskell 98 (principal) type for e (not using union types) Example 1:
Fergus Henderson wrote:
f x = case x of Nothing -> False Just _ -> True
What's the most general type for `f'? The type `f :: Maybe a -> Bool' is less general than e.g. `f :: Union { Maybe a, ... } -> Bool', but you certainly don't want to infer the latter type.
Applying the above rule (1) would just give the expected result: f has type Maybe a -> Bool because from the body of the function there is no necessity of using a more general type using union types. Example 2:
foo :: Maybe a -> b -> Maybe b foo x y = case list of [] -> Nothing (x:xs) -> Just x where list = case x of Nothing -> 0 -- oops, meant [] instead of 0 Just foo -> [y]
The type of list must be inferred as Maybe a -> { [b], Integer } because otherwise the expression would not be typeable. However, the type of the case body for "case list of ..." should be inferred as [a] -> Maybe a (which is the most specific and here as well the most general type when not considering union types) which could not be legally applied to the list argument, which is of type { [a], Integer }, because it is too general: it cannot match type [a] for all elements of the union. Thus, the function is not correctly typed (I assume the quite obvious matching rules with union types as follows: t1 matches Union t2 t3 if t1 matches t2 or t1 matches t3 and Union t2 t3 matches t1 if both t2 and t3 match t1).
Ashley Yakeley wrote:
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.
Againg: applying (1) yields B1 :: B (which is the most specific type not using unions) and *not* B1 :: A. It seems that the typing rule given by (1) is a compromise of the proposed explicit style for the use of union types and the flexibility and accuracy achieved by type inference. -- Bernd Holzmüller
participants (2)
-
Bernd Holzmüller -
Fergus Henderson