My favorites | Sign in
Project Home Wiki Issues Source
READ-ONLY: This project has been archived. For more information see this post.
Search
for
Calculus  
A calculus for Scala with higher-kinded types
Updated Feb 5, 2010 by adria...@gmail.com

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

Powered by Google Project Hosting