Evan,
I read with interest your mail on polymorphic I/O requests.
These are difficult, but can be made easier if you recognise the two
checks which are needed for strong typing can be separated. First, some
background. Accessing a typed external environment requires an access
expression which tells you where to look for the input value and a type
assertion saying what type the value should have. The access expression
needs to be checked to make sure that there is a value there at all and
the type assertion needs to be checked for validity.
One model for this is to evaluate access expressions at compile time and bind
to data in the external environment at that time. Since the value is known
at this time and we know that all denotable values have a type which we can
compute then we can make a valid type assertion and do complete static
typechecking. However, for interactive programs we want to be able to write
programs involving access expressions whose type cannot be inferred at
compile time.
Static typechecking can still be performed, but with reference to type
assertions about access expressions which are made by the programmer.
These type assertions are assumed to be true by the compiler, but code
must be generated to check this validity before the access expression is
evaluated. This check can be separated from the success or failure of the
evaluation of the access expression by using an infinite union type. Access
expressions all have the same union type. The assertion of type within a
program is via an orthogonal union projection construct. So in the stream
I/O model, we have
data Request = ... | Access Name | Output Name UnionType | ...
data Response = ... | SomeResponse UnionType | ...
where an Access request reads input which is of type UnionType and
Output writes out a value of type UnionType.
To create a value of type UnionType, you use
inject value
and to get the value, you use
project unionvalue :: type
so for example a program (in Haskellese) to output an integer is
main resps = [Output "a" (inject 3)]
(with no failure check - but we know how to write that). And one to read
an integer is
main resps = [Access "a",AppendChan "stdout" ("Int was "++show a)]
where
a = project (extract (resps!!0)) :: Int
extract (SomeRespomse value) = value
(again no error stuff but that should be obvious too!)
I dont see any difficulty doing the same with continuation style I/O.
Dave McNally
University of St Andrews, Scotland.
