It's true that GADTs does just that. But only if you use them. And they are not part of Haskell. :) -- Lennart Jacques Carette wrote:

I was under the impression that, in ghc 6.4 at least, GADTs did just that: use information gained by matching on the type constructor to refine types. I sort-of expected that the extension to pattern matching would follow.

Or is that a nice paper waiting to be written?

Jacques

Lennart Augustsson wrote:

...

A somewhat similar problem exists even without fields:

foo :: Either a b -> Either () b foo (Left _) = Left () foo x@(Right _) = x

Since Haskell type checking doesn't use the information gained by pattern matching to refine types we just have to accept that some perfectly safe programs don't type check.

-- Lennart

Lennart Augustsson wrote:

A somewhat similar problem exists even without fields:

foo :: Either a b -> Either () b foo (Left _) = Left () foo x@(Right _) = x

Since Haskell type checking doesn't use the information gained by pattern matching to refine types we just have to accept that some perfectly safe programs don't type check.

Well, not perfectly safe. We already had this discussion (about []), but to say it again: the value bound by any pattern has some particular type. x above doesn't have type (Either a b) for arbitrary a and b, but rather (Either a b) for some specific a and b. Unless that specific a happens to be (), x doesn't have the correct type to be the rhs of foo. It would require a radical change to GHC (moving away from System F as a basis for the intermediate language Core) to implement a language in which this wasn't true. Here is (approximately) the Core translation of foo above:

foo :: forall a b. Either a b -> Either () b foo = /\ a b -> \ e -> case e of Left _ -> Left @() @b () Right _ -> e

You call this as (foo @a @b e), where e has type (Either a b). So, the call (foo @a @b (Right @a @b x)) reduces (ignoring types) to (Right @a @b x). This reduces a term of type (Either () b) to one of type (Either a b). That's not type safe. Jon Cast

...

Lennart Augustsson wrote:

<snip>

Jonathan Cast wrote:

...

Here is (approximately) the Core translation of foo above:

...

foo :: forall a b. Either a b -> Either () b foo = /\ a b -> \ e -> case e of Left _ -> Left @() @b () Right _ -> e

You call this as (foo @a @b e), where e has type (Either a b).

So, the call (foo @a @b (Right @a @b x)) reduces (ignoring types) to (Right @a @b x). This reduces a term of type (Either () b) to one of type (Either a b). That's not type safe.

There are no types around at run time

We agree on this, but disagree on the reason. I think we may have to agree to disagree on the reason, but I would rather explain my position first (see below).

so in case foo is being passed a Right argument the representation of the result is identical to the argument.

So? Types are logical tools we use to structure our programs and guarantee their safety; type safe is a sufficient condition for ``will not segfault (or similarly fail)'', not an equivalent condition. In any case, it doesn't matter. If I say:

newtype Plus alpha beta = Plus (Either alpha beta) bat :: Plus alpha beta -> Either alpha beta bar x = x

bar's result is /guaranteed/ by the standard to have the same representation as its argument, but it still doesn't type check. Why? Because ``type safe'' doesn't mean ``uses the right representation at run time''. Types are not a computer science concept; they are a foundation of mathematics concept, invented around the turn of the previous century I believe by Bertrand Russell to get around certain logical problems in set theory, and I believe brought to prominence by Martin-Löf as a foundation for intuitionistic mathematics. Types made their first contact with lambda-terms in Alonzo Church's time, at which point the lambda-calculus was still intended as a system for foundations of mathematics. We use types in computer science because they are useful, but they don't arise from information theory or representation theory or any other branch of computer science. Therefore, genuine types don't exist at run time. In any language. Types are not properties of programs (which are not mathematical objects), but rather of languages (which are); since no machine language (that I know of) is typed, types do not exist at run time. No type theory (that I know of) goes beyond System F in accepting anything like foo. So, given the current state of the art, foo is unconditionally ill-typed. That could change if someone comes up with a /consistent/ type theory that accepts foo, but foo is ill-typed at the moment.

(OK, if you want to be very pedantic, this isn't necessarily true for every possible implementation of Haskell, just all existing ones. :)

``Perfectly correct'' is an open invitation to pedanticism :) Jon Cast

Hello Lennart, Friday, June 24, 2005, 9:16:22 PM, you wrote: LA> There are, of course, type systems where my program works fine. LA> O'Haskell is an example of a language with such a type system. LA> In O'Haskell the Either type is defined like this: i like O'Haskell because it's very close to traditional OO languages in its ways to extend the types. why O'Haskell is not really implemented as extension to GHC/Hugs? because it is not compatible with System F? -- Best regards, Bulat mailto:bulatz@HotPOP.com

Lennart Augustsson wrote: <snip>

There are, of course, type systems where my program works fine. O'Haskell is an example of a language with such a type system. In O'Haskell the Either type is defined like this:

