A Dynamic Semantics for Haskell (Draft)

Kevin Hammond and Cordelia Hall^{∗}

April 14, 1992

Abstract

This paper defines a dynamic semantics for the functional programming language Haskell. The semantics defines the meaning of expressions, modules and programs, including all nonoptional I/O requests. All constructs in the Haskell language are considered. We use the same natural semantics style as the definition of Standard ML.

For brevity, we assume that the translations specified by the Wadler/Peyton Jones static semantics have been performed, and base our source language on the target language of the static semantics.

1 Introduction

This paper defines the dynamic semantics of the full Haskell language [HW90, HJW91, HJW92]. The dynamic semantics is complementary to the existing static semantics for Haskell [JW92] in two respects: firstly it defines the meaning of the second-order polymorphic lambda-calculus which is synthesised by that semantics; secondly it is defined using a natural semantic form, where meaning is expressed through judgement rules. This corresponds to the type inference judgements used in the static semantics.

The paper is designed as a short reference work, to be read in conjunction with the Haskell report. Consequently, only minimal explanatory text is provided here. We expect that other papers will provide a full commentary on the semantics, and take a more introductory slant.

We have not attempted to give an explicit semantics of graph-reduction. In the context of a language definition, such an approach seems both excessively low-level and unnecessarily restrictive. Rather, we have captured the essence of non-strict evaluation through the notion of “closures”: syntactic values paired with an environment.

This semantics thus defines the meaning of a Haskell program by specifying its resulting value (in terms of state-transitions on an initial state), but leaves unspecified such operational details as evaluation order, or sharing. These details are, in our opinion, best covered by an operational semantics for a particular machine model rather than the general language semantics.

∗Department of Computing Science, University of Glasgow, 17 Lilybank Gardens, Glasgow, UK. Tel: +44-41-339-8855 ext {5619,4984}. Email: {kh,cvh}@dcs.glasgow.ac.uk

2 Notation

Except where noted, we use the same notation as the definition of Standard ML [HMT91]. The syntax of our source language is as defined for the static semantics of Haskell [JW92], but with the extension of patterns to include simple variables (var) in addition to typed variables (var : τ). For clarity, this abstract syntax is summarised in Figures 1–3. A program comprises a set of modules, each of which is a set of bindings.

We assume these bindings may be mutually recursive. A small function translates the static semantics binds and monobinds into this simpler form.

\begin{aligned}[[rec m]] & = & [[m]] \\ [[b_{1} then b_{2}]] & = & \{[[b_{1}]]\} ∪ \{[[b_{2}]]\} \\ [[m_{1} ; m_{2}]] & = & \{[[m_{1}]]\} ∪ \{[[m_{2}]]\} \\ [[\{\}]] & = & \{\} \\ [[m]] & = & \{m\} \end{aligned}

Our semantics is given in terms of the semantic domain SemVal defined below. A Closure comprises a syntactic expression object plus an environment, ≪ exp, E ≫ . This is used to define a non-strict semantics for function application. We use ⟨…⟩ to enclose semantic tuples in the SemVal domain. This avoids confusion with the syntactic tuple domains, and allows the direct representation of 1-tuples where necessary. D^{∗} defines the domain of all tuples of D: ⟨⟩, ⟨D⟩, ⟨D, D⟩ …

Every semantic domain D incorporates an implicit bottom element ⊥_{D}. BasVal and BasCon are fully defined in Section 9.

program → {mod_{1}, …, mod_{n}}  (n > 0)
mod → binds
binds → {bind_{1}, …, bind_{n}}  (n ≥ 0) Set of bindings
bind → pat grhs  A pattern binding
| var match  A function binding
match → match_{1} match_{2}  Case alternatives
| mrule
mrule → grhs
| pat mrule
grhs → grhs_{1} grhs_{2}  Guarded right-hand side
| | guard = exp
| = exp
guard → exp
pat → var  Variable
| _Wildcard
| con pat_{1} … pat_{n}  Compound pattern
| ~pat  Lazy pattern
| var@pat  As-pattern
| [pat_{1}, …, pat_{n}]  (n ≥ 0) List pattern
| (pat_{1}, …, pat_{n})  (n ≥ 2) Tuple pattern
| ()  Unit pattern
| var : τ  Translated patterns
| var : κ τ  Dictionary variables

Figure 1: Abstract syntax: Definitions and Patterns

