notes.rtf

{\rtf1\ansi\ansicpg1252\cocoartf1038\cocoasubrtf290
{\fonttbl\f0\fswiss\fcharset0 Helvetica;}
{\colortbl;\red255\green255\blue255;}
\margl1440\margr1440\vieww15340\viewh12720\viewkind0
\pard\tx720\tx1440\tx2160\tx2880\tx3600\tx4320\tx5040\tx5760\tx6480\tx7200\tx7920\tx8640\ql\qnatural\pardirnatural

\f0\fs24 \cf0 EL e^L =~ e^L?\
LE e^E =~ e^E?\
\
(K 0) (LE \\omega)\
(K 0) (EL \\omega)\
\
((LE K) I) \\omega\
\
Potential problems: diverge, error (if in model!)\
\
L's K is NOT E's K, it's equivalent!\
L's K doesn't use 2nd arg, no diverge.\
LE K (L's K) MUST NOT cause diverge!\
LE K is an L fct!\
\
Changing which exps are evaluated changes what fcts compute\
Restricting eval's exps (lazy) restricts the places where exps diverge\
\
Interop ought not to change what functions compute\
Converted functions ought not to diverge where they did not before, and vice versa\
Assumed types add arg/result checks and conversions, but do not change fcts\
\
Restricted eval exps must be mirrored in other langs to preserve fct behavior\
More strict veal can cause new behavior: diverge, errors\
\
Lazy behavior is superset of eager behavior, more expressible that does not change fct behavior\
\
Eager fct converted to lazy that diverges: K\
	Illustrates need for force/unforce evaluation cxts\
\
Lazy fct translated to eager that diverges: Y\
	Cannot mechanically translate terms: Y combinator diverges\
\
No lazy fct exists that, when converted to eager without extra force points, computes differently/diverges\
\
Labels can use tyvars after all, since labels are well-formed only if the underlying type is well-formed, the mark is irrelevant, can be tyvar!!\
\
==\
\
SOME VALUES EXPRESSIBLE IN LAZY AND NOT EAGER ONES\
\
Can simulate recursive lazy values in eager languages with thunks and forcing.\
\
fix \\ x : [N] . cons 1 x\
Lazy: it's a value\
Eager: diverges\
\
fix \\ f : [N] -> [N] . \\ x : [N] . cons 1 f\
Eager: works, value, must force thunks\
\
==\
\
FIXED POINT OPERATIONS\
\
Operand types are the same for H and M (t->t) because the same definition works for both H and M, it doesn't diverge in M because application isn't used to substitute.\
\
==\
\
STRIPPING LABELS\
\
Reduction rules must strip labels because the expressions the underlying types are put into are expected to have the underlying types.  If not, the outer expression would be ill-typed.  An alternative would be to strip the labels in the typing rules, like they are for guards.\
\
==\
\
WHY TYPES ON GUARDS ARE NEEDED\
\
For the matching labels mechanism, and for type-directed value conversion in guards, which represent language boundaries.\
\
==\
\
TYVARS AS LABELS IS SAFE\
\
Label confusion not possible because no free tyvars.  If nested forall, outer forall will go away when reducing inner forall.  Reduction of HS/MS is referentially transparent.\
\
==\
\
LUMP TYPES\
\
The only H and M expressions that can have lump types, as in:\
\
HM L ?\
\
MH L ?\
\
are Scheme importation guards, e.g. HS or MS:\
\
HM L (MS L 0)\
\
Anything else would not be well-typed, so you don't have to account for it in the op sem.\
\
==\
\
??? MAKE SURE THIS IS TRUE AFTER THE SWITCH TO CONVERSION SCHEMES ???\
\
TYPE LABELS CANNOT BE NESTED\
\
Eval contexts guarantee that type labels created by applying an imported type abstraction from Scheme cannot be nested, so the type label removal substitution notation t[ti/ti.x] can mean to remove all type labels. Also why the Parametricity Violated red rule can strip the label.\
\
==\
\
LABELS STRIPPED ON HS AND MS GUARD REDUCTIONS\
\
Because the typing rules for the expressions that are the results of these reduction rules do not account for labels, and for these reductions to be useful to outer expressions that do not anticipate label types, the types must be stripped.  This happens for any reduction which produces an expression that contains a type that originates from the guard type.\
\
==\
\
VARIABLE LANGUAGE SUPERSCRIPTS\
\
MUST add language subscripts to variables 'x' and type variables 'X' because otherwise \\x:N.(N^HM x) and \\\\X.^(X->N)HM (\\x:X.0) are well typed! Explaining that vars/tyvars separate between langs and losing subscripts will make syntax unreadable, not enough fonts to distinguish.\
\
==\
\
LABEL AND LUMP TYPES ONLY FOR INTEROP\
\
Uses elsewhere by the programmer are errors.  This allows me to not address the guard reduction cases for these types, which is beyond the scope of this paper.\
\
As such, HS L v uses 'v' because L is only used for the importation of type abstractions into Scheme, which, if the type variable is ever used and the inner expression is well-typed, should yield a function at some point, and since function arguments are unforced, the only expressions in HS L ? would be unforced Scheme values 'v^s'.\
\
==\
\
UNFORCED VALUE USED IN H/MS L V^S\
\
Unforced because lumps are special, only used by the system. Where the system uses them (for functions), the possible expressions that could be substituted into an HS L ? is exactly represented by v^s, since all Scheme arguments are v^s (doesn't force H/M importation guards).\
\
==\
\
FORCED VALUE USED IN H/MS (AX.T) W^S\
\
Forced because HS (Ax.t) v^s is reducible via HS t E^s, which reduces inside SH guards, so we use forced value w^s to exclude the possibility of SH guards.\
\
==\
\
LABELS AND LUMPS USABLE ONLY BY THE SYSTEM\
\
Any uses by the programmer is an error like type errors.  Thus there are missing reduction rules/other missing considerations that would result in stuck states, maybe bad types, etc. if this is ignored.\
\
==\
\
SH/SM FORALL TYPE ABSTRACTIONS CANNOT ROUNDTRIP\
\
SH/M (Ax.t) (\\\\x.e) loses the type abstraction, so you cannot roundtrip a type abstraction into and then out of Scheme.  This is okay, though, because the only kind of polymorphic function in Scheme is just a regular function, or the function might be inside another value.  The roundtrip side of this is (H/MS (Ax.t) w^s) \{t\}, which defers importing these (ad-hoc) polymorphic functions until H/M has a use for them, then it doesn't have to worry about converting the Scheme forced value into a type abstraction if it's necessary.  So we lose the type abstraction going from an explicitly (parametric) polymorphic value in H/M to an implicitly (ad-hoc) polymorphic value in S using lumps, and we reverse the process by deferring the conversion of polymorphic values into H/M until applied to a type, and verified with labels.  Two sides of the same coin, or something.\
\
NOTE: You now get the type abstraction back if you're expecting a polymorphic value back.\
\
==\
\
REMOVED H/MS FORALL FORCED VALUES\
\
Convert to wrapped type abstraction instead. Improvement to David's model.\
\
==\
\
CONVERSION OF TYPE ABSTRACTIONS FOR HM/MH CONVERTS H TYPES TO/FROM M TYPES\
\
The conversion wraps the imported type abstraction in a proxy type abstraction, but the mechanism that substitutes the type argument into the imported type abstraction must first convert the type into an equivalent form in the other language.  This is new, and should be discussed.  You may have to define what equality of types and conversion of types means very explicitly.\
\
==\
\
DIFFERENT H/M TYPES TO PREVENT TYPE APPLICATIONS SUBSTITUTING TYVARS IN OTHER LANG\
\
Don't want to substitute an H type for x^m, etc.\
\
==\
\
LUMPS PERMIT SCHEME TO SUPPLY ARGUMENTS OF ANY TYPE\
\
Okay, doesn't break H/M's type system. Scheme has no expectations, it supplies what it wants, it has to check what it gets back, just like everything else.\
\
==\
\
HM/MH SHOULD NOT BE STRIPPED OF LABELS IN TYPING RULES\
\
Labels inserted/removed by the system for Scheme importations.  Anything happening inside Scheme should keep the labels so they can eventually work their way back to the outer Scheme importation and be removed.\
\
==\
\
TYVARS AS LABELS SAFE FOR NESTED FORALL TYPES WITH IDENTICAL PARAMETERS\
\
Safe in all two cases: (1) forall appears in function argument type position, in which case lumps are involved instead of labels, and (2) forall appears in function result position, in which case the same reduction happens, and the identical labels never make it outside the original guard for the nested forall type.\
\
==\
\
LABELS STRIPPED IN REDUCTION RULES AND TYPING RULES\
\
Reduction rules, to keep labels from spreading outside the original, outermost guard.  Typing rules, so expressions outside the outermost guard don't have to know about labels as an interop mechanism.\
\
==\
\
EMBEDDINGS\
\
My model uses both natural and lump embeddings (see Matthews).\
\
==\
\
TYVAR IN LABEL IS NOT FREE\
\
Cannot substitute it, like the forall tyvar.\
\
==\
\
CONVERTING GENERAL TYPES WITH POSSIBLE LABEL SUBEXPRESSION TYPES (E.G. LISTS)\
\
If the type of a guard is a general type (e.g. list) where a subexpression type is a variable type, it's safe to convert the outer type because the label applies to the inner type.  The shape of the outer type (e.g. for list, nil or cons) is not what's being protected, so it's safe to convert these.  However, the subexpressions must vary by the types they're instantiated with, and thus cannot be converted or inspected or otherwise reduced.  So, it's safe to convert nil and cons, but cons's subexpressions must be unconvertible.  Where a data constructor directly contains a type (e.g. nil), the labels must be assumed to not be there in SH/M cases because of the case where a Scheme function is imported into H/M (the expression came from the outer language), and are stripped in the H/MS cases because the typing rules do not strip them, and the outer expressions do not expect them.  To summarize: In general, it's safe to convert the data constructors, then pass the guard to the inner expressions and let their types deal with them (including the label case).\
\
==\
\
LUMPS AND BRANDS/LABELS DO THE SAME THING\
\
Restrict conversion.  Brands/labels are lumps that keep track of the original type, useful where the original target language is typed.  Lumps for Scheme-to-Haskell (i.e. untyped-to-typed), brands/labels for Haskell-to-Scheme (i.e. typed-to-untyped).  Brands/labels for Haskell-to-ML and vice versa (i.e. typed-to-typed) because the target language is typed.\
\
==\
\
CONVERSION OF TYPES BETWEEN LANGUAGES IS NECESSARY FOR IMPORTING TYPE ABSTRACTIONS\
\
Type arguments for imported type abstractions must be converted between languages because the result of the inner language's type application must be able to take as arguments converted values from the outer language.  The polymorphic function arguments must be type converted, not "lumped".  It's different than the typed-to-untyped (e.g. SH/SM) cases.\
\
If types can be equal, you can convert between them.  Simplest solution.\
\
If I had used lumps, there would have to be an outer type in the guard and some way to express equality between types with lumps and types without. Too complicated.\
\
==\
\
SUBSTITUTING CONVERTED TYPES REQUIRES SPECIAL TYPE ABSTRACTION VALUE\
\
Type conversions (as opposed to value conversions) cannot be part of the reduction rule for imported type abstractions.  Thus, the type conversion must happen in the type application reduction rule, which would require making imported type abstractions values until they are applied to types.  This also requires unifying H and M types and allow one type application to span both languages.  (You can't substitute twice because you don't know the type variable for the imported type abstraction unless you dirty the core language op sem with interop stuff.)}