Permalink
Find file
Fetching contributors…
Cannot retrieve contributors at this time
1412 lines (1087 sloc) 44.6 KB
grammar
embed
{{ tex
\section{Type system}
\label{sec.typing}
TODO
}}
defns
JdomEB :: J ::=
defn
dom ( EB ) gives name :: :: domEB :: domEB_ {{ com Environment binding domain }} by
{{ com
Gets the name of an environment entry.
}}
------------------------------------------------------- :: type_param
dom(TV) gives TV
------------------------------------------------------- :: value_name
dom(value_name:typescheme) gives value_name
----------------------------------------------------- :: const_constr_name
dom(constr_name of typeconstr) gives constr_name
----------------------------------------------------- :: constr_name
dom(constr_name of forall type_params_opt, (t1, ..., tn) : typeconstr) gives constr_name
----------------------------------------------------- :: opaque_typeconstr_name
dom(typeconstr_name:kind) gives typeconstr_name
----------------------------------------------------- :: trans_typeconstr_name
dom(type_params_opt typeconstr_name = t) gives typeconstr_name
----------------------------------------------------- :: record_typeconstr_name
dom(typeconstr_name : kind {field_name1; ...; field_namen}) gives typeconstr_name
----------------------------------------------------- :: record_field_name
dom(field_name:forall type_params_opt, typeconstr_name -> typexpr) gives field_name
------------------------------------------------------- :: location
dom(location:t) gives location
defns
JdomE :: J ::=
defn
dom ( E ) gives names :: :: domE :: domE_ {{ com Environment domain }} by
{{ com
Gets all of the names in an environment.
}}
------------------------------------------------------- :: empty
dom(empty) gives
dom(E) gives name1..namen
:JdomEB:dom(EB) gives name
------------------------------------------------------- :: cons
dom(E,EB) gives name name1..namen
defns
Jlookup :: Jlookup_ ::=
defn
E |- name gives EB :: :: EB :: EB_ {{ com Environment lookup }} by
{{ com
Returns the rightmost binding that matches the given name.
}}
:JdomEB:dom(EB) gives name'
name noteq name'
name' noteq TV
E |- name gives EB'
------------------------------------------------------- :: rec1
E,EB |- name gives EB'
name noteq TV
E |- name gives EB'
------------------------------------------------------- :: rec2
( E,TV ) |- name gives ( shift 0 1 EB' )
:JdomEB:dom(EB) gives name
------------------------------------------------------- :: head
E,EB |- name gives EB
defns
Jidx :: Jidx_ ::=
defn
E |- idx bound :: :: bound :: bound_ {{ com Well-formed index }} by
{{ com
Determines whether an index is bound by an environment.
}}
E |- idx bound
:JdomEB:dom(EB) gives name
name noteq TV
------------------------------------------------------- :: skip1
E, EB |- idx bound
E |- idx bound
------------------------------------------------------- :: skip2
E, TV |- (idx + 1) bound
------------------------------------------------------- :: found
E, TV |- 0 bound
defns
JTtps_kind :: JT ::=
defn
|- type_params_opt : kind :: :: tps_kind :: tps_kind_ {{ com Type parameter kinding }} by
{{ com
Counts the number of parameters and ensures that none is repeated.
}}
tp1 ... tpn distinct
length (tp1)...(tpn) = n
------------------------------------------------------- :: kind
|- (tp1, ..., tpn) : n -> Type
defns
JTEok :: JT ::=
defn
E |- ok :: :: Eok :: Eok_ {{ com Environment validity }} by
{{ com
Asserts that the various components of the environment are well-formed
(including that there are no free type references), and regulates name
shadowing. Environments contain identifiers related to type definitions and
type variables as well as expression-level variables (i.e., value names), so
they are dependent from left to right. Shadowing of type, constructor, field
and label names is forbidden, but shadowing of value names is allowed.
}}
------------------------------------------------------- :: empty
empty |- ok
E |- ok
------------------------------------------------------- :: typevar
E , TV |- ok
E |- forall t : Type
------------------------------------------------------- :: value_name
E, (value_name : forall t) |- ok
E |- ok
E |- typeconstr_name gives typeconstr_name : kind
dom(E) gives names
constr_name notin names
----------------------------------------------------- :: constr_name_c
E,(constr_name of typeconstr_name) |- ok
type_params_opt = (tv1, ..., tvm)
E |- forall type_params_opt, t1 : Type ... E |- forall type_params_opt, tn : Type
E |- typeconstr_name gives typeconstr_name : m -> Type
dom(E) gives names
constr_name notin names
:formula_length_list_typexpr_ge:length ( t1 ) ... ( tn ) >= 1
:formula_length_list_type_param_eq:length (tv1) ... (tvm) = m
----------------------------------------------------- :: constr_name_p
E,(constr_name of forall (tv1, ..., tvm), (t1, ..., tn) : typeconstr_name) |- ok
E |- forall (tv1, ..., tvm), t : Type
dom(E) gives names
field_name notin names
E |- typeconstr_name gives typeconstr_name:m->Type {field_name1; ...; field_namen}
:formula_length_list_type_param_eq:length (tv1) ... (tvm) = m
field_name in field_name1...field_namen
---------------------------------------------------- :: record_destr
E, (field_name:forall (tv1, ..., tvm), typeconstr_name -> t) |- ok
E |- ok
dom(E) gives names
typeconstr_name notin names
----------------------------------------------------- :: typeconstr_name
E,(typeconstr_name : kind) |- ok
dom(E) gives names
typeconstr_name notin names
E |- forall (tv1, ..., tvm), t : Type
----------------------------------------------------- :: typeconstr_eqn
E, ((tv1, ..., tvm) typeconstr_name = t) |- ok
E |- ok
dom(E) gives names
typeconstr_name notin names
field_name1...field_namen distinct
---------------------------------------------------- :: typeconstr_record
E, (typeconstr_name:kind {field_name1; ...; field_namen}) |- ok
E |- t : Type
dom(E) gives names
location notin names
------------------------------------------------------- :: location
E,(location : t) |- ok
defn
E |- typeconstr : kind :: :: typeconstr :: typeconstr_ {{ com Type constructor kinding }} by
{{ com
Ensures that the type constructor is either defined in the environment or
built-in. The result kind indicates how many parameters the type constructor
expects.
}}
E |- ok
E |- typeconstr_name gives typeconstr_name:kind
----------------------------------------------------- :: abstract
E |- typeconstr_name:kind
E |- ok
E |- typeconstr_name gives type_params_opt typeconstr_name=t
|- type_params_opt : kind
----------------------------------------------------- :: concrete
E |- typeconstr_name:kind
E|- ok
E |- typeconstr_name gives typeconstr_name:kind{field_name1; ...; field_namen}
----------------------------------------------------- :: record
E |- typeconstr_name:kind
E |- ok
------------------------------------------------------- :: int
E |- int : Type
E |- ok
------------------------------------------------------- :: char
E |- char : Type
E |- ok
------------------------------------------------------- :: string
E |- string : Type
E |- ok
------------------------------------------------------- :: float
E |- float : Type
E |- ok
------------------------------------------------------- :: bool
E |- bool : Type
E |- ok
------------------------------------------------------- :: unit
E |- unit : Type
E |- ok
------------------------------------------------------- :: list
E |- list : 1 -> Type
E |- ok
------------------------------------------------------- :: option
E |- option : 1 -> Type
E |- ok
------------------------------------------------------- :: ref
E |- ref : 1 -> Type
defn
E |- typescheme : kind :: :: ts :: ts_ {{ com de Bruijn type scheme well-formedness }} by
{{ com
Ensures that the type is well-formed in an extended environment.
}}
E,TV |- t : Type
------------------------------------------------------- :: forall
E |- forall t : Type
defn
E |- forall type_params_opt , t : kind :: :: tsnamed :: tsnamed_ {{ com Named type scheme well-formedness }} by
{{ com
Ensures that the named type paramaters are distinct, and that the type is
well-formed. Instead of extending the environment, this simply substitutes a
collection of well-formed types, here $\ottkw{unit}$. This works because the
type well-formedness judgment below only depends on well-formedness of
sub-expressions, and not on the exact form of sub-expressions.
}}
E |- << ( tv1 <- unit ), ..., ( tvn <- unit ) >> t : Type
tv1...tvn distinct
------------------------------------------------------- :: forall
E |- forall (tv1, ..., tvn), t : Type
defn
E |- typexpr : kind :: :: t :: t_ {{ com Type expression well-formedness }} by
{{ com
Ensures that all of the indices and constructors that appear in a type are
bound in the environment.
}}
E |- ok
E |- idx bound
------------------------------------------------------- :: var
E |- <idx, num> : Type
%TODO: constraints for linearity
E |- t : Type
E |- t' : Type
------------------------------------------------------- :: arrow
E |- t -> '[^' qlt '^]' t' : Type
%TODO: constraints for linearity
E |- t1 : Type .... E |- tn : Type
:formula_length_list_expr_ge: length (t1) ... (tn) >= 2
------------------------------------------------------- :: tuple
E |- ( t1*....*tn ) '[^' qlt '^]' : Type
%TODO: constraints for linearity
:JTtypeconstr: E |- typeconstr : n -> Type
E |- t1 : Type ... E |- tn : Type
length (t1)...(tn) = n
------------------------------------------------------- :: constr
E |- (t1,...,tn) typeconstr '[^' qlt '^]' : Type
defns
JTeq :: JT ::=
defn
E |- typexpr == typexpr' :: :: eq :: eq_ {{ com Type equivalence }} by
{{ com
Checks whether two types are related (potentially indirectly) by the type
abbreviations in the environment. The system does not allow recursive types
that do not pass through an opaque (generative) type constructor, i.e., a
variant or record. Therefore all type expressions have a canonical form
obtained by expanding all type abbreviations.
}}
E |- t : Type
----------------------------------------------------- :: refl
E |- t == t
E |- t' == t
----------------------------------------------------- :: sym
E |- t == t'
E |- t == t'
E |- t' == t''
----------------------------------------------------- :: trans
E |- t == t''
%TODO: constraints for linearity
E |- ok
E |- typeconstr_name gives (typevar1, ..., typevarn) typeconstr_name=t
E |- t1 : Type ... E |- tn : Type
----------------------------------------------------- :: expand
E |- (t1, ..., tn) typeconstr_name == << ( typevar1<-t1 ), ..., ( typevarn<-tn) >>t
%TODO: constraints for linearity
E |- t1 == t1'
E |- t2 == t2'
----------------------------------------------------- :: arrow
E |- t1 -> '[^' qlt1 '^]' t2 == t1' -> '[^' qlt2 '^]' t2'
%TODO: constraints for linearity
E |- t1 == t1' .... E |- tn == tn'
length (t1)....(tn) >= 2
----------------------------------------------------- :: tuple
E |- ( t1 * .... * tn ) '[^' qlt1 '^]' == ( t1' * .... * tn' ) '[^' qlt2 '^]'
%TODO: constraints for linearity
:JTtypeconstr: E |- typeconstr : n -> Type
E |- t1 == t1' ... E |- tn == tn'
length (t1)...(tn) = n
----------------------------------------------------- :: constr
E |- (t1, ..., tn) typeconstr '[^' qlt1 '^]' == (t1', ..., tn') typeconstr '[^' qlt2 '^]'
defns
JTidxsub :: JT ::=
defn
'<<' typexpr1 , .. , typexprn '>>' typexpr' gives typexpr'' :: :: idxsub :: inxsub_ {{ com de Bruin type substitution }} by
{{ com
Replaces index 0 position $n$ with the $n$th type in the list, and reduces all
other indices by 1.
}}
------------------------------------------------------- :: alpha
<< t1, .., tn >> typevar gives typevar
length (t1)..(tm) = num
------------------------------------------------------- :: idx0
<<t1, .., tm, t', t1'', .., tn''>> <0, num> gives t'
length (t1)..(tn) <= num
------------------------------------------------------- :: idx1
<< t1, .., tn >> <0, num> gives unit
------------------------------------------------------- :: idx2
<< t1, .., tn >> <idx + 1, num> gives <idx, num>
------------------------------------------------------- :: any
<< t1, .., tn >> _ gives _
%TODO: constraints for linearity
<<t1, .., tn>> t1' gives t1''
<<t1, .., tn>> t2' gives t2''
------------------------------------------------------- :: arrow
<<t1, .., tn>> (t1' -> '[^' qlt1 '^]' t2') gives t1'' -> '[^' qlt1 '^]' t2''
%TODO: constraints for linearity
<<t1, .., tn>> t1' gives t1'' .... <<t1, .., tn>> tm' gives tm''
------------------------------------------------------- :: tuple
<<t1, .., tn>> (t1' * .... * tm') '[^' qlt1 '^]' gives (t1'' * .... * tm'') '[^' qlt2 '^]'
%TODO: constraints for linearity
<<t1, .., tn>> t1' gives t1'' ... <<t1, .., tn>> tm' gives tm''
------------------------------------------------------- :: tc
<<t1, .., tn>> (t1', ..., tm') typeconstr '[^' qlt1 '^]' gives (t1'', ..., tm'') typeconstr '[^' qlt2 '^]'
defns
JTinst :: JT ::=
defn
E |- typexpr <= typescheme :: :: inst :: inst_ {{ com de Bruijn type scheme instantiation }} by
{{ com
Replaces all of the bound variables of a type scheme.
}}
E |- forall t' : Type
E |- t1 : Type .. E |- tn : Type
<<t1, .., tn>>t' gives t''
------------------------------------------------------- :: idx
E |- t'' <= forall t'
defns
JTinst_named :: JT ::=
defn
E |- typexpr <= forall type_params_opt , typexpr' :: :: inst_named :: inst_named_ {{ com Named type scheme instantiation }} by
{{ com
Replaces all of the bound variables of a named type scheme.
}}
E |- forall (typevar1, ..., typevarn), t : Type
E |- t1 : Type ... E |- tn : Type
------------------------------------------------------- :: named
E |- <<typevar1<-t1, ..., typevarn<-tn>>t <= forall (typevar1, ..., typevarn), t
defns
JTinst_any :: JT ::=
defn
E |- typexpr <= typexpr' :: :: inst_any :: inst_any_ {{ com Wildcard type instantiation }} by
{{ com
Replaces $\ottkw{\_}$ type variables with arbitrary types.
}}
E |- <idx, num> : Type
------------------------------------------------------- :: tyvar
E |- <idx, num> <= <idx, num>
E |- t : Type
------------------------------------------------------- :: any
E |- t <= _
%TODO: constraints for linearity
E |- t1 <= t1'
E |- t2 <= t2'
------------------------------------------------------- :: arrow
E |- t1 -> '[^' qlt1 '^]' t2 <= t1' -> '[^' qlt2 '^]' t2'
%TODO: constraints for linearity
E |- t1 <= t1' .... E |- tn <= tn'
length (t1)....(tn) >= 2
------------------------------------------------------- :: tuple
E |- (t1 * .... * tn) '[^' qlt1 '^]' <= (t1' * .... * tn') '[^' qlt2 '^]'
%TODO: constraints for linearity
E |- t1 <= t1' ... E |- tn <= tn'
:JTtypeconstr: E |- typeconstr : n -> Type
length (t1)...(tn) = n
------------------------------------------------------- :: ctor
E |- (t1, ..., tn) typeconstr '[^' qlt1 '^]' <= (t1', ..., tn') typeconstr '[^' qlt1 '^]'
defns
JTval :: JT ::=
defn
E |- value_name : typexpr :: :: value_name :: value_name_ {{ com Variable typing }} by
{{ com
Determines if a variable can have a specified type.
}}
E |- value_name gives value_name:ts
E |- t <= ts
------------------------------------------------------- :: value_name
E |- value_name:t
>>
<<
defns
JTfield :: JT ::=
defn
E |- field_name : typexpr -> typexpr' :: :: field :: field_ {{ com Field name typing }} by
{{ com
Determines the type constructor associated with a given field name. Since
field names are used to destructure record data, the type is a function type
from a record to the type of the corresponding position.
}}
E |- field_name gives field_name:forall ( tv1, ..., tvm ), typeconstr_name -> t
E |- ( t1', ..., tm' ) typeconstr_name -> t'' <= forall ( tv1, ..., tvm ), ( tv1, ..., tvm ) typeconstr_name -> t
------------------------------------------------------- :: name
E |- field_name : ( t1', ..., tm' ) typeconstr_name -> t''
>>
<<
defns
JTconstr_p :: JT ::=
defn
E |- constr : typexpr1 ... typexprn -> typexpr' :: :: constr_p :: constr_p_ {{ com Non-constant constructor typing }} by
{{ com
Determines the type constructor associated with a given value constructor.
Non-constant constructors are attributed types for each argument as
well as a return type.
}}
%TODO: constraints for linearity
E |- constr_name gives constr_name of forall (tv1, ..., tvm), (t1,....,tn):typeconstr
E |- ( t1' * .... * tn' ) -> ( t1'', ..., tm'' ) typeconstr '[^' qlt1 '^]' <= forall ( tv1, ..., tvm ), ( t1 * .... * tn ) -> ( tv1, ..., tvm ) typeconstr '[^' qlt2 '^]'
----------------------------------------------------- :: name
E |- constr_name : t1' .... tn' -> (t1'', ..., tm'') typeconstr '[^' qlt '^]'
%TODO: constraints for linearity
E |- t : Type
------------------------------------------------------- :: some
E |- Some : t -> (t option '[^' qlt '^]')
defns
JTconstr_c :: JT ::=
defn
E |- constr : typexpr :: :: constr_c :: constr_c_ {{ com Constant constructor typing }} by
{{ com
Constant constructors are typed like non-constant constructors without
arguments.
}}
%TODO: constraints for linearity
E |- ok
E |- constr_name gives constr_name of typeconstr_name
E |- typeconstr_name gives typeconstr_name : n -> Type
E |- t1 : Type ... E |- tn : Type
length (t1) ... (tn) = n
----------------------------------------------------- :: constr
E |- constr_name : (t1, ..., tn) typeconstr_name '[^' qlt '^]'
%TODO: constraints for linearity
E |- t : Type
------------------------------------------------------- :: none
E |- None : t option '[^' qlt '^]'
defns
JTconst :: JT ::=
defn
E |- constant : typexpr :: :: const :: const_ {{ com Constant typing }} by
{{ com
Determines the type of a constant.
}}
E |- ok
------------------------------------------------------- :: int
E |- integer_literal : ( int '[^' nonlinear '^]' )
E |- ok
------------------------------------------------------- :: float
E |- float_literal : ( float '[^' linear '^]' )
E |- ok
------------------------------------------------------- :: char
E |- char_literal : ( char '[^' nonlinear '^]' )
E |- ok
------------------------------------------------------- :: string
E |- string_literal : ( string '[^' nonlinear '^]' )
:JTconstr_c: E |- constr : t
------------------------------------------------------- :: constr
E |- constr : t
E |- ok
------------------------------------------------------- :: false
E |- false : ( bool '[^' nonlinear '^]' )
E |- ok
------------------------------------------------------- :: true
E |- true : ( bool '[^' nonlinear '^]' )
E |- ok
------------------------------------------------------- :: unit
E |- () : ( unit '[^' nonlinear '^]' )
%TODO: constraints for linearity
E |- t : Type
------------------------------------------------------- :: nil
E |- [] : ( t list '[^' qlt '^]' )
defns
JTpat :: JT ::=
defn
Tsigma & E |- pattern : typexpr gives E' :: :: pat :: pat_ {{ com Pattern typing and binding collection }} by
{{ com
Determines if a pattern matches a value of a certain type, and calculates the
types of the variables it binds. A pattern must bind any given variable at
most once, except that the two alternatives of an or-pattern must bind the same
set of variables. $[[Tsigma]]$ gives the types that should replace type
variables in explicitly type-annotated patterns.
}}
E |- t : Type
------------------------------------------------------- :: var
Tsigma & E |- x : t gives empty,x:t
E |- t : Type
------------------------------------------------------- :: any
Tsigma & E |- _ : t gives empty
:JTconst: E |- constant : t
------------------------------------------------------- :: constant
Tsigma & E |- constant : t gives empty
Tsigma & E |- pattern : t gives E'
E |- t' <= Tsigma src_t
E |- t == t'
------------------------------------------------------- :: typed
Tsigma & E |- ( pattern : src_t ) : t gives E'
Tsigma & E |- pattern : t gives E'
Tsigma & E |- pattern' : t gives E''
E' PERMUTES E''
------------------------------------------------------- :: or
Tsigma & E |- pattern | pattern' : t gives E'
:JTconstr_p:E |- constr : t1 ... tn -> t
Tsigma & E |- pattern1 : t1 gives E1 ... Tsigma & E |- patternn : tn gives En
dom(E1@...@En) gives name1..namem
name1..namem distinct
------------------------------------------------------- :: construct
Tsigma & E |- constr (pattern1,...,patternn) : t gives E1@...@En
:JTconstr_p:E |- constr : t1...tn->t
------------------------------------------------------- :: construct_any
Tsigma & E |- constr _ : t gives empty
Tsigma & E |- pattern1:t1 gives E1 .... Tsigma & E |- patternn:tn gives En
length (pattern1)....(patternn) >= 2
dom(E1@....@En) gives name1..namem
name1..namem distinct
------------------------------------------------------- :: tuple
Tsigma & E |- ( pattern1 , ...., patternn ) : ( t1 * .... * tn ) gives ( E1 @ .... @ En)
%TODO: constraints for linearity (especially partial matches)
Tsigma & E |- pattern1:t1 gives E1 ... Tsigma & E |- patternn:tn gives En
E |- field_name1 : t->t1 ... E |- field_namen : t->tn
length ( (pattern1) ... (patternn) ) >= 1
dom(E1@...@En) gives name1..namem
name1..namem distinct
----------------------------------------------------- :: record
Tsigma & E |- {field_name1=pattern1; ...; field_namen=patternn} : t gives E1@...@En
Tsigma & E |- pattern : t gives E'
Tsigma & E |- pattern' : (t list) gives E''
dom(E') gives name1..namem
dom(E'') gives name1'..namen'
name1..namem name1'..namen' distinct
------------------------------------------------------- :: cons
Tsigma & E |- pattern :: pattern' : (t list) gives E'@E''
defns
JTuprim :: JT ::=
defn
E |- unary_prim : typexpr :: :: uprim :: uprim_ {{ com Unary primitive typing }} by
{{ com
Determines if a unary primitive has a given type. Note that linear references
are useless and, hence, forbidden.
}}
E |- ok
---------------------------------------------------------------- :: not
E |- not : ( bool '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' ( bool '[^' nonlinear '^]' )
E |- ok
---------------------------------------------------------------- :: uminus
E |- ~- : ( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' ( int '[^' nonlinear '^]' )
%linear references are useless because of inplace modification
E |- t : Type
---------------------------------------------------------------- :: ref
E |- ref : (t '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' (t '[^' nonlinear '^]' ref) '[^' nonlinear '^]'
E |- t : Type
---------------------------------------------------------------- :: deref
E |- ! : ( ( t '[^' nonlinear '^]' ) ref) '[^' nonlinear '^]' -> '[^' nonlinear '^]' ( t '[^' nonlinear '^]' )
defns
JTbprim :: JT ::=
defn
E |- binary_prim : typexpr :: :: bprim :: bprim_ {{ com Binary primitive typing }} by
{{ com
Determines if a binary primitive has a given type.
}}
%Though ((=) (obs x)) returns an observer type, such partial applications are to
%be forbidden in expression typing rules.
E |- t : Type
---------------------------------------------------------------- :: equal
E |- = : ( t '[^' observed '^]' ) -> ( ( t '[^' observed '^]' ) -> '[^' observed '^]' ( bool '[^' nonlinear '^]' ))
E |- ok
---------------------------------------------------------------- :: plus
E |- + : ( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' (( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' ( int '[^' nonlinear '^]' ))
E |- ok
---------------------------------------------------------------- :: minus
E |- - : ( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' (( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' ( int '[^' nonlinear '^]' ))
E |- ok
---------------------------------------------------------------- :: times
E |- * : ( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' (( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' ( int '[^' nonlinear '^]' ))
E |- ok
---------------------------------------------------------------- :: div
E |- / : ( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' (( int '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' ( ( int '[^' nonlinear '^]' ) option '[^' nonlinear '^]' ))
E |- t : Type
---------------------------------------------------------------- :: assign
E |- := : ( ( t '[^' nonlinear '^]' ) ref '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' (( t '[^' nonlinear '^]' ) -> '[^' nonlinear '^]' unit '[^' nonlinear '^]')
defns
JTe :: JT ::=
defn
Tsigma & E |- expr : typexpr :: :: e :: e_ {{ com Expression typing }} by
{{ com
Detremines if an expression has a given type. Note that
$[[:user_syntax__typexpr: t]]$ is a type, not a type scheme, but it may contain
type variables (which are recorded in $[[E]]$). $[[Tsigma]]$ gives the types
that should replace type variables in explicitly type-annotated patterns.
While the choice of a rule is mostly syntax-directed (for any given
constructor, a single rule applies, except for $\ottkw{let}$),
polymorphism is handled in a purely declarative manner. The
choice of instantiation for a polymorphic bound variable or primitive is free,
as is the number of variables introduced by a polymorphic $\ottkw{let}$.
}}
E |- unary_prim : t
E |- t == t'
------------------------------------------------------- :: uprim
Tsigma & E |- (%prim unary_prim) : t'
E |- binary_prim : t
E |- t == t'
------------------------------------------------------- :: bprim
Tsigma & E |- (%prim binary_prim) : t'
:JTvalue_name: E |- value_name : t
E |- t == t'
------------------------------------------------------- :: ident
Tsigma & E |- value_name : t'
:JTconst: E |- constant : t
E |- t == t'
------------------------------------------------------- :: constant
Tsigma & E |- constant : t'
Tsigma & E |- e : t
E |- t' <= Tsigma src_t
E |- t == t'
------------------------------------------------------- :: typed
Tsigma & E |- (e:src_t) : t
%TODO: add constraints for linearity
Tsigma & E |- e1:t1 .... Tsigma & E |- en:tn
length (e1)....(en) >= 2
E |- ( t1 * .... * tn ) == t'
------------------------------------------------------- :: tuple
Tsigma & E |- e1,....,en : t'
%TODO: add constraints for linearity
:JTconstr_p:E |- constr : t1...tn->t
Tsigma & E |- e1 : t1 ... Tsigma & E |- en : tn
E |- t == t'
------------------------------------------------------- :: construct
Tsigma & E |- :Expr_construct: constr (e1,...,en) : t'
%TODO: add constraints for linearity
Tsigma & E |- e1 : t
Tsigma & E |- e2 : t list
E |- t list == t'
------------------------------------------------------- :: cons
Tsigma & E |- e1 :: e2 : t'
%TODO: add constraints for linearity
Tsigma & E |- e1 : t1 ... Tsigma & E |- en : tn
E |- field_name1 : t->t1 ... E |- field_namen : t->tn
t = (t1', ..., tl') typeconstr_name
E |- typeconstr_name gives typeconstr_name:kind {field_name1'; ...; field_namem'}
field_name1...field_namen PERMUTES field_name1'...field_namem'
length (e1)...(en)>=1
E |- t == t'
----------------------------------------------------- :: record_constr
Tsigma & E |- {field_name1=e1; ...; field_namen=en} : t'
%TODO: add constraints for linearity
Tsigma & E |- expr : t
E |- field_name1 : t->t1 ... E |- field_namen : t->tn
Tsigma & E |- e1 : t1 ... Tsigma & E |- en : tn
field_name1...field_namen distinct
length (e1) ... (en) >= 1
E |- t == t'
----------------------------------------------------- :: record_with
Tsigma & E |- {expr with field_name1=e1; ...; field_namen=en} : t'
%TODO: add constraints for linearity
Tsigma & E |- e : t1 -> t
Tsigma & E |- e1 : t1
------------------------------------------------------- :: apply
Tsigma & E |- e e1 : t
%TODO: add constraints for linearity
Tsigma & E |- e : t
E |- field_name : t->t'
E |- t' == t''
----------------------------------------------------- :: record_proj
Tsigma & E |- e.field_name : t''
%TODO: add constraints for linearity
Tsigma & E |- e1 : bool
Tsigma & E |- e2 : bool
E |- bool == t
------------------------------------------------------- :: and
Tsigma & E |- e1 && e2 : t
%TODO: add constraints for linearity
Tsigma & E |- e1 : bool
Tsigma & E |- e2 : bool
E |- bool == t
------------------------------------------------------- :: or
Tsigma & E |- e1 || e2 : t
%TODO: add constraints for linearity
Tsigma & E |- e1:bool
Tsigma & E |- e2:t
Tsigma & E |- e3:t
------------------------------------------------------- :: ifthenelse
Tsigma & E |- if e1 then e2 else e3 : t
%TODO: add constraints for linearity
Tsigma & E |- e1 : bool
Tsigma & E |- e2 : unit
E |- unit == t
------------------------------------------------------- :: while
Tsigma & E |- while e1 do e2 done : t
%TODO: add constraints for linearity
Tsigma & E |- e1 : int
Tsigma & E |- e2 : int
Tsigma & E,:VN_id:lowercase_ident:int |- e3 : unit
E |- unit == t
------------------------------------------------------- :: for
Tsigma & E |- for lowercase_ident = e1 for_dirn e2 do e3 done : t
%TODO: add constraints for linearity
Tsigma & E |- e1 : unit
Tsigma & E |- e2 : t
------------------------------------------------------- :: sequence
Tsigma & E |- e1; e2 : t
{{ com
In the above rule, $[[e1]]$ must have type $[[:user_syntax__typeconstr: unit]]$.
Ocaml lets the programmer off with a warning, unless \texttt{-warn-error~S} is
passed on the compiler command line.
}}
%TODO: add constraints for linearity
Tsigma & E |- e:t
Tsigma & E |- pattern_matching : t -> t'
------------------------------------------------------- :: match
Tsigma & E |- match e with pattern_matching:t'
Tsigma & E |- pattern_matching : t -> t'
E |- t -> t' == t''
------------------------------------------------------- :: function
Tsigma & E |- function pattern_matching : t''
{{ com
We give three rules for $\ottkw{let}$ expressions. The rule
\ottdruleref{JTe\_let\_mono} describes ``monomorphic let'': it does not allow the
type of $[[expr]]$ to be generalised. The rule \ottdruleref{JTe\_let\_poly}
describes ``polymorphic let'': it allows any number of type variables in the
type of $[[:user_syntax__non_expansive: nexp]]$ to be generalised (more
precisely, this generalisation applies simultaneously to the types of all the
variables bound by $[[pat]]$), at the cost of requiring
$[[:user_syntax__non_expansive: nexp]]$ to be non-expansive (which is described
syntactically through the grammar for $[[:user_syntax__non_expansive: nexp]]$).
The rule \ottdruleref{JTe\_letrec} allows mutually recursive functions to be
defined; since immediate functions are values, thus nonexpansive, there is no
need for a monomorphic $\ottkw{let\:rec}$ rule.
}}
%TODO: add constraints for linearity
Tsigma & E |- pat=expr gives x1:t1, .., xn:tn
Tsigma & E@ x1:t1, .., xn:tn |- e : t
------------------------------------------------------- :: let_mono
Tsigma & E |- let pat=expr in e : t
%TODO: add constraints for linearity
shift 0 1 Tsigma & E,TV |- pat=nexp gives x1:t1, .., xn:tn
Tsigma & E@ x1:forall t1, .., xn:forall tn |- e : t
------------------------------------------------------- :: let_poly
Tsigma & E |- let pat=nexp in e : t
%TODO: add constraints for linearity
shift 0 1 Tsigma & E,TV |- letrec_bindings gives x1:t1, ..., xn:tn
Tsigma & E@(x1:forall t1), ..., (xn:forall tn) |- e : t
------------------------------------------------------- :: letrec
Tsigma & E |- let rec letrec_bindings in e : t
%TODO: add constraints for linearity
E |- ok
E |- location gives location:t
E |- t ref '[^' nonlinear '^]' == t'
------------------------------------------------------- :: location
Tsigma & E |- location : t'
defn
Tsigma & E |- pattern_matching : typexpr -> typexpr' :: :: pat_matching :: pat_matching_ {{ com Pattern matching/expression pair typing }} by
{{ com
Determines the function type of a sequence of pattern/expression pairs. The
function type desribes the type of the value matched by all of the patterns and
the type of the value returned by all of the expressions. $[[Tsigma]]$ gives
the types that should replace type variables in explicitly type-annotated
patterns.
}}
%TODO: add constraints for linearity
Tsigma & E |- pattern1:t gives E1 ... Tsigma & E |- patternn:t gives En
Tsigma & E@E1 |- e1:t' ... Tsigma & E@En |- en:t'
length (pattern1)...(patternn) >= 1
------------------------------------------------------- :: pm
Tsigma & E |- pattern1 -> e1 | ... | patternn -> en : t -> t'
defn
Tsigma & E |- let_binding gives E' :: :: let_binding :: let_binding_ {{ com Let binding typing }} by
{{ com
Determines the types bound by a let bindings pattern.
}}
Tsigma & E |- pattern : t gives x1:t1, .., xn:tn
Tsigma & E |- expr : t
------------------------------------------------------- :: poly
Tsigma & E |- pattern = expr gives (x1:t1), .., (xn:tn)
defn
Tsigma & E |- letrec_bindings gives E' :: :: letrec_binding :: letrec_binding_ {{ com Recursive let binding typing }} by
{{ com
Determines the types bound by a recursive let's patterns (which are always just variables).
}}
{{ com
\ottbreakconclusionlinetrue
}}
%TODO: add constraints for linearity
%%WIDTH: >~a4/landscape/normalsize
E' = E@value_name1:t1->t1',...,value_namen:tn->tn'
Tsigma & E' |- pattern_matching1 : t1->t1' ... Tsigma & E' |- pattern_matchingn : tn->tn'
value_name1 ... value_namen distinct
------------------------------------------------------- :: equal_function
Tsigma & E |- value_name1 = function pattern_matching1 and ... and value_namen = function pattern_matchingn gives value_name1:t1->t1', ..., value_namen:tn->tn'
{{ com
\ottbreakconclusionlinefalse
}}
>>
<<
defns
JTconstr_decl :: JT ::=
defn
type_params_opt typeconstr |- constr_decl gives EB :: :: constr_decl :: constr_decl_ {{ com Variant constructor declaration }} by
{{ com
Collects the constructors of a variant type declaration using named type
schemes for the type parameters.
}}
------------------------------------------------------- :: nullary
(tv1, ..., tvn) typeconstr |- constr_name gives constr_name of typeconstr
------------------------------------------------------- :: nary
(tv1, ..., tvn) typeconstr |- constr_name of t1*...*tn gives constr_name of forall (tv1, ..., tvn), (t1,...,tn) : typeconstr
defns
JTfield_decl :: JT ::=
defn
type_params_opt typeconstr_name |- field_decl gives EB :: :: field_decl :: field_decl_ {{ com Record field declaration }} by
{{ com
Collects the fields of a record type using named type schemes for the type
parameters.
}}
------------------------------------------------------- :: only
(tv1, ..., tvn) typeconstr_name |- fn:t gives fn:forall (tv1, ..., tvn), typeconstr_name -> t
defns
JTtypedef :: JT ::=
defn
|- typedef1 and .. and typedefn gives E' and E'' and E''' :: :: typedef :: typedef_ {{ com Type definitions collection }} by
{{ com
A type definition declares several sorts of names: type constructors
(some of them corresponding to freshly generated types, others to type
abbreviations), and data constructors and destructors. These names are
collected into three environments:
\begin{itemize}
\item $[[E']]$ contains generative type definitions (variant and record types);
\item $[[E'']]$ contains type abbreviations;
\item $[[E''']]$ contains constructors and destructors for generative datatypes.
\end{itemize}
The order $[[E']]$, $[[E'']]$, $[[E''']]$ is chosen so that their
concatenation is well-formed, because no component may refer to a
subsequent one. The first component $[[E']]$, only contains
declarations of names which do not depend on anything. The second
component $[[E'']]$ contains type abbreviations topologically sorted
according to their dependency order, which is possible since we
do not allow recursive type abbreviations (in Objective Caml,
without the \texttt{-rectypes} compiler option, recursive type
abbreviations are only allowed when guarded polymorphic variants and
object types) --- recursive types must be guarded by a generative
datatype. Finally $[[E''']]$ declares constructors and destructors for
the types declared in $[[E']]$; $[[E''']]$ may refer to types declared
in $[[E']]$ or $[[E'']]$ in the types of the arguments to these
constructors and destructors.
This judgement form does not directly assert the correctness of the
definitions: this is performed by the rule
\ottdruleref{JTtype\_definition\_list} below, which states that the
environment assembled here must be well-formed.
}}
------------------------------------------------------- :: empty
|- gives empty and empty and empty
|- </typedefi//i/> gives E and E' and E''
------------------------------------------------------- :: eq
|- type_params_opt typeconstr_name = t and </typedefi//i/> gives E and E',(type_params_opt typeconstr_name = t) and E''
{{ com
\ottbreakconclusionlinetrue
}}
%%WIDTH: >~a4/landscape/normalsize
|- </typedefi//i/> gives E and E' and E''
|- type_params_opt : kind
type_params_opt typeconstr_name |- constr_decl1 gives EB1 ... type_params_opt typeconstr_name |- constr_decln gives EBn
------------------------------------------------------- :: def_sum
|- type_params_opt typeconstr_name = constr_decl1 | ... | constr_decln and </typedefi//i/> gives E, (typeconstr_name : kind) and E' and E''@EB1,...,EBn
{{ com
A variant type definition yields two sorts of bindings: one for the type
constructor name and one for each constructor.
}}
%%WIDTH: >>a4/landscape/normalsize
|- </typedefi//i/> gives E and E' and E''
|- type_params_opt : kind
type_params_opt typeconstr_name |- field_name1:t1 gives EB1 ... type_params_opt typeconstr_name |- field_namen:tn gives EBn
------------------------------------------------------- :: def_record
|- type_params_opt typeconstr_name = {field_name1:t1; ...; field_namen:tn} and </typedefi//i/> gives E, (typeconstr_name : kind {field_name1; ...; field_namen}) and E' and E''@EB1,...,EBn
{{ com
A record type definition yields two sorts of bindings: one for the type
constructor name and one for each field. The field names are also recorded
with the type constructor binding; this information is used in the rule
\ottdruleref{JTe\_record\_constr} to make sure that record expressions
specify all fields. (We would similarly tag type constructor bindings for
variant types with their constructor names if we wanted to check the
exhaustivity of pattern matching.)
}}
{{ com
\ottbreakconclusionlinefalse
}}
defns
JTtype_definition :: JT ::=
defn
E |- type_definition gives E' :: :: type_definition :: type_definition_ {{ com Type definition well-formedness and binding collection }} by
{{ com
Collects the bindings of a type definition and ensures that they are
well-formed. Any given name may be defined at most once, and all names used
must have been bound previously or earlier in the same type definition phrase.
The conditions are checked by the premise $[[E@E'''' |- ok]]$ in the rule
\ottdruleref{JTtype\_definition\_list} and the assembly is performed by the
type definitions collection rules above. This implies that the type
abbreviations must be topologically sorted in their dependency order.
(Generative type definitions are exempt from such constraints.) Programmers do
not have to abide by this constraint: they may order type abbreviations in any
way. Therefore the rule \ottdruleref{JTtype_definition_swap} allows an
arbitrary reordering of type definitions --- it suffices for a type definition
to be correct that there exist a reordering that makes the type abbreviations
properly ordered.
}}
|- typedef1 and ... and typedefn gives E' and E'' and E'''
E'''' = E'@E''@E'''
E@E'''' |- ok
------------------------------------------------------- :: list
E |- type typedef1 and ... and typedefn gives E''''
E |- type </typedefi//i/> and typedef' and typedef and </typedefj''//j/> gives E'
------------------------------------------------------- :: swap
E |- type </typedefi//i/> and typedef and typedef' and </typedefj''//j/> gives E'
{{ com
}}
defns
JTdefinition :: JT ::=
defn
E |- definition : E' :: :: definition :: definition_ {{ com Definition typing }} by
{{ com
Collects the bindings of a definition and ensures that they are well-formed.
Each definition can bind zero, one or more names. Type variables that are
mentionned by the programmer in type annotations are scoped at this level.
Thus, the $[[Tsigma]]$ substitution is arbitrarily created for each definition
to ensure that each type variable is used consistently in the definition.
}}
Tsigma & E,TV |- pat=nexp gives (x1:t1'),..,(xk:tk')
------------------------------------------------------- :: let_poly
E |- let pat = nexp : (x1:forall t1'),..,(xk:forall tk')
Tsigma & E |- pat=expr gives (x1:t1'),..,(xk:tk')
------------------------------------------------------- :: let_mono
E |- let pat = expr : (x1:t1'),..,(xk:tk')
Tsigma & E,TV |- letrec_bindings gives (x1:t1'),..,(xk:tk')
------------------------------------------------------- :: letrec
E |- let rec letrec_bindings : (x1:forall t1'),..,(xk:forall tk')
E |- type typedef1 and ... and typedefn gives E'
------------------------------------------------------- :: typedef
E |- type typedef1 and ... and typedefn : E'
defns
JTdefinitions :: JT ::=
defn
E |- definitions : E' :: :: definitions :: definitions_ {{ com Definition sequence typing }} by
{{ com
Collects the bindings of a definition and ensures that they are well-typed.
}}
E |- ok
---------------------------------------------------------------- :: empty
E |- : :Env_list:
%TODO: add constraints for linearity
:JTdefinition:E |- definition : E'
:JTdefinitions:E@ E' |- definitions' : E''
---------------------------------------------------------------- :: item
E |- definition definitions' : E'@E''
defns
JTprog :: JT ::=
defn
E |- program : E' :: :: prog :: prog_ {{ com Program typing }} by
{{ com
Checks a progam.
}}
:JTdefinitions: E |- definitions : E'
----------------------------------------------------- :: defs
E |- definitions : E'
>>
<<
defns
JTstore :: JT ::=
defn
E |- store : E' :: :: store :: store_ {{ com Store typing }} by
{{ com
Checks that the values in a store have types.
}}
------------------------------------------------------- :: empty
E |- empty : :Env_list:
E |- store : E'
<<>> & E |- v : t
------------------------------------------------------- :: map
E |- store, l |-> v : E',(l:t)
>>
<<
defns
JTtop :: JT ::=
defn
E |- < program , store > : E' :: :: top :: top_ {{ com Top-level typing }}
{{ tex [[E]] \vdash \langle [[program]], [[store]] \rangle }} by
{{ com
Checks the combination of a program with a store. The store is typed in an
environment that includes its bindings, so that it can contain cyclic
structures.
}}
E@E' |- store : E'
:JTprog:E@E' |- program : E''
------------------------------------------------------- :: defs
E |- <program, store> : E'@E''
>>
<<
defns
JTLin :: JT ::=
defn
Tsigma & E |- L :: :: Lin :: Lin_ {{ com Label-to-environment extraction }} by
{{ com
Used in the proof only
}}
------------------------------------------------------- :: nil
Tsigma & E |-
dom(E) gives names
location notin names
------------------------------------------------------- :: alloc
Tsigma & E |- ref v = location
Tsigma & E |- v : t
E |- location gives (location:t)
------------------------------------------------------- :: deref
Tsigma & E |- !location = v
------------------------------------------------------- :: assign
Tsigma & E |- location := v
defns
JTLout :: JT ::=
defn
Tsigma & E |- L gives E' :: :: Lout :: Lout_ {{ com Label-to-environment extraction }} by
{{ com
Used in the proof only
}}
------------------------------------------------------- :: nil
Tsigma & E |- gives :Env_list:
Tsigma & E |- v : t
------------------------------------------------------- :: alloc
Tsigma & E |- ref v = location gives (location:t)
------------------------------------------------------- :: deref
Tsigma & E |- !location = v gives :Env_list:
Tsigma & E |- v : t
E |- location gives (location:t)
------------------------------------------------------- :: assign
Tsigma & E |- location := v gives :Env_list:
%% The next com is a hack to get the title in the right place when
%% typesetting the reduction rules after the typing rules.
{{ com
\section{Operational Semantics}
\label{sec.runtime}
The operational semantics is a labelled transition system that lifts imperative
and non-deterministic behavior our of the core evaluation rules.
Notable aspects of the formalization include:
\begin{itemize}
\item
explicit rules for evaluation in context (instead of a grammar of evaluation contexts),
\item
substitution-based function application,
\item
right-to-left evaluation ordering, which is overspecified compared to the OCaml
manual; furthermore, this choice of evaluation ordering for record expressions
differs from the implementation's choice, which is based on the type
declaration,
\item
unlike the implementation, we do not treat curried functions specially.
\item
As in the type system, several rules have premises that state there are at
least 1 (or 2) elements of a list, despite there being 3 or 4 dots. This is
because Ott does not use dot imposed length restrictions in the theorem prover
models.
\end{itemize}
}}
embed
{{ coq
Hint Constructors JdomEB JdomE Jlookup_EB Jidx_bound
JTtps_kind
JTEok JTtypeconstr JTts JTtsnamed JTt
JTeq JTidxsub JTinst JTinst_named JTinst_any
JTvalue_name JTfield
JTconstr_p JTconstr_c
JTconst
JTpat
JTuprim JTbprim
JTe JTpat_matching JTlet_binding JTletrec_binding
JTstore JTLin JTLout
: rules.
}}
{{ coq
Hint Constructors JTconstr_decl JTfield_decl JTtypedef JTtype_definition
JTdefinition JTdefinitions
JTprog JTtop
: rules.
}}