exp → var  Variable
| con  Constructor
| integer  Integer
| float  Real number
| char  ASCII character
| string  Literal string
| \mrule  Lambda abstraction
| exp exp′  Function application
| case exp of match  Case expression
| if exp_{1} then exp_{2} else exp_{3}  Conditional
| [exp|quals]  List comprehension
| let binds in exp  Local definition
| [exp_{1}, …,exp_{n}] (n ≥ 0) List
| (exp_{1}, …,exp_{n})  (n = 0 or n ≥ 2) Tuple
| Λα_{1} … α_{n}-> exp  Type abstraction
| exp τ_{1} … τ_{n}  Type application
quals → quals,quals  Qualifiers
| pat<-exp  Generator
| guard  Filter

Figure 2: Abstract syntax: Expressions

Monotypes τ → α  Type variable
| χ τ_{1} … τ (k ≥ 0) Structured type
| τ_{1} → τ_{2}  Function type
| [τ]  List type
| (τ_{1}, …, τ_{k})  (k = 0 or k ≥ 2) Tuple type
| Bool  Boolean type

Figure 3: Syntax of semantic types

b ∈ BasVal = {PrimPlusInt, PrimEqInt, …} Basic Values
BasCon = {(:), Nil, True, False, …}  Basic Constructors
Con =  BasCon + con
Closure = ≪ match, Env ≫  Closures
c, f, v ∈ SemVal = BasVal + Con SemVal^{∗}+  Semantic Values

SemVal^{∗} + Closure

E ∈ Env = {var ↦ SemVal+ Environments

BasVal ↦ exp }

S ∈ State = Channel × File × Environ× States

Prog × Args × Echo

Channel = {SemVal ↦ SemVal}  Filesystem channels
File = {SemVal ↦ SemVal} Files: name ↦ contents
Environ = {SemVal ↦ SemVal}  Program environment
Prog =  SemVal  Program Name
Args =  SemVal^{∗}  Program arguments
Echo =  < SemVal, SemVal >  Echoing on/off; Echo allowed

m_{1} ⊕ m_{2} operator updates an environment mapping m_{1} by the new mapping m_{2}. m_{1} ⊕^{→} m_{2} is similar, but allows values in m_{1} to be “shadowed” by those in m_{2}. e ⊖ m removes the mapping m from an environment e.

We use two judgement forms ⊢ and ⊧. The latter is used for judgements on matches, of the form E,v ⊧ match ⇒ v’; the former is used in all other cases. We use a special annotated version

of the former judgement ⊢^{OS} S ⇒ S’ to indicate operating system transformations of the state. For obvious reasons, we do not define the effect of these transformations in this semantics.

3 Expressions

This section defines the semantic rules for expressions. The semantic function sval maps a semantic string into the semantic list of characters comprising the elements of that string. fix is the least fixpoint operator. map and concat are defined in the obvious way, + + is used for list concatenation. caseError is used to define the semantics of match failure. It uses the error function from the Haskell prelude.

map f [ ] = [ ]

map f ((:) x xs) = (:) (f x) (map f xs)

concat [ ] = [ ]

concat ((:) x xs) = (+ +) x (concat xs)

caseError = error “Unexpected Match”

The first few rules handle the semantics for simple expressions. Note that the semantics for conditional expressions (rule 10) is defined in terms of the semantics for case-expressions (rule 9).

E (var) = v ; E ⊢ var ⇒ v  (1)

E ⊢ exp ⇒ v E_{0} (b) = exp

E ⊢ b ⇒ v (2)

E ⊢ con ⇒ con <>  (3)
E ⊢ char ⇒ char  (4)

sval (string) = v E ⊢ string ⇒ v

(5)

E’ ⊢ exp ⇒ v

E ⊢ ≪ exp, E’ ≫ ⇒ v (6)

E ⊢ exp ⇒ ≪ match, E’ ≫ E ⊕^{→} E’, ≪ exp’, E ≫ ⊧ match ⇒ v

E ⊢ exp exp’ ⇒ v

(7)

E ⊢ exp ⇒ con < v_{1} …, v_{n} >

E ⊢ exp’ ⇒ v

E ⊢ exp exp’ ⇒ con < v_{1}, …, v_{n}, v > (8)

E ⊢ exp ⇒ v E,v ⊧ match ⇒ v’

E ⊢ case exp of match ⇒ v’

(9)

E ⊢ case exp_{1} of {True = exp_{2} False = exp_{3}} ⇒ v E ⊢ if exp_{1} then exp_{2} else exp_{3} ⇒ v

(10)

E ⊢ (:) exp_{1} (… ((:)exp_{n} [ ]) …) ⇒ v

