Syntax
about the grammar:
@> is a combinator that takes a parser and a scope identifier and returns a parser that adds the parsed binder to that scope
>@ is a combinator that takes a scope identifier and a parser and returns a parser that activates that scope for the duration of the original parser
''', '>@', '@>', '(', ')', '|' and '*' are reserved for the grammar -- must be quoted
ident
label
tm =
( ident // variable
| new tp // instantiating a type -- may result in a polymorphic value (abstract [type|value] members)
// re-used as syntax for objects (values)
| tm . label // selecting a label on a term -- only allowed on concrete values: no abstract members
// NOTE: self variable always has a concrete type. e.g {x => val a: Int; val res: Int=x.a}
// ^^^ allowed
// the `x.a' will only be evaluated when res is accessed first (and res may only be accessed on a concrete value)
// TODO: ok to select a member on a value with abstract type members?
// TODO: find a valid example (this isn't one: y: x.t, x: {type t;val a: t=y} |- x.a : x.t, as x escapes its scope)
| tm & template // value refinement: make one or more abstract members of tm concrete
)
template = { ident@>s : tp => s>@(mem*(;)) } // a template: declares a type ('tp') for the self variable ('ident'), which is bound ('s>@') in the ;-separated list of members ('mem*(;)')
v = new template // these mem's must be able to specify concrete value members (VALinTP?)
// should types be omitted?
// - a type member may be selected on an object anyway
// + the object itself isn't needed to specify the selected type, the object's type suffices
// + phase separation: operationally, these types are not necessary
// - do need a rule to evaluate `new tp' (if we can't eradicate all types from opsem, why do it at all)
// --> couldn't expand `tp' to its list of members statically, this is clearly a run-time operation
tp =
( template // TODO: should a type specify the concrete value for a value member (VALinTP?)?
| tp # label //
// only really need to track "abstractness"
// a type describes the type of the members of its instances, also describing the value is just some kind of extremely precise type
| tp & tp //
| tm . type //
| self // explicit notiation for the implicit recursive self-type
//| impure tp // [IMPURE] when we add effects, not every term is a path,
// member initialisation may become more tricky (maybe not: val x: impure t = someImpureThingy) -- thought we needed a rule to
// evaluate RHS of member def, as we want to replace path by path, but a term with impure type isn't a path
//| exact tp // [EXACTP] exact types: types w/o subsumption
)
mem =
( val label : tp
| val label : tp = tm //
| type label <: tp >: tp // TODO: include definition-site variance
| type label = tp
| type label <@ tp // nominal type
)Helper Relations
We use HOAS in the rules: object-level abstraction is denoted using meta-level abstraction, object-level substitution is meta-level application.
Expansion: <~
yields the list of members contained in a type, does not preserve type equality in the sense that tp <~ members does not imply t =:= {_: t => members}
Member lookup: lookup
Combining list of members: mix
Small-step structured operational semantics
have operational and static semantics share the same helper relations as much as possible cycles should be modelled by cycles: {x => val a=x.b; val b=x.a}.a should not get stuck, it should loop
tp <~ members // expand the type tp to its list of members (HOAS: abstracts over the self-variable)
lookup(label, members (new tp), `val _ : _ = tm') // label is bound to tm in members, with (new tp) used as the self-variable (HOAS: applying `members' to `(new tp)' means replacing members's free variable with `(new tp)')
------------------------------------ [eval/sel@v]
(new tp).label --> tm
TOrig <~ OrigMems
merge OrigMems RefineMems AllMems
-------------------------------------------- [eval/mix@v]
(new TOrig) & RefineMems --> new {x: self => AllMems}Context Rules
evaluaton proceeds ...
- under member selection: [].label
- under value-composition: [] & tp
- under member definition?
- in dependent types?
- context function becomes a lot more complex
- maybe better to incorporate some kind of evaluation in type equivalence
Static Semantics
Typing rules: (G |- is implicit)
Type Assignment
(TODO: use bidirectional typing rules?)
expands T SelfT Mems % T must expand to a list of members with self type SelfT
% (T is not necessarily equivalent to a structural type -- e.g., nominal type binding)
T < SelfT % subtyping ignores abstract vs concrete members
% T may have abstract type/value members to model polymorphic lambda's as values
selfv : SelfT |- WF@mems (Mems selfv) % assuming a self variable of the right type,
% the members must be well-formed (also checks there are not duplicates)
---------------------------------------------------------- [of/new]
new T : T // or should we remove the values from the type of new tp ?
Tgt : TTgt // Tgt is of type TTgt
concrete@tp TTgt // TTgt does not have abstract members
expands TTgt _ Mems // TTgt expands to a list of members Mems (abstracts over self-variable) -- TTgt < '_' should be admissible
lookup Label (Mems Tgt) Mem // lookup Label in the list of members (where the self variable is replaced by Tgt)
// [IMPURE] TODO: if TTgt is impure, substituting Tgt may result in paths becoming impure..
inversion@mem/val/tp Mem TMem. // get the result type for this member -- well-formedness ensures Label is bound to a value of type TMem
---------------------------------------------------------- [of/sel@v]
Tgt . Label : TMem
Orig : TOrig // Orig is of type TOrig
expands TOrig TOrigSelf OrigMems // TOrig expands to a list of members OrigMems with self-type TOrigSelf
merge OrigMems RefinedMems AllMems // merging OrigMems with RefinedMems yields AllMems
// given a typing derivation for the self-type, the refined list of members must be well-formed
// must include new members in self type, as they may contribute concrete type members
selfv : {x: TOrigSelf & {_ => RefinedMems} => RefinedMems} |- WF@mems (AllMems selfv)
----------------------------------------------------------------------------------------- [of/mix@v]
Orig & {RefinedMems} : TOrig & {x: TOrigSelf & {_ => RefinedMems} => RefinedMems}
TM : TP'
//[EXACTP] <- subsumable TP' // to support exact types, only allow subsumption selectively
TP' < TP
-------------------------------- [of/sub] // --> rules no longer syntax directed.
TM : TP // preservation up to subtyping becomes easier to prove (dismissing hypothetical judgements modulo subtyping), what exactly is harder?
Type Equality
algorithmic rules vs more direct rules (that include transitivity,...)
- pro's
syntax directed rules --> inversion
- con's
prove transitivity, symmetry separately
normalisation (expands to structural type if possible -- expansion of nominal types doesn't preserve equality)
A <~ memsA B <~ memsB selfTp = A & B // TODO: should it be possible to specify selfTp ? (see nuObj)
self: selfTp |- ForAll newM in (memsB self). // put a hypothetical self variable in the context
l=label(newM), lookup(l, memsA self, AM), newM <m< AM // must be a refinement:
mix(memsA, memsB, memsMix) //
------------------------------------------- [=:=-mix]
A & B =:= {_: selfTp => memsMix}
expand type alias
Subtyping
includes type equality
Well-formedness
Remarks
paths: every term is a path, since there are no side-effects
path-equality must be decidable (syntactic equality modulo de-referencing members)
encoding polymorphic values: via type passing vs. abstract objects
type passing: run-time types
- opsem becomes more complicated
- no erasure
- DGP (SYB) more interesting
abstract objects
- type passing is not essential for intensional type analysis (see Crary&Weirich)
Extensions
exact types: no subsumption (colouredpoint problem), interaction with virtual classes state: impure types