In article <·····················@st-andrews.ac.uk> ····@st-andrews.ac.uk (Antony J. T. Davie) writes:
> Haskell [...] has a complete formal description,
Where?
Seriously, I know that such a description was being written. Has it been
finished? Is it available?
Dave.
--
"One in the eye for the Lord, one hand, one sword, one running sore.
Under the sea wind came Augustine. Join hands, make war, Lord."
-- Blyth Power
In article <·····@skye.dcs.ed.ac.uk> ··@dcs.ed.ac.uk (Dave Berry) writes:
>In article <·····················@st-andrews.ac.uk> ····@st-andrews.ac.uk (Antony J. T. Davie) writes:
>> Haskell [...] has a complete formal description,
>
>Where?
Glasgow!
>Seriously, I know that such a description was being written. Has it been
>finished?
Practically! The semantics has been divided into:
Static Semantics [50+ pages, full Haskell source level, not kernel]
This is essentially complete. One or two odd corners remain to
be completed. The most significant of these is derived instances.
I do have a recent draft for these, if you're interested.
Dynamic semantics [20 pages, post static-semantics level]
This is complete as far as I'm aware.
The static semantics follows the SML form, but at the level of Haskell
source, rather than defining the semantics of a kernel language. This
gives a much more direct semantics than with SML, which we hope helps
to make it clearer. As part of the typing rules, the static semantics
defines a translation into 2nd-Order Lambda Calculus. This defines
the meaning of source-level overloading. The translation is used as
the basis for the dynamic semantics, which is consequently both
shorter and simpler than the static semantics. For consistency,
an axiomatic style is used.
The static semantics has been used as the formal specification of the
type inference algorithm used in the new Glasgow compiler.
> Is it available?
*Drafts* are available from ftp.dcs.glasgow.ac.uk using Internet FTP.
Host: ftp.glasgow.ac.uk
Login: anonymous
Password: <your email address>
Files: pub/glasgow-fp/papers/static-semantics.dvi
dynamic-semantics.dvi
Type: Binary
These are binary DVI files, so remember to set FTP type binary when
fetching them.
Comments are very much appreciated!
Kevin
--
This Signature Intentionally Left Blank. E-mail: ··@dcs.glasgow.ac.uk
^^^