data Left a = Left a data Right a = Right a data Either a b > Left a, Right b

which means that Either is really a union of the Left and Right types. Now my program type checks. :)

foo :: Either a b -> Either () b foo (Left _) = Left () foo x@(Right _) = x

And it has type checked in various type systems for quite a while, but not in System F. But System F is not the end all of type systems.

OK. I happily yield. Jon Cast

Daniel Brown wrote:

Jonathan Cast wrote:

...

Lennart Augustsson wrote:

...

foo :: Either a b -> Either () b foo (Left _) = Left () foo x@(Right _) = x

Since Haskell type checking doesn't use the information gained by pattern matching to refine types we just have to accept that some perfectly safe programs don't type check.

Well, not perfectly safe. We already had this discussion (about []), but to say it again: the value bound by any pattern has some particular type. x above doesn't have type (Either a b) for arbitrary a and b, but rather (Either a b) for some specific a and b. Unless that specific a happens to be (), x doesn't have the correct type to be the rhs of foo. It would require a radical change to GHC (moving away from System F as a basis for the intermediate language Core) to implement a language in which this wasn't true.

I see that the argument to foo has type `Either a b` (unquantified), but why can't x, bound to the value that matches the pattern, have the type of the pattern?

Because it's bound to a value of the type of the argument, not of the type of the pattern. What about the function

bar :: alpha -> beta bar x = x

? The pattern here is x, and its type is (x :: forall tau. tau). But, I think it axiomatic that typing rules have to forbid functions like bar.

In this case, that would let `x :: forall x. Either x b`, which unifies with `Either () b`.

Jon Cast

Malcolm Wallace wrote:

Whereas in the named field example, the rhs expression v {field1=Void} does indeed have the type Fields Void as declared in the signature. The expression explicitly converts all the relevant interior fields to Void. At least, that is how it could appear to a naive programmer like me :-)

If v has a second field with the same type of field1, do you really expect that field2 is silently casted to the new type of field1? (This would be unsafe) Christian

On Thu, Jun 23, 2005 at 09:08:12PM +0200, Christian Maeder wrote:

Malcolm Wallace wrote:

...

...

voidcast :: Fields a -> Fields Void voidcast v@(VariantWithTwo{}) = v { field1 = Void , field2 = Void } voidcast v@(VariantWithOne{}) = v { field1 = Void }

I would not expect that updating only field1 can change the type of v.

But it can. Note that if you change the second field1 to field3 (both in datatype definition and voidcast function), the code will be accepted.

The right thing is to construct a new value.

In the report, section 3.15.3, "Updates Using Field Labels", the translation is simply a pattern-match and (re-)construction. There is no requirement that "input" and "output" types are the same. It can be a nice feature actually, I've used it once or twice. Best regards Tomasz

Christian Maeder writes:

Even consecutive updates (that could be recognized by the desugarer) don't work:

voidcast v@VariantWithTwo{} = v { field1 = Void} {field2 = Void }

Yes, I find it interesting that consecutive updates are not equivalent to a combined update. I believe this is largely because named fields are defined as sugar - they behave in some sense like textual macros in other languages, which can often turn out to have unexpected properties. Here is a strawman proposal, which does not fix the consecutive update problem, but which might address the original typing problem. The Report (section 3.15) defines the following conditions on a named field update: * all labels must be taken from the same datatype * at least one constructor must define all of the labels mentioned in the update * no label may be mentioned more than once * an execution error occurs when the value being updated does not contain all of the specified labels. Now, this last condition is rather nasty - a runtime error - and I would like to eliminate it. I think we can do so by also eliminating the second condition. That is, I would like to be able to use a set of labels that might not be contained solely within a single constructor. The obvious semantics is that if a constructed value does not contain a label of that type, that part of the update is discarded. Hence, I could write a single expression that updated all possible variants of a type, simply by unioning all their possible labels. e.g.

data Fields a = VariantWithOne { field1 :: a } | VariantWithTwo { field2 :: a }

voidcast :: Fields a -> Fields Void voidcast v = v { field1 = Void , field2 = Void }

The only change required in the desugaring translation specified in the Report, is to replace the default case match from _ -> error "Update error" to v -> v (The desugaring does not currently seem to implement condition 2, and the original case default only partially addresses condition 4.) What might be the downside of such a change? Well, an update expression (such as in my example above) could confuse the programmer into thinking that the value contains at least two fields, when it in fact contains only one. Likewise, it may suggest strongly that a certain value associated with a label will afterwards be stored within the variable (as now), whereas it is possible that the value afterwards appears nowhere within the variable (because the label was not a member). How do these problems weigh against the increased convenience of the proposal? I think they are very slight, and the benefit is potentially larger. It would break no old programs. It would permit some current programs to be more succinct. Regards, Malcolm