n ≥ 1

E ⊢ [exp_{1}, …, exp_{n}] ⇒ v

(11)

E ⊢ [ ] ⇒ Nil <>  (12)
E ⊢ () ⇒ <>  (13)

∀i. 1 < i ≤ n, E ⊢ exp_{i} ⇒ v_{i}

E ⊢ (exp_{1}, …, exp_{n}) ⇒ < v_{1}, …, v_{n} > (14)

Rules (15)–(17) define the semantics of list comprehensions, as specified in the Haskell report.

E ⊢ concat [ [ exp | qual_{2} ] | qual_{1} ] ⇒ v E ⊢ [exp | qual_{1}, qual_{2} ] ⇒ v

(15)

E ⊢ map (\pat = exp) exp’ ⇒ v E ⊢ [exp | pat -> exp’] ⇒ v

(16)

E ⊢ if exp’ then [exp] else [ ] ⇒ v E ⊢ [exp | exp’] ⇒ v (17)

Rules (18)–(20) give the semantics of let-expressions. Rule (18) applies when there are multiple bindings in a let. Rules (19) and (20) handle non-recursive and recursive bindings, respectively.

E ⊢ let {(∼ pat_{1}, …, ∼ pat_{n}) = (exp_{1}, …, exp_{n})} in exp ⇒ v
n > 1
E ⊢ let {pat_{1} = exp_{1}, …, pat_{n} = exp_{n}} in exp ⇒ v

(18)

fv(pat) ∩ fv(exp) = ∅

E ⊢ case exp’ of {∼ pat = exp} ⇒ v

E ⊢ let {pat = exp’} in exp ⇒ v

(19)

fv(pat) ∩ fv(exp) ≠ ∅

E ⊢ case exp’ of {∼ pat = fix (\ ∼ pat = exp)} ⇒ v

E ⊢ let {pat = exp’} in exp ⇒ v

(20)

Rules (21) and (22) handle the second-order polymorphic λ-calculus forms introduced by the dictionary translations in the static semantics. These terms are used only to convey type information: neither type applications (rule 22) nor type abstractions (rule 21) have any meaning in this value-oriented semantics.

E ⊢ exp ⇒ v

E ⊢ Λ α_{1} … α_{n}-> exp ⇒ v (21)

E ⊢ exp ⇒ v

E ⊢ exp τ ⇒ v (22)

4 Matches

For clarity, we use a different kind of turnstile (⊧) for match inference rules. E,v ⊧ e ⇒ v’ defines the meaning of match with respect to a single matched value e. The semantics for definitions and applications ensures that matches are curried appropriately.

The semantics for pattern-matching is derived from that presented in the Haskell report for case expressions (where the semantics was defined as a translation into a Haskell kernel). This gives a less direct semantics than that of, e.g., Standard ML, but we feel this approach is justified because of the extra complications of lazy pattern matching (introduced by ∼ patterns) and guarded patterns.

Rule (23) simplifies multi-argument matches to single-argument matches.

∀i, j. 0 < i ≤ m, 0 < j ≤ n, x_{i} ∉ (fv(pat_{ij}) ∪ fv(grhs_{i}))

E,v ⊧ { x_{1} = \x_{2} = … \x_{n} = case (x_{1}, …, x_{n}) of { (pat_{11}, …, pat_{1n}) grhs_{1} … (pat_{m1}, …, pat_{mn}) grhs_{m}} } ⇒ v’

m ≥ 1, n ≥ 2
E,v ⊧ {pat_{11} … pat_{1n} grhs_{1} … pat_{m1} … pat_{mn} grhs_{m}} ⇒ v’

(23)

Rule (24) simplifies matches into matches of the form {pat = exp = exp’}.

∀i. 1 ≤ i ≤ n, x_{i} ∉ ⋃ (fv(pat_{i}) ∪ fv(grhs_{i}))
pat_{n} grhs_{n} ≠ = exp_{n}

E,v ⊧ \{ \begin{matrix}pat & 1 & grhs & 1 \\ x_{1} = case x_{1} of \{pat_{2} grhs_{2} \\ x_{2} = case x_{2} of \{pat_{3} grhs_{3} … = caseError\} \} \end{matrix} \} ⇒ v’
n ≥ 1
E,v ⊧ {pat_{1} grhs_{1} … pat_{n}grhs_{n}} ⇒ v’

(24)

Rules (25)–(26) simplify guarded matches. Guards are translated into conditional expressions.

