Under consideration for publication in J.Functional Programming1
Exceptional Syntax
NICK BENTON and ANDREW KENNEDY
Microsoft Research,St.George House,1Guildhall Street,Cambridge CB23NH,UK
(e-mail:{nick,akenn}@https://www.doczj.com/doc/086274254.html,)
Abstract
From the points of view of programming pragmatics,rewriting and operational semantics, the syntactic construct used for exception handling in ML-like programming languages, and in much theoretical work on exceptions,has subtly undesirable features.We propose and discuss a more well-behaved construct.
Capsule Review
The propositions-as-types principle has often been cited as an in?uence on the design of functional programming languages.Often the in?uence is seen only indirectly.In this short note the authors draw lessons from the proof theory of disjunction to suggest changes to the syntax of exception constructs that not only improve their utility in programming, but also admit simpler expression of common program transformations.
1Introduction
Many programming languages(from Mesa and PL/I to SML,Java and C#)include exceptions to provide a structured,but non-local,way of signalling and recovering from error conditions.Programmers often also use exceptions as convenient,and sometimes more e?cient,way of varying control?ow in code which has nothing to do with what most people would consider error-handling(for example,the parser combinators in(Paulson,1991)).
The basic idea of exceptions is simple and familiar:the evaluation of an expression may,instead of completing normally by returning a value or diverging,terminate abnormally by raising a named exception.The evaluation of any expression may be wrapped in an exception handler,which provides an alternative expression to be evaluated in the case that the wrapped expression raises a particular exception. The way in which a raised exception unwinds the evaluation stack until the closest matching handler is found is syntactically implicit,so the handler may be dynam-ically far from the point at which the exception is raised without the intervening calls having explicitly to test for,and propagate,an error value.
There are many di?erences between exception mechanisms in di?erent program-ming languages,but for the purposes of this paper we shall take a simpli?ed version of the constructs provided in Standard ML(Milner et al.,1997)as paradigmatic of those used in modern expression-based languages.To the usual simply-typed
2Nick Benton and Andrew Kennedy
lambda calculus we add a set E of exception names,a new base type exn,and new constructs with the typing rules
Γ E:exn E∈E
Γ M:exn
Γ raise M:A
Γ M:A{Γ N i:A}i=1...n
Γ M handle E1?N1|···|E n?N n:A
{E i}i=1...n?E
where,in the last rule,the E i are required to be distinct.We take as basic a form of handle in which multiple handlers may cover the evaluation of a single expression, as this is strictly more expressive than the simpler form in which only one named exception may be caught at once.We will sometimes use an abbreviated notation, using H to range over?nite sets{E i?N i}of handlers,and writing E∈H for ?N.(E?N)∈H and H(E)for the(unique)N such that(E?N)∈H if that exists.We writeΓ H:A for H={E i?N i}and?i.Γ N i:A.
One way of explaining the intended behavior of these constructs is to give a big-step operational semantics in which there are two(mutually inductive)forms of judgement:M?V means that the closed expression M evaluates to the value V, whereas M↑E means that the expression M raises the exception E.The rules for deriving these judgements comprise the usual evaluation rules for a call by value lambda calculus1together with at least the following:
E?E E∈E
M?E (raise M)↑E
M?V
(M handle H)?V
M↑E
(M handle H)↑E
E∈H
M↑E N?V (M handle H)?V
H(E)=N
M↑E N↑E
(M handle H)↑E
H(E)=N M↑E
(M N)↑E M?λx.M N↑E (M N)↑E
There will be further rules,similar to the last two above,which express the way in which thrown exceptions propagate through whatever other constructs we choose to add to our language.
We became aware of essentially the same shortcoming of the handle construct in three di?erent ways whilst working on our Standard ML compiler,MLj(Benton et al.,1998a).Firstly,when coding in SML to implement both the compiler itself and its libraries,we occasionally came across situations in which exception-handling behaviour could only be expressed clumsily.Secondly,when performing rewriting on the compiler intermediate language,we found that some rewrites were inexpress-ible if the intermediate language contained the usual exception handling construct. 1We restrict attention to call by value,as the na¨?ve addition of exceptions to a language with call by name semantics wrecks the equational theory to the extent that the resulting language is essentially unusable.The ingenious addition of imprecise exceptions to Haskell does,however, sidestep some of the problems;see(Peyton Jones et al.,1999)for details.
Exceptional Syntax3
Γ M:AΓ,x:A P:B{Γ N i:B}i=1...n≥0
Γ try x?M in P unless E1?N1|···|E n?N n:B
{E i}i=1...n?E
M?V P[V/x]?V try x?M in P unless H?V
M↑E N?V
try x?M in P unless H?V
H(E)=N
M?V P[V/x]↑E try x?M in P unless H↑E
M↑E N↑E
try x?M in P unless H↑E
H(E)=N M↑E
try x?M in P unless H↑E
E∈H
Fig.1.Typing rule and natural semantics for try
Thirdly,when formalising the intermediate language in order to prove some theo-rems about the validity of optimising transformations(Benton&Kennedy,1999), we found that the alternative syntax we had chosen(for the previous reason)al-lowed a neat and tractable presentation of the operational semantics in terms of a structurally inductive termination predicate,which would not otherwise have been possible.
2The New Construct
Since the?x for the problems we observed is actually rather simple,and to avoid building unnecessary suspense in the reader,we will reverse the usual order of presentation by giving our solution straight away and then going into the more technical explanations of the problems it solves.
We replace the ML-style handle construct with a new one,which builds in a continuation to be applied only in the case that no exception is raised:
try x?M in P unless E1?N1|···|E n?N n
This?rst evaluates M and,if it returns a value,binds that to x and evaluates P. If M raises the exception E i,however,N i is evaluated instead(x is bound in P but not in any of the N i).If M raises an exception distinct from all the E i,then so does the whole expression.
More formally,Figure1presents a typing rule2for try along with its natural semantics rules.Note that we?nd it convenient to allow empty handlers in this construct and that the type of the expressions N i in a handler is the same as that of the continuation P,not the same as that of the expression M being covered,as is the case with the traditional handle.
2The typing rule for try in our intermediate language is actually a little more complex since it involves computation types(Benton&Kennedy,1999).
4Nick Benton and Andrew Kennedy
3So What Was Wrong With handle?
We now describe the problem with the traditional handle construct in each of the three contexts in which we observed it.To avoid dragging in too much extraneous material concerning,for example,our compiler intermediate language,we will of-ten gloss over the non-exceptional details of the various languages mentioned:this should not(we hope!)obscure our main point.
3.1The Programming Problem
Suppose one has a library of ML functions to open,read and close?les,all of which raise the Io exception if something goes wrong.The problem is to write a function which runs down a list of?lenames,concatenating the results of applying some string-valued function to each?le whilst skipping those?les which cannot be opened successfully.One’s?rst thought might be that the following will su?ce: fun catpartial[]=""
|catpartial(n::ns)=
let val s=readIt(openIn n)
handle Io=>""
in s^catpartial ns
end
However,this doesn’t quite do what we want,as the function readIt might also raise the Io exception:when that happens then we want the exception to be passed up to the caller of catpartial,but the above code will handle the exception and move on to the next name in the list irrespective of whether the error occured in openIn or readIt.
There are,of course,various straightforward ways of programming around this problem.For example,we might use the option datatype:
fun catpartial1[]=""
|catpartial1(n::ns)=
case SOME(openIn n)handle Io=>NONE
of NONE=>catpartial1ns
|SOME f=>readIt f^catpartial1ns
Or use abstraction to delay the call to readIt so that the handler doesn’t cover it: fun catpartial2[]=""
|catpartial2(n::ns)=
(let val f=openIn n
in fn()=>readIt f^catpartial2ns
end handle Io=>fn()=>catpartial2ns
)()
Or use another exception:
Exceptional Syntax5 exception OpenFailed
fun catpartial3[]=""
|catpartial3(n::ns)=
let val f=openIn n handle Io=>raise OpenFailed
in readIt f^catpartial3ns
end handle OpenFailed=>catpartial3ns
But none of these seems entirely satisfactory as they all introduce a new value(sum, closure or exception)only to eliminate it straight away–it’s just there to express some control?ow which the handle construct is too weak to express directly.
The?x:Programming with try
The try-in-unless syntax nicely solves our programming problem:
fun catpartial[]=""
|catpartial(n::ns)=try val f=openIn n
in readIt f^catpartial ns
unless Io=>catpartial ns
end
and also generalises both let and handle:
let x?M in N=try x?M in N unless{}
M handle H=try x?M in x unless H
3.2The Transformation Problem
Like many compilers for functional languages,MLj performs fairly extensive rewrit-ing in order to optimise programs.The design of MLj’s intermediate language,MIL, and its rewrites is motivated by a somewhat informal belief in‘taking the proof theory seriously’.One instance of this prejudice is that the compiler transforms programs into a‘cc-normal form’,in which all of the commuting conversions have been applied.
In natural deduction presentations of logics(and hence,via the Curry-Howard correspondence,in typed lambda calculi),commuting conversions occur when logi-cal rules(usually eliminations)have what Girard(1989)calls a‘parasitic formula’, a typical case being that of the sum.The elimination rule for sums is
Γ M:A+BΓ,x1:A N1:CΓ,x2:B N2:C
Γ case M of in1x1.N1|in2x2.N2:C
in which the formula/type C has no connection with that being eliminated.The presence of such rules introduces undesirable distinctions between proofs and also, for example,causes the subformula property of normal deductions to fail.These problems are addressed by adding commuting conversions to the more familiarβ
6Nick Benton and Andrew Kennedy
andηhttps://www.doczj.com/doc/086274254.html,muting conversions typically have the general form
···A ··
·
C···
··
·
C
E1
C···
E2
D
;
··
·
A
··
·
C···
E2
D···
··
·
C···
E2
D
E1
D
where E1is the‘bad’elimination rule for the top-level connective in A,with par-asitic formula C(which may occur one or more times as a premiss,according to the connective being eliminated),and E2is the elimination rule for the top-level connective in C.For example,if E1is∨-elimination and E2is→-elimination,we get the following commuting conversion on terms:3
(case M of in1x1.N1|in2x2.N2)P
;case M of in1x1.(N1P)|in2x2.(N2P).
(Here and elsewhere,we adopt the‘variable convention’:su?cientα-conversion to avoid unwanted variable capture is assumed.In the above,this implies that neither x1nor x2is free in P.)Commuting conversions often enable further reductions which would otherwise be blocked,as in
(case M of in1x1.λy.y+x1|in2x2.λy.y)2
;case M of in1x1.((λy.y+x1)2)|in2x2.((λy.y)2)
;case M of in1x1.(2+x1)|in2x2.2
and we also?nd generating code from cc-normal forms considerably more straight-forward than for arbitrary terms.Other compilers perform similar rewrites(for example,the case-of-case and let-?oating transformations in(Peyton Jones&San-tos,1998)),though we are unusually dogmatic in recognising them as instances of a common pattern and peforming all of them.
Interestingly,cc-normal form for our intermediate language,which is based on Moggi’s computational metalanguage(Moggi,1991),turns out to be almost the same thing as Sabry and Felleisen’s A-normal form(Sabry&Felleisen,1993;Flana-gan et al.,1993),which was derived from an analysis of CPS-based compilation.A nice discussion of the connection between CPS and Moggi’s metalanguage may be found in(Hatcli?&Danvy,1994).
For most of the type constructors of our intermediate language,MIL,we have well-behaved introduction and elimination rules for which it is clear how to derive the commuting conversions.For the exception-related constructs,the situation is messier(since part of the point of exceptions is that they are not explicitly visible in source-language types)but it is nevertheless obvious that there are some cc-like rewrites which we would like to perform.For example
(M handle E?N)P
3Applied na¨?vely,of course,the duplication of terms in conversions like this one could lead to an unacceptable blowup in code size.MLj avoids this by selective use of a special abstraction construct which compiles to a block of code accessed by jumps.
Exceptional Syntax7 looks as though it should convert to something like
(M P)handle E?(N P)
so that if,for example,N is aλ-abstraction,we get to perform a compile-time β-reduction.But this transformation is not generally sound if either P or the appli-cation of the value of M to the value of P might raise the exception E.Furthermore, there isn’t a correct transformation which we can use instead.It should be remarked at this point that the limited expressibility of an intermediate language based on aλ-calculus with handle is not shared by lower-level target https://www.doczj.com/doc/086274254.html,ing Java bytecodes,for example,a code sequence corresponding to a correct version of the above transformation is easily written:
L1:Code to evaluate M
L2:Code to evaluate P
invokevirtual
L3:Code for rest of computation
L4:pop//throw away the actual exception object
Code to evaluate N
Code to evaluate P
invokevirtual
jmp L3
Exception table:
from to target type
L1L2L4
and the same is true of target languages in which exception handlers are explicitly pushed onto and popped from a stack.
In fact,because of the separation of computations from values in MIL,we would have to express the?rst term above as
let f?(M handle E?N)in let v?P in(f v)
but the essential point remains unchanged:there’s simply no correct way to write the transformation which we feel we should be able to perform.
Of course,one could simply accept the inexpressibility of such transformations and generate slightly lower quality code.Alternatively,one can observe that the commuting conversions are not in themselves generally optimisations;they are re-organisations of the code which enable more computationally signi?cantβredexes to be exposed.Hence the same optimisations might well be obtained by using non-local rewrites which look for larger patterns in the term.This would,however,sig-ni?cantly increase the complexity of the rewriting function and,we believe,would make it less e?cient(despite the fact that the non-local steps would combine the e?ect of more than one local rewrite).
8Nick Benton and Andrew Kennedy
πj(try x?M in P unless{E i?N i})proj-try ;try x?M inπj(P)unless{E i?πj(N i)}
(try x?M in P unless{E i?N i})Q app-try ;try x?M in(P Q)unless{E i?(N i Q)}
case(try x?M in P unless{E i?N i})of in1y1.Q1|in2y2.Q2case-try ;try x?M in case P of in1y1.Q1|in2y2.Q2
unless{E i?case N i of in1y1.Q1|in2y2.Q2}
try x?(case M of in1y1.N1|in2y2.N2)in Q unless{E i?P i}try-case ;try z?M in
case z of in1y1.try x?N1in Q unless{E i?P i}|
in2y2.try x?N2in Q unless{E i?P i}unless{E i?P i}
try x?(try y?M in P unless{E i?N i}i∈I)in Q unless{E j?N j}j∈J try-try ;try y?M in
try x?P in Q
unless{E j?N j}j∈J
unless{E i?try x?N i in Q
unless{E j?N j}j∈J}i∈I∪{E j?N j}E
∈{E i}i∈I
j
Fig.2.Conversions
The?x:Rewriting with try
The try-in-unless syntax comes with unsurprisingβ-like reductions,similar to those for handle and let
try x?raise E in P unless H;N(N=H(E))
try x?raise E in P unless H;raise E(N∈H)
try x?V in P unless H;P[V/x](V a value)
but,unlike handle,also has well-behaved commuting conversions,which allow us to express useful compiler transformations.We present in Figure2a general list of conversions for try-in-unless against itself and the eliminations for sums,products and functions.Although these look complex,it should be noted that in a language like MIL(which separates values from computations at both the type and term levels)or that of(Pitts,1997)(which has term-level restrictions on the places where non-values may occur),most of these cases either do not occur or only occur in a simpli?ed form.In MIL,for example,only try-case and try-try are well typed, because projection,application and case can only be applied to values,whereas a try is always a computation.Furthermore,the restriction that M in the try-case
Exceptional Syntax9 rewrite be a value simpli?es it to
(try-case’):
try x?(case V of in1y1.N1|in2y2.N2)in Q unless{E i?P i}
;case V of in1y1.try x?N1in Q unless{E i?P i}|
in2y2.try x?N2in Q unless{E i?P i}
The try-in-unless construct is the one which we use in MIL,and the MLj compiler actually does perform the try-try and try-case’rewrites.
As an interesting example of MIL rewriting,showing the try construct working with our monadic e?ect analysis(Benton&Kennedy,1999),consider the following ML function for summing all the elements of an array:
fun sumarray a=
let fun s(n,sofar)=let val v=Array.sub(a,n)
in s(n+1,sofar+v)
end handle Subscript=>sofar
in s(0,0)
end
Because the SML source language doesn’t have try,the programmer has made the handler cover both the array access and the recursive call to the inner function s. But this would prevent a na¨?ve compiler from recognising that call as tail-recursive. In MLj,the intermediate code for s looks like(in MLish,rather than MIL,syntax): fun s(n,sofar)=
try val x=try val v=Array.sub(a,n)
in s(n+1,sofar+v)
unless{}
end
in x
unless Subscript=>sofar
end
The try-try rewrite turns this into
fun s(n,sofar)=try val v=Array.sub(a,n)
in try val x=s(n+1,sofar+v)
in x
unless Subscript=>sofar
end
unless Subscript=>sofar
end
(The two identical handlers are actually abstracted as a shared local block.)The e?ect analysis detects that the recursive call to s cannot,in fact,ever throw the Subscript exception,so the function is rewritten again to
fun s(n,sofar)=try val v=Array.sub(a,n)
in s(n+1,sofar+v)
10Nick Benton and Andrew Kennedy
unless Subscript=>sofar
end
which is tail recursive,and so gets compiled as a loop in the?nal code for sumarray.
3.3The Semantics Problem
There are several di?erent styles in which one can specify the operational semantics of ML-like languages.We have already seen(in Section1)a big-step,natural se-mantics presentation,but this is not always the most convenient formulation with which to work when proving results about observational equivalences.A popular alternative is to use a small-step semantics presented using Felleisen’s notion of evaluation context(Felleisen&Hieb,1992).In this style,one?rst de?nes axioms for the primitive transitions R→M,saying that redex R reduces to term M,and then gives an inductive de?nition of evaluation contexts as terms E[·]containing a single‘hole’in the place where the next reduction will take place.A simple lemma that every non-value is uniquely of the form E[R]then allows the one-step transi-tion relation to be de?ned as E[R]→E[M]for every evaluation context E[·]and primitive transition R→M(and the evaluation relation to be de?ned in terms of the re?exive transitive closure of the transition relation).Wright and Felleisen (1994)give an evaluation context semantics for ML with exceptions which uses a second kind of context for propagating exceptions.
Pitts has argued(1997)that for reasoning about contextual equivalences it is convenient to reify the notion of evaluation context and give a small-step operational semantics in which a con?guration is a pair of a term and an explicit context (continuation).The advantages of this approach include the fact that the right-hand sides of transitions are all de?ned by structural induction over the left-hand side and that there is a Galois connection between relations on terms and relations on contexts which has proved useful in reasoning about,for example,equivalence of polymorphic functions.This style of presentation is also particularly natural if the language includes?rst-class continuations,in the style of Scheme or SML/NJ (see(Harper et al.,1993),for example).
Pitts formalises contexts by introducing new syntactic categories for de?ning continuation stacks:a con?guration looks like
(x1).N1?···?(x n).N n,M
where M is the term being evaluated(in aλ-calculus with a strict let construct and a restriction that only values and variables may occur in eliminations)and (x1).N1?···?(x n).N n is a sequence of(closed)abstractions representing the context in which the evaluation takes place.The rules de?ning the transition relation include
K?(x).N,V → K,N[V/x]
K,let x?M in N → K?(x).N,M
K,(λx.M)V → K,M[V/x]
Exceptional Syntax11 which,it should be apparent,amounts to de?ning a kind of abstract machine.4 This style of semantics has been applied in(Pitts,2000;Pitts&Stark,1998;Bier-man,1998),and the relational operators it induces are further discussed in(Abadi, 2000).Coincidentally,the current implementation of MLj uses essentially the same representation internally for e?cient rewriting of terms in context.
Pitts gives the relationship between the stack-based semantics and a natural semantics using the following lemma:For all appropriately-typed,closed K,M and V
K,M →? ·,V ??K@M?V
where·is the empty continuation stack and the‘unwinding’operator@is de?ned by
·@M=M
(K?(x).N)@M=K@(let x?M in N).
Note how the place where the action(reduction)happens is at the root of the syntax tree of a stack con?guration but buried deep in that of its unwinding,as
((x1).N1?···?(x n).N n)@M
=let x1?(
let x2?
(...(let x n?M in N)...) in N2)
in N1
It is straightfoward to extend Pitts’s semantics to a language with exceptions: one simply allows(closed)handlers H(which we previously introduced as an abbre-viation for part of the syntax of the handle construct and are now making slightly more?rst-class)to appear as a new kind of element in continuation stacks,with the new transitions
K?H,V → K,V
K?H,raise E → K,N if H(E)=N
K?H,raise E → K,raise E if E∈H
K?(x).N,raise E → K,raise E
K,M handle H → K?H,M
4Actually,since Pitts is interested in which con?gurations lead to termination,for reasoning about contextual equivalence,the one-step transitions are implicit in inference rules de?ning the termination predicate directly,such as
K,N[V/x]
K?(x).N,V
.
12Nick Benton and Andrew Kennedy
The connection with the natural semantics extends to
K,M →? ·,raise E ??K@M↑E
where the de?nition of@is extended by
(K?H)@M=K@(M handle H)
and this is the formulation we initially used when working on the equational theory of MIL.However,there is a certain amount of clutter involved in using stacks (extra syntax,type rules,etc.),and we noticed that if one’s syntax is su?ciently well-behaved then it is possible to obtain an equally tractable presentation of the transition relation just using terms of the original language.For Pitts’s language without exceptions,the idea is to axiomatise directly transitions between terms of the form let x?M in N by using commuting conversion transitions to‘bubble up’the next redex in M until it is at the top(and its surrounding context within M has been pushed into N).For example:
let x?V in N→let y?N[V/x]in y(N=x) let x?(let y?M in N)in P→let y?M in let x?N in P
let x?(λy.M)V in N→let x?M[V/y]in N
Using this style of presentation,the relationship between the big-step and small-step semantics becomes
(let x?M in x)→?(let x?V in x)??M?V.
Intuitively,the stack-free transition relation is de?ned directly on a variant of Pitts’s ‘unwound’terms,in which the let s associate the other way around from the original de?nition:
(K?(x).N)@M=let x?M in(K@N).
The equivalence of the two de?nitions of@depends on the validity of the associativ-ity of let(which,as discussed in(Benton et al.,1998b),is a commuting conversion in the logic corresponding to Moggi’s computational metalanguage).
However,if we add exceptions and the handle construct,the de?nition of the stack-free transition relation fails to extend.Once again,the problem is the lack of commuting conversions which would allow an exception handler to be pushed into a surrounding context so that the evaluation of the expression convered by the handler‘bubbles’to the top.More concretely,consider the following putative transition:
let x?(M handle E?N)in P→?
We’d like to put something on the right-hand side in which the evaluation of M is at the top of the syntax tree,but there’s no rewrite to anything of the form let x?M in....Nor can we extend the collection of top-level forms to include handle as well as let constructs:there’s no rewrite to something of the form M handle E?... either.
Exceptional Syntax13 try x?V in P unless H→try y?P[V/x]in y unless{}(P=x) try x?raise E in P unless H→try y?H(E)in y unless{}
try x?(λy.M)V in P unless H→try x?M[V/y]in P unless H
try x?(try y?M in P unless H)in Q unless H
→try y?M in(try x?P in Q unless H )unless(H catch H in x.Q) {E i?N i}catch{E j?N j}in x.Q def={E i?try x?N i in Q unless{E j?N j}}
∪{E j?N j| ?i.E i=E j}
Fig.3.Transition semantics
The?x:Operational semantics with try
If our language includes try-in-unless,then there is no di?culty in giving a stack-free presentation of a structurally inductive transition semantics.Figure3presents transitions between terms of the form try x?M in P unless H(recall that try-in-unless generalises let).The syntax(H catch H in x.Q)is an abbreviation for the covering of one handler by the other handler and continuation used in the try-try conversion(as in Figure2).
The connection between the transition semantics and the big-step semantics is then expressed by
M?V??try x?M in x unless{}
→?try x?V in x unless H
M↑E??try x?M in x unless{}
→?try x?raise E in P unless H(E∈H)
This formulation of the transition semantics is the one which we have used when reasoning about observational congruence for MIL in order to validate e?ect-based transformations(Benton&Kennedy,1999).5
4Remarks on Concrete Syntax
Using try-in-unless in theoretical work or in a compiler intermediate language is straightforward.But adding the construct to a programming language requires a human-friendly concrete syntax to be chosen and,annoyingly,there doesn’t seem to be an obviously‘right’choice here.The main problem is choosing whether the handlers or the continuation expression should come?rst,i.e.between
try x=M try x=M
in N unless E=>P
unless E=>P and in N
end end
5Though,embarassingly,the HOOTS paper gives an incorrect shorthand for one handler covering another in the operational semantics.
14Nick Benton and Andrew Kennedy
Neither of these is entirely satisfactory.In the?rst case the fact that the handler only covers M and not N is obscured;this is particularly bad if N is large.In the second,that x is bound in N but not in P is certainly not what one would expect. Our own preference for SML is?rstly to retain the handle construct in the source syntax,since it is simpler and su?ces for most situations,and then either to add the?rst alternative above or(more radically)to allow both of them.Since try-in-unless generalises let,it also seems sensible to do without the try keyword and just allow unless to be an optional part of let-expressions.We have tweaked MLj so that it will accept syntax like the following:
fun f((n1,n2)::rest)=
let val s1=openIn n1
val s2=openIn n2
in combine(s1,s2)
unless Io=>f rest
end
Note that SML allows multiple sequential declarations in a single let expression. None of the variables in the left-hand sides are bound in the handler,which is evaluated if any of the right-hand sides raise a matching exception.
5Remarks on Try-Finally
Some imperative languages have a try statement which allows execution of a com-mand to be covered not only by a set of handlers,but also by an optional?nally clause.This speci?es a command which is to be executed once control has left the covered command(and any of the handlers),irrespective of whether the exit was normal or by raising an exception.The try-(catch)-?nally construct is typically used for imperative‘cleanup’code which needs to be executed whether or not an error occurs,the usual example being closing open?les.
One way to extend ML with a similar feature would be by new syntax M finally N,the typing rule for which requires N to be of type unit,and whose behaviour may be speci?ed by the translation:
let val x=M handle e=>(N;raise e)
M finally N=in N;x
end
where x is not free in N.In the absence of special syntax,one has to program directly in terms of the translation,which involves the unpleasant duplication of N.This duplication may be minimised by abstracting(thunking)N,and by doing the same to M one can write a higher-order function finally of type(unit->’a)*(unit ->unit)->’a.One might(and the referees did)wonder whether our alternative syntax for exception handling allows the behaviour of finally to be obtained in a more convenient?rst-order way.Unfortunately,the answer is no.The translation of M finally N in our syntax is
Exceptional Syntax15 let val x=M
in N;x
unless e=>N;raise e
end
which,although it arguably makes the control?ow a little clearer,is not really any better than the translation in terms of handle–it still duplicates N.6
6Conclusions
Although the point is undeniably a small one,we hope we have convinced the reader that the try-in-unless syntax for exception handling really is more well-behaved than the traditional handle construct.It is also probably worth noting that if one translates a language with exceptions into one without them,by using sums to encode the exceptions monad(if the set of exceptions is in?nite then this requires either in?nite syntax or defaults in pattern matching),then the derived elimination construct for computations is essentially try-in-unless.(The di?erence is that all exceptions are always caught,though all but a?nite number are then rethrown.)
As far as we know,MIL is the?rst language to use try-in-unless,though we are not the only people to have spotted that it might be a useful programming construct–whilst we were writing this Judicael Courant suggested the essentially same thing on the CAML mailing list(1999).
From a methodological perspective,we feel that this is another small piece of evidence for the bene?ts of taking insights from proof-theory seriously when do-ing language design.Although the solution seems obvious in retrospect,and other people might have reached it by a di?erent route,we personally would not have recognised that there was an identi?able problem in the?rst place(as opposed to some ugly bits of code and slightly messy proofs)had we not been thinking in terms of proof-theoretic normal forms.
References
Abadi,M.(2000). -closed relations and admissibility.Mathematical Structures in Computer Science,10(3),313–320.
Benton,N.,&Kennedy,A.(1999).Monads,e?ects and transformations.Third Inter-national Workshop on Higher Order Operational Techniques in Semantics(HOOTS), Paris.Electronic Notes in Theoretical Computer Science,vol.26.Elsevier.
Benton,N.,Kennedy,A.,&Russell,G.1998a(September).Compiling Standard ML to Java bytecodes.3rd ACM SIGPLAN Conference on Functional Programming. Benton,P.N.,Bierman,G.M.,&de Paiva,V.C.V.(1998b).Computational types
6This duplication di?ers from those introduced by commuting conversions in that the continu-ations of the two copies of N are di?erent,so the sharing cannot be captured by MIL’s special ‘local block’abstractions.This problem with finally is the reason that the JVM includes a very restricted and ad hoc form of subroutine.
16Nick Benton and Andrew Kennedy
from a logical perspective.Journal of Functional Programming,8(2),177–193.Pre-liminary version appeared as Technical Report365,University of Cambridge Computer Laboratory,May1995.
Bierman,G.M.(1998).A computational interpretation of theλμ-calculus.Pages336–345of:Brim,L.,Gruska,J.,&Zlatu?s ka,J.(eds),Proceedings of the Symposium on Mathematical Foundations of Computer Science.Lecture Notes in Computer Science, vol.1450.
Courant,J.(1999).A common use of try...with.Message to the CAML mailing list,16 December.http://pauillac.inria.fr/caml/caml-list/2121.html.
Felleisen,M.,&Hieb,R.(1992).The revised report on the syntactic theories of sequential control and state.Theoretical Computer Science,103,235–271.
Flanagan,C.,Sabry,A.,Duba,B.F.,&Felleisen,M.(1993).The essence of compiling with continuations.Proceedings of the1993Conference on Programming Language Design and Implementation.ACM.
Girard,J.-Y.,Lafont,Y.,&Taylor,P.(1989).Proofs and Types.Cambridge Tracts in Theoretical Computer Science,no.7.Cambridge University Press.
Harper,R.,Duba,B.,&MacQueen,D.(1993).Typing?rst-class continuations in ML. Journal of Functional Programming,4(3),465–484.
Hatcli?,J.,&Danvy,O.(1994).A generic account of continuation-passing styles.Proceed-ings of the21st Annual Symposium on Principles of Programming Languages.ACM. Milner,R.,Tofte,M.,Harper,R.,&MacQueen,D.(1997).The De?nition of Standard ML(revised).The MIT Press.
Moggi,E.(1991).Notions of computation and https://www.doczj.com/doc/086274254.html,rmation and Computation, 93,55–92.
Paulson,L.C.(1991).ML for the Working Programmer.Cambridge University Press. Peyton Jones,S.,&Santos,A.(1998).A transformation-based optimiser for Haskell. Science of Computer Programming,32(1-3),3–47.
Peyton Jones,S.,Reid,A.,Hoare,T.,Marlow,S.,&Henderson,F.(1999).A semantics for imprecise exceptions.Proceedings of the1999Conference on Programming Language Design and Implementation.ACM.
Pitts,A.M.(1997).Operational Semantics for Program Equivalence.Invited talk at MFPS XIII,CMU,Pittsburgh.See https://www.doczj.com/doc/086274254.html,/users/amp12/talks/. Pitts,A.M.(2000).Parametric polymorphism and operational equivalence.Mathematical Structures in Computer Science,10,1–39.A preliminary version appeared in Proceed-ings,Second Workshop on Higher Order Operational Techniques in Semantics(HOOTS II),Stanford CA,December1997,Electronic Notes in Theoretical Computer Science10, 1998.
Pitts,A.M.,&Stark,I.D.B.(1998).Operational reasoning for functions with local state.Pages227–273of:Gordon,A.D.,&Pitts,A.M.(eds),Higher Order Operational Techniques in Semantics.Publications of the Newton Institute.Cambridge University Press.
Sabry,A.,&Felleisen,M.(1993).Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation,6(3/4),289–360.
Wright,A.K.,&Felleisen,M.(1994).A syntactic approach to type https://www.doczj.com/doc/086274254.html,rmation and Computation,115(1),38–94.
语法专练：方位介词 A、根据中文提示，用适当的方位介词填空： 1. There is a big pear tree __________ (在……的前面) my house. 2. Who was _________ (在……的后面) you when you were waiting in a line? 3. What’s _______(在……的下面)the desk? 4. The children are playing hide-and-seek. Maomao is hiding himself _______(在……里)the wardrobe. 5. The tallest boy in my class sits ________ (在……的隔壁) me. 6. They are standing _______ the door. (在……外面) B、用适当的介词填空： 1. You can’t see the ball. It’s ______ the door. 2. Shall we meet ________ the gate of the cinema? 3. Is he playing _______ the street or ______ the road? 4. Are they ________ a factory or _______ a farm? 5. I sit ________ the twins. The elder sister is _______ my left and the younger one is _______ my right. 6. The big tree ______ our classroom is nearly 100 years old. 7. The teacher is writing on the blackboard ______ the classroom. 8. ---- Where is the light? ---- It’s just _______ the table. 9. ---- Where are the lamps? ---- They are _____ the desks. 10. A plane is flying ________ the clouds.
方位介词与时间介词专项 一．选择填空。 ( )1．Mrs. Brown came to China ____ 1996. A．from B．of C．to D．in ( )2．The room was full ____ smoke after the big fire. A．of B．with C．in D．for ( )3. Here are some presents ____ you ____ our best wishes. A．to; with B. for; with C．of; about D．for; for ( )4. Both Mr Green and Mrs Green were born ____ June, 1956. A．in B．at C．on D．for ( )5．The little boy is always interested ____ science. A．with B．by C．in D．at ( )6．Li Lei often gets up ____ seven o'clock on Sundays. A．on B．in C．at D．for ( )7．They arrived early ____ a Tuesday morning. A．on B．at C．in D．of ( )8．--When were you born? --I was born ____ August 25, 1983. A．on B．in C．at D．to ( )9. The classroom is quite different_______that one. ( )10．Let me show you the place ____ the map. A．with B．on C．in ( )11．He got many gift________his birthday_______his friends. ( )12.The visitors ____ Japan arrived ____ Beijing Station last Tuesday morning. A．from; at B．of; to C．from; to D．of; on ( )13．It's cold outside. Please__________your warm clothes. A. put in B. take off C. put on D. put up ( )14. Look, you'll see a bridge__________the river. ( )15. –Your coat looks nice, Is It________cotton? -Yes. It's________Shanghai. A. made of, made by B. made of, made in C. made for, made in D. made from, made by 二、用适当的介词填空。 1．What's wrong ____ your watch? 2．One ____ the students is in the classroom. 3．I think the shop is closed ____ this time of day. 4．My father teaches English ____ a school. 5．We have lunch ____ the middle of the day. 6．You can buy some school things ____ your way home. 7．I was born ____ July 1, 1982. 8．Don't sleep ____ the open air. 9．I often help my mother _____ the housework. 10．It's time ____ school.
初中英语重难点之“方位”介词 介词的种类很多。在初中英语中，有许多表示事物存在的方向和位置的介词，我们称之为方位介词。如in（在……里），behind (在……后面)，down (向下)等等。其中有些方位介词的意义比较接近，在用法上很难区分，如on, over, above 都有“在……之上”的意思，但含义却不尽相同。我们可以用三个图示配以简短的文字叙述来说明这三个介词的不同用法。 on over above 通过这种方法，我们很容易掌握这三个介词的用法。现将初中英语教材中的部分方位介词用图示的方法归纳列举如下: (强调与物体的表面相接触)
几组方位介词的区别 方位介词in, on, to的区别： 1.in表示"在……范围内”，还表示“在…之中” Chongqing lies in the southwest of China. 2.on表示“与……毗邻，接壤” Canada lies on the north of America. 3.to表示方位，不接壤 Hunan lies to the east of Zhejiang. 表示地点位置的介词： 1.at, in, on, to at 用于小地方，at school, at home
In 用于大地方，in Beijing, in China On在……上面，on the map, on the table To到……To Chongqing 2.Above, over, on Above在……上方（高过另一个物体，不强调垂直） The airplane flies above that tall building.（不在正上方） over在……上方（垂直上方） The bridge spans over the river. On在……上面（物体表面有接触） There's some water on the floor, so you should be careful. 3.Below, under在……下面 Under在……下（正下方） The cat lies under the chair.（正下方） Below在……下（不一定是正下方） The cat lies under the chair.（不是正下方） 4.in front of, in the front of 在……的前面 in front of 在外部的前面，两个东西是独立的，相反的是behind The building is in front of the hospital. The building is behind the hospital.
时间介词与方位介词 一．时间介词(on, in, at): 1.in表示“在一段时间内或一天内的部分时间”,用于某年，季节，月份，一段时间或泛指的一天 中的上午，下午，晚上等前面。 (1)in 2014 (2)in spring/summer/autumn/winter (3)in January/February/March/April/May/June/July/August/September/October/November/December (4)in the morning/afternoon/evening on表示“某一天或某一天内的部分时间”，用于星期，节日，具体的某一天或具体日子的上午，下午，晚上等前面。 (1)on Monday/Tuesday/Wednesday/Thursday/Friday/Saturday/Sunday (2)on Children’s Day(儿童节)/Women’s Day(妇女节) (3)on December 27 (4)on Saturday morning at表示“某指定时间”，用于重点时间前，也可用于一天中的某段特定时间，如黎明(dawn),中午(noon),黄昏(dusk),午夜(midnight)。 (1)at 8:00 o’clock (2)at noon/dawn/dusk/midnight 二．方位介词： 1. 含义：用来表示人或物的________的词语。 2. 常见的方位介词：above, below, under, below, behind, in front of, beside, in, on等。 3. 用法： (1)in front of与in the front of: A. in front of:指在物体_______的前面。 There is a small river in front of the house. B. in the front of:指在物体_________的前面。 There is a blackboard in the front of the classroom. (2)above, over与on: A. above 意为“在......的上面，高于” The map is above the desk. B．over 意为“在......的正上方” There is thick cloud over Beijing. C. on 意为“在......上” The book is on the desk. (3)below与under: A. below 意为“在......的下方，低于” The river is below the mountain. B. under 意为“在......的正下方” The ball is under the chair. (4)behind 意为“在......的后面”
慕课、翻转课堂、微课的介绍和特点 所谓“慕课”(MOOC)，顾名思义，“M”代表Massive(大规模)，与传统课程只有几十个或几百个学生不同，一门MOOCs课程动辄上万人，最多达16万人；第二个字母“O”代表Open(开放)，以兴趣导向，凡是想学习的，都可以进来学，不分国籍，只需一个邮箱，就可注册参与；第三个字母“O”代表Online(在线)，学习在网上完成，无需旅行，不受时空限制；第四个字母“C”代表Course，就是课程的意思。[1] MOOC是新近涌现出来的一种在线课程开发模式，它发端于过去的那种发布资源、学习管理系统以及将学习管理系统与更多的开放网络资源综合起来的旧的课程开发模式。通俗地说，慕课是大规模的网络开放课程，它是为了增强知识传播而由具有分享和协作精神的个人组织发布的、散布于互联网上的开放课程。 这一大规模在线课程掀起的风暴始于2011年秋天，被誉为“印刷术发明以来教育最大的革新”，呈现“未来教育”的曙光。2012年，被《纽约时报》称为“慕课元年”。[2]多家专门提供慕课平台的供应商纷起竞争，Coursera、edX和Udacity是其中最有影响力的“三巨头”，前两个均进入中国。 主要特点: 1)、大规模的：不是个人发布的一两门课程：“大规模网络开放课程”(MOOC)是指那些由参与者发布的课程，只有这些课程是大型的或者叫大规模的，它才是典型的的MOOC。 2)、开放课程：尊崇创用共享（CC）协议；只有当课程是开放的，它才可以成之为MOOC。 3)、网络课程：不是面对面的课程；这些课程材料散布于互联网上。人们上课地点不受局限。无论你身在何处，都可以花最少的钱享受美国大学的一流课程，只需要一台电脑和网络联接即可。
时间介词与方位介词 一.时间介词(On, in, at): 1. in表示“在一段时间内或一天内的部分时间”，用于某年，季节，月份，一段时间或泛指的一天中的上午， 下午，晚上等前面。 (1) in 2014 (2) i n SPri ng/summer/autu mn/win ter (3) i n JanU ary/February/March/April/May/J Un e∕July∕AUgUSt/September/OCtober/November/DeCember (4) in the morning/afternoon/evening 2. on表示“某一天或某一天内的部分时间”，用于星期，节日具体的某一天或具体日子的上午，下午，晚上 等前面。 (1) On Mon day/Tuesday/Wed nesday/ThUrSday/Friday/SatUrday/S Un day (2) on ChiIdren ' S Day(儿童节)∕Women' S Day(妇女节) (3) o n DeCember 27 (4) on SatUrday morning 3. at表示“某指定时间”，用于重点时间前，也可用于一天中的某段特定时间，如黎明(dawn),中午(noon),黄 昏(dusk),午夜(midnight)。 (1) at 8:00 o ' clock (2) at noon /daw n/dusk/mid ni ght 4. 用法比较： 二.方位介词： 1. 含义：用来表示人或物的__________ 的词语。 2. 常见的方位介词：above, below, Under, below, behind, in front of, beside, in, on 等。 3. 用法： (1) in front of 与in the front of: A. in front of: 指在物体_________ 的前面。 There is a small river in front of the house. B. in the fro nt of: 指在物体__________ 的前面。 There is a blackboard in the front of the CIaSSroom. (2) above, over 与on: A. above 意为“在.... 的上面，高于” The map is above the desk. B. over ............. 意为“在的正上方” There is thick cloud over Beiji ng. C. on 意为“在...... 上” The book is On the desk. (3) below 与Under: A. below 意为“在...... 的下方，低于” The river is below the moun ta in. B. Under 意为“在.... 的正下方”
精品文档 时间介词与方位介词 一．时间介词(on, in, at): 1.in表示“在一段时间内或一天内的部分时间”,用于某年，季节，月份，一段时间或泛指的一天中的上午，下午，晚上等前面。 (1)in 2014 (2)in spring/summer/autumn/winter (3)in January/February/March/April/May/June/July/August/September/October/November/Decemb er (4)in the morning/afternoon/evening 2.on表示“某一天或某一天内的部分时间”，用于星期，节日，具体的某一天或具体日子的上午，下午，晚上等前面。 (1)on Monday/Tuesday/Wednesday/Thursday/Friday/Saturday/Sunday (2)on Children's Day(儿童节)/Women's Day(妇女节) (3)on December 27 (4)on Saturday morning 3.at表示“某指定时间”，用于重点时间前，也可用于一天中的某段特定时间，如黎明(dawn),中午(noon),黄昏(dusk),午夜(midnight)。 (1)at 8:00 o'clock (2)at noon/dawn/dusk/midnight 4.用法比较： 二．方位介词： 1. 含义：用来表示人或物的________的词语。 2. 常见的方位介词：above, below, under, below, behind, in front of, beside, in, on 等。 3. 用法： (1)in front of与in the front of: A. in front of:指在物体_______的前面。 There is a small river in front of the house. B. in the front of:指在物体_________的前面。 There is a blackboard in the front of the classroom. (2)above, over与on: A. above 意为“在......的上面，高于” The map is above the desk. B．over 意为“在......的正上方” There is thick cloud over Beijing.
初中英语《方位介词短语》练习题附答案及英语提分方法 Ⅰ. 把下列词组翻译成英语。 1. 在沙发上_____________ 2. 在桌子底下____________ 3.在你的背包里____________ 4. 在抽屉里___________ 5. 在教室（外部）前面__________ Ⅱ. 单项选则。 1. Your computer is ______ to the door. A. behind B. on C. in D. next 2 The map is ____ the wall ____ our classroom. A. on; on B. of; on C. on; at D. on; of 3 Look! The window is _____ the wall and the picture is _____ the wall. A. on; on B. in; in C. in; on D. on; in 4 －Where is my ball? I can’t see it. Look! It’s _____ the door. A. on B. in C. at D. behind 5. Sally is very happy. There is a big smile ______ her face. A. on B. to C. in D. at 6. My father is ill (生病), He is ______. A. in bed B. in the bed C. on bed D. on the bed 7. There is a map ofChina______ the wall in the classroom. A. in B. on C. under D. at
作品简介 本微课视频的教学内容为牛津小学英语5B Unit8 At the weekends (B)部分的单词教学。本部分的教学内容和教学重点是掌握6个昆虫类单词及insects的发音。教学目标是让学生通过微视频的学习，能够正确、流利地朗读6种昆虫类的单词以及单词insects，并能够熟练运用。教学难点是让学生读准单词发音，掌握发音规律，掌握以字母y结尾的可数名词变为复数时的变化规则。情感态度方面，需要学生具有通过微视频学习知识的兴趣，能够积极、主动的参与到教学活动中来，通过微视频学习的方式，掌握语言技能；能够根据自己对知识的掌握程度和实际需要借助视频学习的优势，反复观看，解决自己的难点问题，积极参与到视频教学中的操练项目，巩固和运用知识。 作品的创作说明： 教学设计 教学内容：牛津小学英语5B Unit8 At the weekends (B) 教学目标：让学生通过微视频学习，能够正确、流利地朗读6种昆虫类的单词以及单词insects，并能够熟练运用。 教学重点：熟练掌握6个昆虫类单词及insects的发音 教学难点：让学生读准6个昆虫类单词及insects的发音，掌握发音规律，知道以y结尾的可数名词变为复数时的变化规律。 教学过程：
Step 1借助情境图，激发兴趣，揭示课题 1.出示情境图，公园的一角 T: Here’s a picture. Is it nice? What can you see in the picture? T: Today, let’s learn some words about insects. 2.揭示课题，读2遍 Step2利用猜谜的游戏，呈现新单词，学习新单词 1.边听边猜，激发兴趣，学习新单词a grasshopper , a bee 教师讲两个昆虫的特点，让学生猜他们是什么？学生猜对后，教师呈现昆虫的图和单词，带领学生跟读，并指导单词grasshopper中a 和o的发音以及字母组合ee的发音。利用已知的单词学习新单词的发音。 2.自主阅读，猜一猜，他们是哪些昆虫 （1）学生自己读文本，猜文本中所指的是哪些昆虫。学生抓住昆虫的特点，思考。 （2）核对答案，并学习他们的发音，同时学习他们的复数形式及发音。 （3）引导学生观察发现，掌握以辅音字母+y 结尾的可数名词复数形式的变化规律。 3．整体呈现单词，齐读 整体呈现新单词，播放录音让学生整体跟读一遍，加以巩固。Step3 巩固操练 1.仔细阅读，根据歌谣内容，选择正确的图，填空。
小学英语方位介词练习题 一、用以下方位介词in, on, beside ,under，above，next to , in front of , behind , between，into填空 1.Beijing is______the north of China . 2.The twins usually stand ____their parents ,and their parents are in the middle . 3.There is a map of China __________ the wall of our classroom. 4.Before000,there was no airline _________the two cities. 5.The boy sitting __________Tina, so she couldn’t see the film clearly. 6.She will leave her homework __________ the teacher ‘s desk after school today. 7.You must ride your bike ___________ the right side of the road. 8.Mr Smith lives __________ that building. His house is ___________ the fifth floor. 9.There was an exciting moment in our class when a large bird flew _____ the room. 10.The boy is taller than his friend, so he sits ___________ him in the classroom. 二、选择
英语中方位介词用法 介词是一种用来表示词与词, 词与句之间的关系的词。在句中不能单独作句字成分。介词后面一般有名词代词或相当于名词的其他词类，短语或从句作它的宾语。介词和它的宾语构成介词词组，在句中作状语，表语，补语，定语或介词宾语。 at ,in, on, to at (1)表示在小地方; (2)表示“在……附近，旁边” in (1)表示在大地方; (2)表示“在…范围之内”。 on 表示毗邻，接壤 to 表示在……范围外，不强调是否接壤 及时练 1.He arrived _____ the station at ten. 2.He is sitting ______ the desk. 3.He arrived _____ Shanghai yesterday. 4.Jiangsu lies ________ the east of China. 5.Russia live ______ the north of China. 6.Fujian is ________ the south of Jiangsu Province. 2)above, over, on 在……上 above 指在……上方,不强调是否垂直，与below相对; over指垂直的上方,与under相对,但over与物体有一定的空间，不直接接触。 on表示某物体上面并与之接触。 1.The bird is flying above my head. 2.There is a bridge over the river. 3.He put his watch on the desk.
3)below, under 在……下面 under表示在…正下方 below表示在……下，不一定在正下方 There is a cat under the table. Please write your name below the line. 方位介词 1. at表示"在......处"，一般指较小的比较具体的地点。 如： He isn't at school. He is at home. 他不在学校，他在家。 2. in表示"在......内部;在......里面"的意思。如： What is in the box? 盒子里有什么? 3. on表示"在某物的上面"，但两者互相接触。 如：My books are on that table. 我的书在那张桌子上。 on the wall 在墙上 4. under表示"在某物垂直的正下方"，两者之间不接触。 如：My cat is under my chair. 我的猫在我的椅子下。 5. behind表示"在某物体的后面"。如：The broom is behind the door. 笤帚在门后。 6. in front of表示"在......的前面"，正好与behind相反。 如： There are some big trees in front of our classroom. 我们教室前面有几棵大树。 7. near表示"在某物体的附近"，意为"接近、靠近"。 如： The ball is near the door. 球在门旁边。
第04 讲_时间和方位介词 时间介词 知识精讲 介词是一种“媒介”词，是用来表示句子中某一个词或短语与另外一个词或短语之间的关系的词。 、表“在??时”的时间介词 、常见时间介词辨析 1. in 和after
after+将来时间点” 表示将来的某一after 时刻以后, 用于将来时。 She will appear after five o' clock this afternoon. 2. since 和for 3. by 和till/ until 三点剖析 一、考点：时间in/ on/ at 介词的用法 、重难点：时间介词的辨析及用法
时间介词是中考的考查重点。时间介词的中考题主要以单项选择以及完形填空等题型来考查。 注意：during 表示事件发生在何时（when ），意为“在??期间内”的行为或状态。in 表示时间段，相当于during ，但是注意在选择的时候一定要优先选择during 。 例：They visited many cities during their stay in China. 他们在中国期间，游览了许多城市。 题模精讲 题模一表“在?时”的时间介词 例 1.1 、 He often goes to school by bike ________ the morning. A、at B、in C、on D、for 例 1.2 、 They started off ________ an autumn afternoon. A、at B、in C、on D、during 例 1.3 、 用适当的时间介词填空。 I often got up ________ 6 o ' clock when I worked in the company ________ 2008. 题模二常见时间介词辨析 例 2.1 、
创作编号：BG7531400019813488897SX 创作者：别如克* 微课的类型介绍 按照不同的划分方法，微课可以被分为许多种类型，其中按照教学方法来分类，微课大致可以划分为分别为五类，分别为：讲授类、讨论类、启发类、演示类、练习类等。那么今天我们就为大家介绍几种常见的微课类型，以便于大家在今后的微课制作中有更好设计思路和创意。 一、讲授类 讲授类微课适用于教师运用口头语言向学生传授知识,如描绘情境、叙述事实、解释概念、论证原理和阐明规律。这是中小学最常见、最主要的一种微课类型。 1.课堂实录微缩版 这种类型的微课中有教师、有学生、有活动、有交互……然而学生不是教研员，也不是评课专家。他不需要观看师生活动过程，学生需要的仅仅是学习内容本身。 2.画中画版 这种方式的优点在于，老师的头像出现在视频局部，仿佛老师就在自己身边一对一讲解，亲切而自然，更易于被学生接受从而愿意去学习。 二、讨论类 讨论类微课适用于在教师指导下，由全班或小组围绕某一种中心问题通过发表各自意见和看法，共同研讨，相互启发，集思广益地进行学习。 三、演示类 1.幻灯片动画式 演示类微课适用于教师在课堂教学时，把实物或直观教具展示给学生看，或者作示范性的实验，或通过现代教学手段，通过实际观察获得感性知识以说明和印证所传授知识。 PPT类微课是指教师借助PPT的视频录制功能将嵌入有课程讲解配音的PPT直接录制成流媒体视频。这类微课视频的制作门槛低，要求老师必须具备一定的动画设计制作能力。 2.手机+白纸 工具随手可得，技术难度低，操作快捷方便，画面真实亲切，并且易于分享
结语： 但在实际微课的设计与拍摄时，老师还得根据课程的性质、教学的要求、学校的实际硬件条件及自身的技术能力来选择微课的类型，只有这样，微课才能真正与课堂教学相结合，并能通过翻转课堂教学来提升课程教学的质量。 创作编号：BG7531400019813488897SX 创作者：别如克*
语法讲解：方位介词 一、方位介词 1. at表示“在……处”，一般指较小的比较具体的地点。He isn’t at school. He is at home. 2. in表示“在……内部；在……里面”的意思。What is in the box? 盒子里有什么？ 3. on表示“在某物的上面”，但两者互相接触。My books are on that table. 我的书在那张桌子上。 4.above在……上方。指两者既不垂直也不接触（反义词below)。 Many birds are flying above the woods.许多鸟在树林上飞。 5. under表示“在某物垂直的正下方”，两者之间不接触。My cat is under my chair. 我的猫在我的椅子下。 6. behind表示“在某物体的后面”。The boy is behind the door. 男孩在门后。 7 in front of表示“在……的前面”，正好与behind相反。如： There are some big trees in front of our classroom. 我们教室前面有几棵大树。 8. near表示“在某物体的附近”，意为“接近、靠近”。The ball is near the door. 球在门旁边。 介词in, on, under, behind是表示静态位置的介词。 二、常见方位介词短语 (一)、由介词in构成的方位介词短语 1、in the front 在前面 2、in the front row 在前排 3、in the back row 在后排 4、in the third row 在第三排 5、in front of... 在……前面（范围之外） 6、in the front of... 在……前部（范围之内） 7、in the middle在中间 8、in the street在街上 9、in the middle of...在……中间
常用方位介词和短语 【概念引入】 介词后面可以跟名词和代词做宾语，构成介词短语。今天我们主要学习一下用来表示方位的介词和介词短语。 【用法讲解】 1. on 介词on表示“在某物之上”的意思，它通常表示一个物体在另一个物体之表面上面。两者之间有接触。 例如：Your book is on the desk. 你的书在课桌上面。 There is a ball on the floor. 地板上有个球。 拓展：above 和over的区别 on指的有接触面的上面，但是over和above都是没有接触面的上面。 over“在……正上方”，与under相对。 例如：There is a bridge over the river. 河上有一座桥。 The picture is hanging over the blackboard. 那张图挂在黑板的正上方。 above只表示“在……上方或位置高出……”，不一定是正上方，与below相对。 例如：A plane flew above our heads. 一架飞机从我们头上飞过。 The Turners live above us. 特纳一家人住在我们的上面。 2. in 介词in表示“在某物的里面”，它通常表示一个物体在另外一个物体的内部、中间或者在某个范围之内。 例如：Your pen is in the pencil case. 你的钢笔在铅笔盒里面。 She is the tallest in her class. 她是她们班最高的。 3. under 介词under表示“在某物的下面”，它通常表示一个物体在另外一个物体的垂直正下面，两者之间没有接触。 例如：My bike is under the tree. 我的自行车在树的下面。 The shoes are under the chair. 鞋在椅子的下面。 拓展：under和below 的区别 under表示“在……之下”，通常表示位置处于正下方，与介词over“在……上方”相对应。 例如： T here is a book under the table. 桌子下面有一本书。 A cat is sitting under the table.一只猫在桌子下面。 below表示“在……之下”，“在……的下游”，与介词above相对应，常指在某物体之下，但不一定在该物的正下方。 例如：He is below the average at school.他的学习成绩在水准以下。 I looked down at the hall below. 我瞧了瞧下面的大厅。 4. behind 介词behind表示“在某物的后面”，它通常表示一个物体在另外一个物体的后面。 例如：Your brother is behind the tree. 你的弟弟在树的后面。 She is standing behind her mother. 她站在她妈妈的后面。
本微课视频有以下几个优点： 1、通过本节课的教学，让学生进一步体会，数学来源于生活，又用于生活，提供学生生活中熟悉的材料作背景，学生学习兴趣很高。 2、教学设施中，我非常重视开头的引入教学，激发学生学习的兴趣。注意鼓励学生大胆发言，注意从生活中的两幅图片出发，展现知识的形成过程，使学生能够利用已有的生活知识和数学知识，通过知识迁移、类比的方法归纳得出同类项的概念以及合并同类项的法则。使他们不会觉得数学概念学习的单调乏味，逐步提高学生抽象概括的能力。 3、教学的设计主要是体现以“学生为主体，教师为主导”的教学理念。整个教学过程都是学生在思考、交流，相互比赛，并解决问题，老师只是进行适当的点拨，从而真正体现了以学生为主体，教师为主导的教学理念。学生通过自学，再小组讨论，把不懂的问题都在组内消化完成。全班交流展示时，所举同类项的例子，能检验该学生是否真正掌握了同类项的概念，突出了合作交流的重要性。 4、通过议一议，汇报学习成果，培养了学生的数学语言表达能力，促使学生对合并同类项的法则理解记忆。通过比一比，看谁反应快；填一填，看谁写得最快；全班分为两组进行比赛能检验学生对同类项的概念及合并同类项的法则是否掌握，学生通过两组比赛活动，也能发扬学生合作学习的精神，进一步培养学生团结协助、严谨求实的学习精神。从而激发了学生探究数学的兴趣，更能发挥学生解决问题的主动性，使每个学生在比赛活动中都有收获。 5、通过学生谈收获，教师做补充，培养学生的数学语言表达能力和自我整理的学习习惯。因此整堂课主要突出了以下三个方面：贯穿了一个原则——以学生为主体的原则；培养了一种意识——合作交流的意识；锻炼了一种能力——数学语言表达能力。
初中英语语法总结：方位介词 表示地点的介词in、on、behind、next to、near、over、under (1). in在……里面：The pencil is in the desk. 铅笔在课桌里。 (2). on在……上面：There are some apple on the tree. 树上有些苹果。 (3). under在……下面/正下方：What's under your desk? 你书桌底下是什么？ (4). over在……正上方：There is a shelf over the table. 桌子上方有一个书架。 (5). above 在……斜上方：Raise your arms above your head. (6). below 在……斜下方：Her skirt came below her knees. (7).behind在……之后：There is a bike behind the tree. 树后有一辆自行车。 (8).next to在……旁边：There is a café next to the barber's. 理发店隔壁是一家咖啡馆。 (9).near在……附近：My bed is near the window. 我的床在窗户旁。 (10).by 在……旁：He was sitting by the window. 第一组：over, above和on的用法 1）over指在…的正上方，表示垂直在上。如: There is a lamp over the desk. 2)above指在上方，属于斜上方。如： Raise your arms above your head. 3)on指在上面，表示两物体接触。如： There is a cup on the table. 第二组：under / below的用法： 1) under在……下面/正下方：What's under your desk? 2) below 在……斜下方：Her skirt came below her knees. 练习： ( ) 1 The boat is passing___ the bridge. A. through B. below C. under D. across ( ) 2 Two planes are flying___ the city. A. through B. over C. on D, below
词法大全（三）-介词 Contents 三大时间介词 三大方位介词 三大交通方式介词 几大易混介词 几个小点 大显身手
介词 介词是一种用来表示词与词, 词与句之间的关系的虚词。 常见介词 at before after in on by to near next to with for under in front of behind from since about 三大时间介词 at on in ↑↑↑ 点日剩下 常见的固定搭配： in the morning/afternoon/evening at noon/night/midday/midnight 如morning 等有任何词修饰，则用on，如on a cold morning 三大方位介词 in Guangzhou is in the south of Guangdong. on Sichuan is on the east of Tibet. to Japan is to the east of China. 三大交通方式介词 by car by plane by train by ship by bike in my father’s car in a car on a bike on his bike 几大易混介词 in front of He is sitting in front of me. in the front of The boy sat in the front of the car. The boy sat in front of the car. (此句子较离奇) across 横过She swam across the river. through 穿过He went through the door. There are many apples on the tree. There is a boy in the tree. 树上长的用on，否则用in 几个小点 We arrived in Tokyo at nine. We arrived at the cinema at nine. arrive at 用于小地点arrive in 用于大地点