Re: Haskell 1.3 (newtype)
Sebastian suggests using some syntax other than pattern matching to express the isomorphism involved in a newtype. I can't see any advantage in this. Further, Simon PJ claims that if someone has written data Age = Age Int foo (Age n) = (n, Age (n+1)) that we want to be able to make a one-line change newtype Age = Age Int leaving all else the same: in particular, no need to add twiddles, and no changes of the sort Sebastian suggests. I strongly support this! (No, Simon and I are not in collusion; indeed, we hardly ever talk to each other! :-) Cheers, -- P
Re: Haskell 1.3 (newtype)
Well, I'm glad to see I provoked some discussion! Simon writes: Lennart writes: | So if we had | |data Age = Age !Int |foo (Age n) = (n, Age (n+1)) | | it would translate to | |foo (MakeAge n) = (n, seq MakeAge (n+1)) | | [makeAge is the "real" constructor of Age] Indeed, the (seq MakeAge (n+1) isn't eval'd till the second component of the pair is. But my point was rather that foo evaluates its argument (MakeAge n), and hence n, as part of its pattern matching. Hence foo is strict in n. Why should foo evaluate its argument? It sounds to me like Lennart is right, and I should not have let Simon lead me astray! I think its vital that users know how to declare a new isomorphic datatype; it is not vital that they understand strictness declarations. Hence, I favor that newtype Age = Age Int data Age = Age !Int be synonyms, but that both syntaxes exist. This is assuming I have understood Lennart correctly, and that foo (Age n) = (n, Age (n+1)) foo' a = (n, Age (n+1)) where (Age n) = a are equivalent when Age is declared as a strict datatype. Unlike Sebastian or Simon, I believe it would be a disaster if for a newtype one had to distinguish these two definitions. Cheers, -- P
Re: Haskell 1.3 (newtype)
Lennart writes: | So if we had | | data Age = Age !Int | foo (Age n) = (n, Age (n+1)) | | it would translate to | | foo (MakeAge n) = (n, seq MakeAge (n+1)) | | [makeAge is the "real" constructor of Age] | | Now, surely, seq does not evaluate its first argument when the | closure is built, does it? Not until we evaluate the second component | of the pair is n evaluated. Indeed, the (seq MakeAge (n+1) isn't eval'd till the second component of the pair is. But my point was rather that foo evaluates its argument (MakeAge n), and hence n, as part of its pattern matching. Hence foo is strict in n. Sebastian writes: | Is it really a good idea to extend the language simply to allow foo and | foo' to be equivalent? The effect of foo' can still be achieved if Age is | a strict data constructor: | | data Age = Age !Int | | foo'' :: Age - (Int, Age) | foo'' a = (n, Age (n+1)) where (Age n) = a | | and compilers are free (obliged?) to represent a value of type Age by an | Int. Indeed, it's true that foo'' does just the right thing. Furthermore, I believe it's true that given the decl data T = MkT !S the compiler is free to represent a value of type T by one of type S (no constructor etc). Here are the only real objections I can think of to doing "newtype" via a strict constructor. None are fatal, but they do have a cumulative effect. 1. It requires some explanation... it sure seems a funny way to declare an ADT! 2. The programmer would have to use let/where bindings to project values from the new type to the old, rather than using pattern matching. Perhaps not a big deal. 3. We would *absolutely require* to make (-) an instance of Data. It's essential to be able to get data T = MkT !(Int - Int) 4. We would only be able to make a completely polymorphic "newtype" if we added a quite-spurious Data constraint, thus: data Data a = T a = MkT !a (The Data is spurious because a value of type (T a) is going to be represented by a value of type "a", and no seqs are actually going to be done.) 5. We would not be able to make a newtype at higher order: data T k = MkT !(k Int) because there's no way in the language to say that (k t) must be in class Data for all t. [This is a somewhat subtle restriction on where you can put strictness annotations, incidentally, unless I've misunderstood something.] Simon
Re: Haskell 1.3 (newtype)
On Tue, 12 Sep 1995, Lennart Augustsson wrote: The posted semantics for strict constructors, illustrated by this example from the Haskell 1.3 post, is to insert seq. data R = R !Int !Int R x y = seq x (seq y (makeR x y)) -- just to show the semantics of R So if we had data Age = Age !Int foo (Age n) = (n, Age (n+1)) it would translate to foo (MakeAge n) = (n, seq MakeAge (n+1)) [makeAge is the "real" constructor of Age] I had assumed (as Simon seems to) that the semantics of pattern matching against a strict constructor would accord with the following: 1. matching a simple pattern involves evaluating the expression being matched to the point that its outermost constructor is known 2. for strict constructors this must result in the annotated constructor argument(s) being evaluated From what Lennart says, this is not the intended semantics. So what *is* the intended semantics? Sebastian Hunt
Re: Haskell 1.3 (newtype)
The design of newtype appears to me incorrect. The WWW page says that declaring newtype Foo = Foo Int is distinct from declaring data Foo = Foo !Int (where ! is a strictness annotation) because the former gives case Foo undefined of Foo _ - True = True and the latter gives case Foo undefined of Foo _ - True = undefined. Now, on the face of it, the former behaviour may seem preferable. But trying to write a denotational semantics is a good way to get at the heart of the matter, and the only way I can see to give a denotational semantics to the former is to make `newtype' define a LIFTED type, and then to use irrefutable pattern matching. This seems positively weird, because the whole point of `newtype' is that it should be the SAME as the underlying type. By the way, with `newtype', what is the intended meaning of case undefined of Foo _ - True ? I cannot tell from the summary on the WWW page. Defining `newtype' in terms of `datatype' and strictness avoids any ambiguity here. Make newtype equivalent to a datatype with one strict constructor. Smaller language, more equivalences, simpler semantics, simpler implementation. An all around win! Cheers, -- P