E,v ⊧ \{ \begin{matrix}pat = if gd_{1} then exp_{1} else … if gd_{n} then exp_{n} else exp \\ = exp’ \end{matrix} \} ⇒ v’

E,v ⊧ {pat | gd_{1} = exp_{1} | … | gd_{n} = exp_{n} = exp = exp’} ⇒ v’

(25)

E,v ⊧ \{ \begin{matrix}pat = if gd_{1} then exp_{1} else … if gd_{n} then exp_{n} else exp’ \\ = exp’ \end{matrix} \} ⇒ v’ E,v ⊧ {pat | gd_{1} = exp_{1} | … | gd_{n} = exp_{n} = exp’} ⇒ v’

(26)

Rules (27)–(33) define the semantics of variable matches, lazy pattern matches and as-patterns.

x_{0} ∉ fv(exp)

∀i. 1 ≤ i ≤ #fv(pat), x_{i} ∈ fv(pat)

E,v ⊧ {x_{0} = let {x_{i} = case x_{0} of {pat = x_{i}}} in exp} ⇒ v’ E,v ⊧ {∼ pat = exp = exp’} ⇒ v’

(27)

E,v ⊧ {var = case var of {pat = exp}} ⇒ v’ E,v ⊧ {var@pat = exp = exp’} ⇒ v’

(28)

E ⊢ exp ⇒ v’

E,v ⊧ { = exp = exp’} ⇒ v’

(29)

E,v ⊧ {var = exp} ⇒ v’ E,v ⊧ {var : τ = exp = exp’} ⇒ v’

(30)

E,v ⊧ {var = exp} ⇒ v’ E,v ⊧ {var : κ τ = exp = exp’} ⇒ v’

(31)

E,v ⊧ {var = exp} ⇒ v’ E,v ⊧ {var = exp = exp’} ⇒ v’ (32)

E ⊕ {var : v} ⊢ exp ⇒ v’

E,v ⊧ {var = exp} ⇒ v’

(33)

Rules (34)–(42) define the semantics of matches against constructor patterns. Rules (34) and (40) are simplification rules, simplifying general constructor matches and tuple matches, respectively; the remaining rules define the matching semantics. The simplification rules are used to simplify deep pattern matches (such as [1,2]) into single-level matches. Note the explicit use of ⊥ in the matching rules.

∀i, j. 1 ≤ i ≤ n, 0 < j ≤ n, var_{i} ∉ ⋃ (fv(pat_{j}) ∪ fv(exp))

E, v ⊧ { con var_{1} … var_{n} = case var_{1} of {pat_{1} = … case var_{n} of {pat_{n} = exp = exp’} …} } ⇒ v’

E, v ⊧ {con pat_{1} … pat_{n} = exp = exp’} ⇒ v’

(34)

v = con < v_{1}, …, v_{n} >

∀i. 1 ≤ i ≤ n, E ⊕^{→} {var_{i} : v_{i}} ⊢ exp ⇒ v’

E,v ⊧ {con var_{1} … var_{n} = exp = exp’} ⇒ v’

(35)

v ≠ con < v_{1}, …, v_{n} > ∧ v ≠ ⊥

E ⊢ exp’ ⇒ v’

E,v ⊧ {con var_{1} … var_{n} = exp = exp’} ⇒ v’

(36)

v = ⊥

E,v ⊧ {con var_{1} … var_{n} = exp = exp’} ⇒ ⊥

(37)

\begin{matrix}v = <> \\ E ⊢ exp ⇒ v’ \end{matrix}

E,v ⊧ {() = exp = exp’} ⇒ v’ (38)

v = ⊥
E,v ⊧ {() = exp = exp’} ⇒ ⊥

(39)

