I've had a few more thoughts on this subject..
As far as the problem with 'as patterns' is concerned (demo2) I think
it should be fairly easy to modify the type checker to allow such
function definitions, as follows
Wherever a varible (which is known to match a given pattern)
occurs in an expression, just convert the pattern to an expression
substitute the resulting expression for the variable and type check
accordingly.
It would then be a matter for the compiler implementor to decide if
the two representations were identical and whether or not to actually
use the 'as pattern'.
The real problem seems to me to be this..
Suppose f has type..
f :: Int -> Char
then
demo1 f :: Either Int c -> Either Char c
But there doesn't seem to me that one can safely infer that
demo1 f (Right "demo") :: Either _ [Char]
(despite the fact that this is certainly true if one were to accept my
earlier arguments).
It is conceivable that a very sophisticated type checker might be could
proceed along the lines that I suggested, but only by making use of
very complex case statements which essentially mirror the case analysis
in the functions definition. This might be ok for automatic type inference
but I don't think anybody would want to write such complex
type signatures without a pretty good reason :-)
I'm begining to think type checking is a lot more subtle than it appears
at first glance, can anybody point me in the direction of a 'readable'
account of current 'state of the art' type systems and inference?
Is the Haskell type system 'state of the art'?
Regards
--
Adrian Hey