Christian Maeder writes:

...

voidcast v@(VariantWithOne{}) = v { field1 = Void , field2 = Void }

Setting field2 only assures type correctness, but the value of field2 would be ignored at runtime.

Exactly what I was proposing.

...

I could write a single expression that updated all possible variants of a type, simply by unioning all their possible labels.

I want to detect errors as early as possible.

But you can already write this:

...

voidcast v@(VariantWithOne{}) = v { field1 = Void , field2 = Void }

and you do not get a compile time error - it is a runtime error. I am proposing that it should not be thought of as an error at all. Regards, Malcolm

Christian Maeder wrote:

Malcolm Wallace wrote:

...

Christian Maeder writes:

...

...

voidcast v@(VariantWithOne{}) = v { field1 = Void , field2 = Void } Setting field2 only assures type correctness, but the value of field2 would be ignored at runtime. Exactly what I was proposing.

I know, but how "save" is this. i.e. when you mistype/exchange field names?

The criterion should be how "robust" you can program, i.e. can you easily detect the spots that you must change (or need not to be changed) when the data type changed? (One of the advantages of Haskell's type system) Christian

Malcolm Wallace wrote:

...

Yes, I find it interesting that consecutive updates are not equivalent to a combined update. I believe this is largely because named fields are defined as sugar - they behave in some sense like textual macros in other languages, which can often turn out to have unexpected properties.

Christian Maeder writes:

I share your characterization "like textual macros". The question is, should this be eliminated?

Although the behaviour is initially surprising, I suppose it is easily explained. After all, an equivalent expression using lambdas would have the same typing problem: data A a = A { one, two :: a } update v@(A{}) = v { one = Void } { two = Void } update' v@(A{}) = (\A one two -> A one Void) $ (\A one two -> A Void two) $ v Because of this, I would be reluctant to define that consecutive field updates can be semantically amalgamated into a single update.

Would it be cleaner, though less convenient some times, if the types of updated values must not change?

I believe this is a very different question from the consecutive update one. By analogy with the lambda equivalent, I can see no reason to outlaw a type change, where all the relevant types change at the same time: update_ok v@(A{}) = v { one=Void, two=Void } update_ok' v@(A{}) = (\A one two -> A Void Void) v Regards, Malcolm

Christian Maeder writes:

Typing fails in your original example: voidcast v@VariantWithOne{} = v {field1 = Void} but not in the "lambda equivalent" voidcast v@VariantWithOne{} = (\ (VariantWithOne a) -> VariantWithOne Void) v

Hmm. Yes, that was my original point.

But voidcast v@VariantWithOne{} = ( \ x -> case x of VariantWithTwo a b -> VariantWithTwo Void b VariantWithOne a -> VariantWithOne Void) v fails like the field notation.

Yes, this is a more accurate translation of the field notation to a lambda expression, and therefore suffers the same problem. My proposal was to allow voidcast v = v { field1 = P, field2 = Q } to be interpreted as the lambda expression voidcast v = ( \ x -> case x of VariantWithTwo a b -> VariantWithTwo P Q VariantWithOne a -> VariantWithOne P) v where the information about field2=Q is omitted from the clauses where no field2 exists. (I'm using P and Q instead of Void, to highlight the apparent loss of information on the RHS of the pattern-match.)

I think writing "VariantWithOne {field1 = Void}" instead of "v {field1 = Void}" is as clear as writing "Right r" again on the rhs instead of "x" from the pattern "x@(Right r)"

I can only repeat myself, that the field being updated (and type-converted) is only one of many, and all other fields should carry the same value in the updated structure as in the original. There is no good way to write this at the moment. If there were no type-conversion, a field update would work just great. But because of the conversion, one is forced to use explicit construction. Regards, Malcolm

Christian Maeder writes:

...

...

voidcast :: Fields a -> Fields Void voidcast v@(VariantWithTwo{}) = v { field1 = Void , field2 = Void } voidcast v@(VariantWithOne{}) = v { field1 = Void }

I would not expect that updating only field1 can change the type of v. The right thing is to construct a new value. This looks as follows with record syntax:

voidcast VariantWithTwo{} = VariantWithTwo { field1 = Void , field2 = Void } voidcast VariantWithOne{} = VariantWithOne { field1 = Void }

Ah, but the reason I want to use field update, rather than a new construction on the rhs, is that my type really has lots of other fields (not mentioned here), which are all of fixed definite types (not parametric). It is much nicer to be able to write v { field1 = Void } than VariantWithOne { field1 = Void , field2 = field2 v , field3 = field3 v , field4 = field4 v , field5 = field5 v ... } which has so much more scope for making a mistake, not to mention the extra maintainance work required if I ever add or delete a field from the type. Regards, Malcolm