∀i, j. 0 < i ≤ n, 0 < j ≤ n,
var_{i} ∉ (⋃ ((fv(pat_{j})) ∪ fv(exp))

E, v ⊧ { (var_{1}, …, var_{n}) = case var_{1} of {pat_{1} = … case var_{n} of {pat_{n} = exp = exp’} …} } ⇒ v’

E, v ⊧ {(pat_{1}, …, pat_{n}) = exp = exp’} ⇒ v’

(40)

v = < v_{1}, …, v_{n} >
∀i. 0 < i ≤ n, E ⊕ {var_{i} : v_{i}} ⊢ exp ⇒ v’
E,v ⊧ {(var_{1}, …, var_{n}) = exp = exp’} ⇒ v’

(41)

v = ⊥
E,v ⊧ {(var_{1}, …, var_{n}) = exp = exp’} ⇒ ⊥

(42)

5 Definitions

This section presents the semantics for definitions. These rules are used to derive value environments. Rule (46) defines the semantics for a set of bindings. Since all bindings are recursive, the resulting environment sum can be used to derive the meanings of each individual binding. This is exploited in rule (43), where the environment sum resulting from a set of recursive pattern bindings is used to define the meaning of those bindings.

E ⊢ var match ⇒ {var : ≪ match, E ≫ }  (43)

pat grhs ≠ var = exp

∀i. 1 ≤ i ≤ #fv(pat), var_{i} = fv(pat)
E ⊢ var_{i} = case exp of {pat | gd = var_{i}} ⇒ E_{i}
E ⊢ pat | gd = exp ⇒ ⨁ (∀i. 1 ≤ i ≤ #fv(pat), E_{i})

(44)

E ⊢ exp ⇒ v

E ⊢ var = exp ⇒ {var : v}

(45)

∀i. 1 ≤ i ≤ n, E ⊕ E’ ⊢ def_{i} ⇒ E_{i}
E’ = ⨁ (∀j. 1 ≤ j ≤ n, E_{j})
E ⊢ { def_{1}, …, def_{n}} ⇒ E’

(46)

6 Modules

The meaning of a group of modules is the meaning of the function main from the module Main. This defines a function from responses to requests which is evaluated lazily in the context of an initial operating system state. The result of the evaluation is a series of operating system state transitions which collectively define the visible effect of executing the Haskell program.

All definitions are potentially mutually recursive, so we define their meaning in the value environment which comprises all definitions in the set of modules, plus the initial environment. Note that the use of ⊕ rather than ⊕^{→} ensures that aliasing of original names cannot occur. We assume that modules are consistent: this is enforced by the static semantics.

∀i. 1 ≤ i ≤ n, E’ ⊢ mod_{i} ⇒ E_{i}

E’ = E ⊕ (⨁(∀j. 1 ≤ j ≤ n, E_{i}))

E’ ⊢ originalname (Main, main) ⇒ v

n ≥ 0
E ⊢ {mod_{1}, …, mod_{n}} ⇒ v

(47)

7 Programs and Request Semantics

This section defines the meaning of programs and their interaction with the file-system by means of the Haskell request/response mechanism.

The semantics does not consider the possibility of FormatError when writing the standard channels stdout, stderr or stdecho. Issues of file and channel interdependence are also ignored. All these issues are operating-system dependent. We consider only the required filesystem requests here, optional requests are ignored.

The meaning of a program is defined with respect to S_{0}, the initial state of the filesystem and E_{0}, the initial environment. The initial value of the “echo-processed” flag in S_{0} should be False; that is no Echo request has been issued initially. This flag is set to True after the first echo request or read from the distinguished channel stdin.

The meaning of a set of modules is a closure, which when applied to a list of responses yields a list of requests. The request is applied to the state to determine a response and a new state. Rule (48) defines the meaning of a program. The meaning of the modules comprising the program, mods, will be a closure, v. This closure is evaluated in the context of the initial state S_{0} to give the value result of the program, v’ and a new state S′.

E_{0} ⊢ mods ⇒ v
S_{0} ⊢ v ⇒ v’, S’
E_{0}, S_{0} ⊢ mods ⇒ v’, S’

(48)

Rules (49) and (50) define the meaning of the program if the main function returns ⊥ or a closure, respectively. In the latter case, match is matched against ⊥ to give a list of requests v. This list of requests is then evaluated in the context of the state to give a list of responses v’ and a new state S′.

S ⊢ ⊥ ⇒ ⊥  (49)

E, ⊥ ⊧ match ⇒ v
≪ match, E ≫ , S ⊧ v ⇒ v’, S’
S ⊢ ≪ match, E ≫ ⇒ v’, S’

(50)

Rules (51)–(53) map lists of requests to lists of responses. We use the same semantic list constructor (:) here as elsewhere in this report. Since any component of the list may be ⊥, there are three rules.

The third rule (for (:)) is the most interesting. The first request is evaluated in the context of S to give a response v’ and a new state S′. The response is then matched against match to return a list of requests v”. The first of these requests must be the the same as v. The remaining requests are evalauted in the context of the new state to give a corresponding list of responses, and the associated state, S′′. The operating system is free to transform this state to give a final state S′′′. In a single-tasking system, we might expect this transformation to be the identity function.

⊢^{OS} S ⇒ S’

≪ match, E ≫ , S ⊧ ⊥ ⇒ ⊥, S’

(51)

⊢^{OS} S ⇒ S’

≪ match, E ≫ , S ⊧ Nil <> ⇒ Nil <>, S’

(52)

S ⊢ v ⇒ v’, S’

E, v’ ⊧ match ⇒ v”

v” = (:) < v, vs’ >

≪ match, E ≫ , S’ ⊧ vs’ ⇒ vs”, S”

⊢^{OS} S” ⇒ S”’

≪ match, E ≫ , S ⊧ (:) < v, vs > ⇒ (:) < v”, vs” >, S”

(53)

The remaining rules construct a response and state transition from a request and an initial state, S. To each remaining rule is attached the implicit side condition ⊥ ∉ v_{i}, where the v_{i} are the parameters of the request. Together with rule (51), this ensures that requests (though not responses) are hyper-strict, as required by the Haskell report. The majority of requests have two rules: one used when the request succeeds, and another used when the request fails.

Section 7.1 defines the auxiliary functions read, write, canReadTextChan etc. which are used here.

Rules (54)–(61) define the semantics of reading values from files or channels.

canReadTextChan c S = < Success, s >

S’ = (Channel of S ⊖ c) in (noEcho c S)

S ⊢ ReadChan < c > ⇒ Str < s >, S’

(54)

canReadTextChan c S = < Failure f, s >

S’ = (Channel of S ⊖ c) in (noEcho c S)

S ⊢ ReadChan < c > ⇒ Failure f, S’ (55)

canReadBinChan c S = < Success, b > S’ = (Channel of S ⊖ c) in (noEcho c S) S ⊢ ReadBinChan < c > ⇒ Bn < b >, S’

(56)

canReadBinChan c S = < Failure f, b > S’ = (Channel of S ⊖ c) in (noEcho c S) S ⊢ ReadBinChan < c > ⇒ Failure f, S’

(57)

canReadTextFile f S = < Success, s > S ⊢ ReadFile < f > ⇒ Str < s >, S

(58)

canReadTextFile f S = < Failure v, s > S ⊢ ReadFile < f > ⇒ Failure v, S

(59)

canReadBinFile f S = < Success, b > S ⊢ ReadBinFile < f > ⇒ Bn < b >, S

(60)

canReadBinFile f S = < Failure v, b > S ⊢ ReadBinFile < f > ⇒ Failure v, S

(61)

Rules (62)–(73) define the semantics of writing or appending values to files or channels.

canWriteTextChan c S s = < Success, v >

S’ = (Channel of S) ⊕^{→} {c : v} S ⊢ AppendChan < c, s > ⇒ Success, S ⊕^{→} S’

(62)

canWriteTextChan c S s = < Failure f, v > S ⊢ AppendChan < c, s > ⇒ Failure f, S (63) canWriteBinChan c S s = < Success, v >

S’ = (Channel of S) ⊕^{→} {c : v}

S ⊢ AppendBinChan < c, s > ⇒ Success, S ⊕^{→} S’

(64)

canWriteBinChan c S True s = < Failure f, v > S ⊢ AppendBinChan < c, s > ⇒ Failure f, S

(65)

canWriteTextFile f S True s = < Success, v >

S’ = (File of S) ⊕^{→} {f : v} S ⊢ AppendFile < f, s > ⇒ Success, S ⊕^{→} S’

(66)

canWriteTextFile f S True s = < Failure v, v’ > S ⊢ AppendFile < f, s > ⇒ Failure v, S

(67)

canWriteBinFile f S True s = < Success, v >

S’ = (File of S) ⊕^{→} {f : v}

S ⊢ AppendBinFile < f, s > ⇒ Success, S ⊕^{→} S’

(68)

canWriteBinFile f S True s = < Failure v, v’ > S ⊢ AppendBinFile < f, s > ⇒ Failure v, S

(69)

canWriteTextFile f S False s = < Success, v >

S’ = (File of S) ⊕^{→} {f : v} S ⊢ WriteFile < f, s > ⇒ Success, S ⊕^{→} S’

(70)

canWriteTextFile f S False s = < Failure v, v’ > S ⊢ WriteFile < f, s > ⇒ Failure v, S (71) canWriteBinFile f S False s = < Success, v >

S’ = (File of S) ⊕^{→} {f : v}

S ⊢ WriteBinFile < f, s > ⇒ Success, S ⊕^{→} S’

(72)

canWriteBinFile f S False s = < Failure f, v > S ⊢ WriteBinFile < f, s > ⇒ Failure f, S

(73)

Rules (74)–(83) handle miscellaneous requests.

canDeleteFile f S = Success

S ⊢ DeleteFile < f > ⇒ Success, ((File of S) ⊖ f) in S

(74)

canDeleteFile f S = Failure v S ⊢ DeleteFile < f > ⇒ Failure v, S

(75)

statusString f S = v S ⊢ StatusFile < f > ⇒ v, S

(76)

statusChanString c S = v S ⊢ StatusChan < c > ⇒ v S

(77)

S ⊢ GetProgName ⇒ Str < Prog of S >, S  (78)
S ⊢ GetArgs ⇒ StrList < Args of S >, S  (79)

s ∈ dom (Environ of S)

s’ = (Environ of S) s

S ⊢ GetEnv < s > ⇒ Str < s’ >, S

(80)

s ∉ dom (Environ of S)

S ⊢ GetEnv < s > ⇒ envError s, S

(81)

S’ = (Environ of S) ⊕^{→} { s : s’}
S ⊢ SetEnv < s, s’ > ⇒ Success, S ⊕^{→} S’

(82)

S′ = doEcho v S

S ⊢ Echo < v > ⇒ Success, S’

(83)

7.1 Auxiliary File-System Functions

This section defines the auxiliary functions which are used when defining the semantics of filesystem requests. read, write, etc. determine whether a file is readable, writable etc. according to the status recorded within the filesystem. readc, writec perform similar operations for channels.

read < v, , , , > = v readc < v, , , > = v
write < , v, , , > = v writec < , v, , > = v

delete < , , v, , > = v

text < , , , v, > = v textc < , , v, > = v
bin < , , , , v > = v  binc < , , , v > = v

We also define some auxiliary functions which are used when returning error values. OSErr constructs an operating-system specific error message from a string and error value.

readError s v =  Failure (ReadError (OSErr s v))
writeError s v = Failure (WriteError (OSErr s v))
searchError s v = Failure (SearchError (OSErr s v))
formatError s v = Failure (FormatError (OSErr s v))
otherError s v = Failure (OtherError (OSErr s v))
envError v =  searchError “Environment variable does not exist” v

canRWFile determines whether the file f can be read or written (depending on the value of w) as a binary or text file (depending on the settings of b and t). If a is True then s’ is appended to the current contents of the file, otherwise s’ replaces the current file contents in the filesystem. OScanCreate and OScreateStatus are operating-system dependent functions which determine whether the file can be created, and if so its initial status, respectively.

canRWFile f S w b t a s’ =

f ∈ dom (File of S) →

< testReadWrite ∧ testBinText → Success; readWriteErrorMesg,

< v, ifWriteThenTestAppend >> ; < w ∧ ¬a ∧ OScanCreate f S b t → Success; readCreateErrorMesg,

< OScreateStatus f S b t, s’ >>

where < v, s > = (File of S) f testReadWrite = w → write v; read v testBinText = (b → bin v; True) ∧ (t → text v; True) readWriteErrorMesg = w → writeError “can’t write file” f;

readError “can’t read file” f

ifWriteThenTestAppend = w → (a → s ++ s’; s’); s

readCreateErrorMesg = w → writeError “can’t create file” f;

readError “file does not exist” f

canWriteTextFile, canWriteBinFile etc. are packaged versions of canRWFile for the obvious cases.

canWriteTextFile f S a s = canRWFile f S True False True a s
canWriteBinFile f S a s = canRWFile f S True True False a s
canReadTextFile f S a s = canRWFile f S False False True a s
canReadBinFile f S a s = canRWFile f S False True False a s

canRWChan is analogous to canRWFile, but for channels. Values written to channels are always appended to the current contents, and channels can never be created.

canRWChan c S w b t s’ =

c ∈ dom (Channel of S) →

< (w →writec; readc) v ∧ bt v → Success;

(w →writeError “can’t write channel” c; readError “can’t read channel” c),

< v, w → s ++s’;s >> ;

searchError “channel does not exist” c

where < v, s > = (Channel of S) c bt v = (b → binc v; True) ∧ (t → textc v; True)

canWriteTextChan etc. are packaged versions of canRWChan analagous to canWriteTextFile etc.

canWriteTextChan c S s = canRWChan c S True False True s
canWriteBinChan c S s = canRWChan c S True True False s
canReadTextChan c S s = canRWChan c S False False True s
canReadBinChan c S s = canRWChan c S False True False s

statusString constructs a string representing the status of a file from the filesystem information. OSstatusFile extends the standard string with operating-system specific information.

statusString f S =

f ∈ dom (File of S) →

Str < (:) < fileType, (:) < readStatus, (:) < writeStatus, OSstatusFile f S >>>> ;

searchError “file does not exist” f

where < v, > = (File of S) f fileType = text v ∧ ¬bin v → ‘t’; bin v ∧ ¬text v → ‘b’;

text v ∨ bin v → ‘f’; OSisDirectory f S → ‘d’; ‘u’

readStatus = read v → ‘r’; ‘-’ writeStatus = write v → ‘w’; ‘-’

statusChanString is similar, but returns status information about a channel. OSStatusChan is used to return the status information if the channel exists, otherwise Failure is returned.

statusChanString c S = f ∈ dom (Channel of S) → Str (OSStatusChan c S);

searchError “channel does not exist” c

canDeleteFile returns either Success if the named file can be deleted or a Failure.

canDeleteFile f S =

f ∈ dom (File of S) →

delete v → Success; writeError “cannot delete file” f;

searchError “file does not exist” f

where < v, s > = (File of S) f

doEcho returns either Success and a new state if echoing is permissible or Failure and the existing state.

doEcho v S =

n → otherError “cannot set echo”;

Success, < v, False > in (Echo of S) where < e, n > = (Echo of S) noEcho sets the flag in the state which causes further Echo requests to fail.

noEcho c S = c = stdin → < e, False > in (Echo of S); S where < e, n > = (Echo of S)

8 Operating System Functions

In writing this semantics, we have assumed the existence of a number of operating system specific functions. These functions are listed in the following table.

Function  Result

OScanCreate file State bin text

True if file can be created in State as a binary and/or text file (as determined by the bin/text predicates), otherwise False.

OScreateStatus file State bin text

A list of characters representing the initial status of a newly created file, as used by the StatusFile request.

OSstatusFile file State

A list of characters containing OS-specific status information about a file, as used by the StatusFile request.

OSstatusChan chan State

A list of characters containing OS-specific status information about the channel chan (for stdout, stderr and stdecho the initial segment of the string should be the maximum line length and the maximum page length allowed for the channel as two separate integers, separated by a single space).

OSisDirectory file State

True if file is a directory in state State, False otherwise.

OSErr string value

An OS-specific error message for error string with parameter value.

9 The Initial Environment

The initial environment comprises definitions for all functions and constructors defined in the module PreludeCore. These values must be available in all Haskell programs. The meanings of other Prelude functions is defined by reference to the Haskell report, which provides a source language definition. We assume that the meaning of basic operations (such as addition on numbers) is obvious. To define this formally would be tedious in the extreme.

The initial environment contains the following functions (BasVal)

PrimPlusInt : \a -> \b -> a + b + is fixed-precision integer addition
PrimMulInt : \a -> \b -> a × b × is fixed-precision integer multiplication
…
error : \s -> ⊥  the error function

plus the standard constructors (BasCon):

0, 1, …, 0.0, 0.1, …, True, False, ’a’, …, (:), Nil, ReadFile, ReadBinFile, ReadChan, ReadBinChan, WriteFile, WriteBinFile, AppendFile, AppendBinFile, AppendChan, AppendBinChan, StatusChan, StatusFile, DeleteFile, GetEnv, SetEnv, GetProgName, GetArgs, Echo, Success, Failure, Str, StrList, Bn, ReadError, WriteError, SearchError, FormatError, OtherError

The characters correspond to those defined by the ASCII character set. The mapping from syntactic variables to semantic constructors is the obvious one, that is, E_{0} (SetEnv) = SetEnv . . ..

References

[HW90] Hudak, P and Wadler, PL (eds), “Report on the Programming Language Haskell, Version 1.0”, Universities of Yale and Glasgow, April 1990.

[HJW91] Hudak, P, Peyton Jones SL, and Wadler, PL (eds), “Report on the Programming Language Haskell, Version 1.1”, Universities of Yale and Glasgow, August 1991.

[HJW92] Hudak, P, Peyton Jones SL, and Wadler, PL (eds), “Report on the Programming Language Haskell, Version 1.2”, SIGPLAN Notices, March 1992.

[JW92] Peyton Jones, SL and Wadler, PL, “The Static Semantics of Haskell”, Unpublished Technical Report, Universitry of Glasgow, 1992.

[HMT91] Harper, Milner and Tofte, The Definition of Standard ML, MIT Press, 1991.