I think that the following points have emerged from the recent discussion
about the proposed newtype declaration:
1) Pattern matching against strict constructors will result in
functions which are strict in the annotated constructor argument. For
example:
data T = A !Int
f :: T -> Bool
f (A n) = True
results in f such that
f (A undefined) = undefined
This results in a loss of referential transparency because, before we can
replace f (A e) by True, we must check that e is not undefined. Of
course, a transformation in this direction can only make a program more
defined, so perhaps we should be more worried by the fact that it would
be unsafe to replace True by f (A e), in general.
2) It would be wrong to define the proposed
newtype N = B G
declaration as being equivalent to
data N = B !G
because a) it will restrict its use to G such that !G makes sense, and b)
programmers will be tripped up by the strict pattern matching semantics
above.
On reflection, I think I agree with point 2, so if the proposed newtype
syntax is adopted it will need to be given a semantics independently of
that of strict constructors, as Simon has described.
On the other hand, it also seems to me that the reason this discussion
started is that the proposed newtype syntax hijacks the constructor
syntax for a new purpose: the definition of an isomorphism. Since the
declaration
newtype N = B G
means "let N be isomorphic to G and let B :: G -> N be one half of the
isomorphism" it is clear that B is not a constructor in the usual sense at
all. In Haskell and its antecedents (though not in the general setting of
term rewriting systems) it is well established that for
f (B e) = ...
to be legal, B must be a constructor (with the consequence that f is
strict). The proposed newtype syntax is a significant departure from
this.
Would it really be so inconvenient if pattern matching couldn't be used
for the iso from G to N? How about a syntax which made both halves of the
isomorphism explicit?
newtype in :: N <-> G :: out
The example from the earlier postings would then be rendered as
newtype in :: Arg <-> Int :: out
foo :: Arg -> (Int, Arg)
foo a = (n, in (n + 1)), where n = out a
Implementations would be free to implement in and out as id
foo a = (n, id (n + 1)), where n = id a
and then magic them away
foo a = (a, a + 1)
Sebastian Hunt
