Changes between Version 39 and Version 40 of LinearTypes/Implementation


Ignore:
Timestamp:
Dec 24, 2018 2:49:29 PM (12 months ago)
Author:
monoidal
Comment:

Zero is no longer a multiplicity

Legend:

Unmodified
Added
Removed
Modified
  • LinearTypes/Implementation

    v39 v40  
    4747{{{
    4848#!haskell
    49 data Mult = Zero
    50           | One
     49data Mult = One
    5150          | Omega
    5251          | MultAdd Mult Mult
     
    5857
    5958The checking algorithm is as follows:
    60 - The typechecking monad is enriched with an extra writer-like state called the ''usage environment'', which is a mapping from variables to multiplicities.
     59- The typechecking monad is enriched with an extra writer-like state called the ''usage environment'', which is a mapping from variables to multiplicities. Variables not present in the usage environment are considered to have usage Zero (which is not a multiplicity).
    6160- The usage environment output by `u v` is `U1 + p * U2` where
    6261   * `U1` is the usage environment output by `u`
     
    8281In order to use the normal unification machinery, we eventually call `tc_sub_type_ds` but before that we check for domain specific rules we want to implement such as `1 <= p` which is achieved by calls to `submult` or `submultMaybe`.
    8382
    84 {{{#!box note
    85 The `Zero` multiplicity is an avatar of the type checking algorithm, and doesn't correspond to a user-facing multiplicity. We will probably take it out in a separate type.
    86 }}}
    87 
    8883==== Solving constraints
    8984
    90 Constraint solving is not completely designed yet. The current implementation follows very simple rules, to get the implementation off the ground. Basically both equality and inequality constraints are treated as syntactic equality unification (as opposed, in particular, to unification up to laws of multiplicities as in the proposal). There are few other rules (described below) which are necessary to type even simple linear programs:
     85Constraint solving is not completely designed yet. The current implementation follows very simple rules, to get the implementation off the ground. Basically both equality and subsumption constraints are treated as syntactic equality unification (as opposed, in particular, to unification up to laws of multiplicities as in the proposal). There are few other rules (described below) which are necessary to type even simple linear programs:
    9186
    9287===== The 1 <= p rule