notes.txt (16496B)
1 2016-04-13: 2 Summary of the extra-info problem. 3 Problem: datatypes need to know all constructors and argument types 4 - to properly do matching 5 - but storing this info as part of the type leads to looping for recursive 6 and mutually recursive types, since the canonical form of all types is 7 full expansion 8 Current solution: 9 - for each type TY, define: 10 - standard TY macro via define-type-constructor 11 - with extra-info = name of additional macro 12 - additional "extra-info" macro that expands into needed datatype clause info 13 - this solution addresses many issues: 14 - breaks the recursion (ie inf looping) in type macros 15 - is much faster, since it avoids the type traversals I was doing to manually 16 unroll recursive types (see subst-special and subst-expr) 17 - allows for substing of quantified tyvars to occur naturally, 18 since the types are passed into the extra-info macro 19 20 What didnt work: 21 - quoting the extra-info (or parts of it) to avoid infinite expansion 22 - summary: 23 - must be exposed to expansion: 24 - struct accessors 25 - any type vars 26 - cannot be exposed to expansion: 27 - call to recursive and mutually recursive type constructors 28 - tried a complicated solution where I used "sentinel" stxs 29 to accumulate the context that the quoted parts were missing 30 - was complicated when needing to instantiate forall types 31 - and didnt fully work for nested datatypes 32 33 - manually subst out recursive calls 34 - essentially, this required me to manually manage the recursive types, 35 including, a la tapl, including unrolling in match 36 - was very performance costly (see subst-special and subst-expr) 37 - this solution does work with mutually recursive types (still inf loops) 38 39 - store extra-info as stx-property 40 - figured out how to use make-syntax-delta-introducer to sync up unexpanded 41 props, so that it may be instantiated properly 42 - but something doesnt work (specifically match) when types are provided 43 - works if everything is defined in the same file 44 - ie, inline basics-general in basics2 45 - doesnt work if (provide (struct-out ...)) is inserted directly in mlish.rkt 46 - couldnt get it to work if Cons? is assigned different contexts in match 47 - eg context of e-, or τ_e 48 - direct match on constructor is fine (see Bool use in bg/basics2.mlish) 49 - but doesnt work when passed through fn call (see bool-id in basics2) 50 - essentially, struct accessors and predicates must be exposed to expansion 51 error is: 52 ; require: namespace mismatch; 53 ; reference to a module that is not available 54 ; reference phase: 0 55 ; referenced module: 'basics-general 56 ; referenced phase level: 0 57 ; in: True26? 58 59 2016-02-29 60 Problem: storing variant info as properties 61 - when instantiating polymorphic type, need to instantiate properties as well 62 Alternate Solution: store variant syntactically in (expanded) type 63 - benefit is instantiation "just works" 64 - drawbacks: 65 - recursive types will expand infinitely 66 - quoting the variant stops infinite expansion but breaks the subst 67 - ie ids in the quote no longer correspond to the bound id 68 - can manually stop expansion but then types will no longer always be 69 fully expanded forms 70 - tried this a few times previously - can get VERY messy - avoid if possible 71 - to make this alternate work, can manually fold/unfold recursive types 72 - cant use \mu from stlc+rec-iso bc each type is more than the mu 73 so folding/unfolding is a little different 74 75 2016-02-19 76 Implementing algebraic data types 77 - macro cannot define type-alias and constructor functions that produce 78 variant values 79 - not only because adts should be an abstraction (ie not type alias) 80 - constructor output will have variant type and not the type defined 81 - macro should basically expand to list implementation in stlc+cons.rkt 82 - where to store the names of the variants (as stx prop?) 83 84 85 2015-10-09 86 TODO: variant case should call current-join? 87 88 2015-10-09 89 Can I get rid of current-type-eval? 90 - would have to put "normalize" call in type=? 91 - and call normalize in current-promote (before pattern matching) 92 93 Thus, it's probably better to keep type-eval 94 95 2015-08-16: 96 TODO: 97 - generalize binding forms 98 - add tags to distinguish different binding forms 99 100 2015-08-16: 101 Paper outline 102 103 stlc.rkt 104 Concepts: 105 - #%app 106 - lambda 107 - user input types must be checked 108 109 stlc+rec-iso.rkt 110 Concept(s): binding form, type=? for binding forms 111 112 2015-08-13 113 Requirements for define-type-constructor syntax: 114 - identifier types, like Int 115 - basic tuples, like arrow 116 - arity 117 - nested tuples, like records 118 - binding forms, like forall 119 120 Problem: 121 Types must be expanded, to check that they are valid, catch unbound ids, etc. 122 But should I attach the expanded type to a term, or the original surface stx? 123 - maybe this is just repeating the same thing I wrote below? 124 - Related question: fully expand types before calling type=? or typecheck? 125 Answer: must only compare fully expanded forms, otherwise these will not work 126 - define-type-alias 127 Rules: 128 - all user-written types must be expanded and checked 129 - check for invalid types, unbound ids 130 - use expanded types (when available) to create new types 131 - expand all types before attaching 132 - assume types are expanded in type=? and typechecks 133 134 2015-07-31 135 Problem: pattern-expander not being recognized 136 Solution: syntax-parse pattern directives must begin with ~ prefix 137 138 2015-07-30: 139 Problem: How to match against an "expanded" type when I have an unexpanded pat? 140 - use the 'orig syntax? 141 - this would probably work but now 'orig is used for more than debugging/msgs 142 - so dont do this 143 - also, wont work because you're only matching part of the type 144 - use pattern expanders! 145 - a declared literal in define-type-constructor is defined as *both*: 146 - and macro that applies a temporary id (defined as void) 147 - a pattern-expander that expands into the expanded form: 148 ((~literal #%plain-app) (~literal tmp-id) . args) 149 150 Note to self: when getting weird macro pattern matching errors, always check if you're accidentally using a pattern variable! 151 152 2015-07-28 153 Problem: How to handle mixed types, ie combining expanded and unexpanded types. 154 Problem: When to eval, ie expand, types into canonical form 155 Solution: 156 - use two tags, #%type and #%plain-type, representing surface type syntax and 157 fully expanded type representation, respectively 158 - #%type wrapper automatically added by the define-type- macros 159 - #%plain-type wrapper added by type-eval 160 - both are macros that expand into their (single) sub-form 161 - enables elegant mixing of expanded and unexpanded types 162 - mixed types still need to be eval'ed 163 - needed to construct other types, eg inferring type of lambda 164 - enables easy checking of is-type? 165 - only checks outer wrapper 166 - rely on each tycon to validate its own arguments 167 - eval-type only expands if not #%plain-type, ie not already expanded 168 - this solution thus far does not require any awkward "hacks" in implementations 169 170 2015-07-25 171 Problem: types and terms occur in the same space 172 What to do about "valid" terms like \x:(void).x or \x:1.x ? 173 - adding an is-type? predicate that checks shape and other things will only 174 partially work because things like \x:(void).x will still pass 175 - define types in a different phase 176 - wont work because you need terms to do type checking so the terms have to be 177 in the same phase 178 - write a separate parser for types 179 - wont work because still cant tell with a valid binding is a term or type, 180 eg, \x:(void).x still passes 181 - unless you hard-code the type names, but then it's not extensible? 182 - can extend the reader but then you have code duplication? 183 - wrap types with a tag, like #%type ? 184 - this might work 185 - will this have extensibility problems later, ie with records and variants? 186 187 2015-07-24 188 When to canonicalize (ie, eval) types: 189 - calling eval before matching is too late 190 - wont catch things like unbound types 191 - syntax-class evaling is too eager 192 - sometimes get error when you shouldnt or wrong erro 193 - eg type (-> 1 2) 194 - I think the right place is to have \vdash eval 195 - and rackunit testing forms 196 197 2015-06-30 198 when extending a typed language, use prefix-in for identifiers: 199 - that are extended, eg #%datum in ext-stlc.rkt 200 - rename-out the extended implementation of the form 201 - or when you want to use racket's version, eg #%app in ext-stlc.rkt 202 - rename-out the prefixed form 203 - must except-out the prefixed forms, eg stlc:#%app and stlc:#%datum in ext-stlc 204 205 2015-06-26 206 Random thought: Can kinds be "erased"? 207 - first thought is no, since they appear to be needed for type equality? 208 - Solution: add them to body of lambda (eg which represents a forall) 209 210 2015-06-26 211 syntax marks problem: 212 - in the type created by \Lambda, eg \x.(-> x x), the binding x and body x's 213 were free-id= but not bound-id= because the body x's had extra marks 214 - this is because (the syntax representing) types are marked going "into" an 215 expansion, but do not receive the cancelling mark coming *out of* the 216 expansion since they are attached as a syntax-property 217 - thus, when this lam goes through another expansion (via \vdash), the binding x 218 and body x's become neither free-id nor bound-id=? 219 Solution: 220 - undo the mark (using syntax-local-introduce) when retrieving the a type 221 as a syntax property (ie in \vdash) 222 - need one more syntax-local-introduce in infer/tvs+erase 223 - i guess the rule is I need as many syntax-local-introduce's as extra 224 expanding lambdas that I add 225 226 227 2015-06-18 228 Design Decision: 229 Types must be fully expanded, if we wish to use expansion to typecheck types 230 (i.e., kinding). 231 Problems: 232 - Type constructors can't be both macro and function 233 - solution: macro that expands to tmp function 234 - must provide predicate to check 235 - Recursive types 236 - solution: ??? 237 - Displaying error msgs 238 - need to keep track of surface stx (similar to 'origin prop?) 239 - solution: ??? 240 - repeated expansion of already expanded types 241 - solution: ??? 242 - what to do about tuples, where there may be a string in the fn position 243 - solution: add an extra "type constructor" in front of each pair 244 - todo: come up with a nicer way to handle "compound" types 245 - what is the expansion of forall? 246 247 2015-06-16 248 Problem: 249 use expansion for typechecking of terms: ok 250 - specifically, ok to go under lambda, since eval happens later 251 use expansion for typechecking of types: doesnt work now 252 - doesnt work because types currently are not fully-expandable 253 - eg a type constructor application (tycon x) is a macro that expands to 254 (#%app tycon x), where this expression will error if expanded further 255 since tycon cannot be used as an identifier 256 - if I define tycon as a regular function, so (tycon x) expands to 257 (#%app tycon x), then it wont catch non-app uses of tycon 258 - should be fine? - this is a parsing, not typechecking problem 259 - but then then parser need to be updated with every new type constructor 260 - this kind of monolithic architecture is what the paper is trying 261 to avoid 262 - alternative: define tycon as a macro where (tycon x) expands to 263 (#%app tycon_new x) 264 - drawback: can't use ~literal to match/destructure the tycon 265 - does this make things like type checking or type=? more difficult? 266 - will have to go through a separately-defined interface, 267 like a \tau? predicate 268 Subproblem: must completely change the representation of types? 269 - must use fully-expanded forms instead of surface syntax 270 - in particular, will be using *fully expanded identifiers* 271 - in this scenario, can I still match with ~literal? 272 Subproblem: where/when to expand 273 - types now must all be expanded since that is when kind checking occurs 274 use expansion for eval of types: not ok 275 - dont want to go under binders 276 - expand then eval? 277 - but then type constructors cant be macros? 278 Possible Solution 279 - I think eval must be separate 280 Subproblem: Do I need a new eval that is different from current-eval? 281 - conflict: 282 - current-eval must go under forall to check for unbound ids 283 - but eval should not go under forall for the case of tyapps 284 - maybe tyapp should go into type=?, as in tapl? 285 Subproblem: where to eval 286 - currently call eval for user type annotations, and in \vdash 287 Subproblem: Can type=? assume fully expanded (ie, evaled) types? 288 289 2015-06-15 290 New Thesis: The abstractions provided by macro systems are effective at 291 implementing type systems 292 293 2015-06-08 294 Problem: how to represent \rightarrow kind operator 295 1) If the kind operator is the same as the function type operator then how do I 296 attach a kind to a function arrow, since the arrow is still undefined at the 297 time. 298 2) If the kind arrow is a different arrow then #%app must be parameterized over 299 the arrow 300 301 2015-05-28 302 Problem: how to represent \forall types 303 1) (Racket) functions 304 - this gets the most linguistic reuse (is this true?) 305 - but this does not allow equality comparisons 306 - unless perhaps compare two foralls for equality by applying to the same tvar 307 - but these type vars would be unbound so it still wouldnt work without 308 adding a new special case 309 2) syntax 310 - easier to compare 311 - but still need to manually implement alpha equality 312 - would still require a special case for comparing the bodies, which have 313 unbound typevars 314 315 Problem: begin in lambda body gets spliced 316 - results in combined syntax properties, eg types 317 Solution: 318 - wrap lambda body with #%expression to indicate expression, ie non-splicing, 319 begin 320 321 2015-05-29 322 Notes: locally-nameless representation of lambdas (and other binding terms) 323 - syntactically distinguishes bound names vs free vars 324 - combination of debruijn (nameless) for bound vars and names 325 - simplifies implementation of capture avoiding substitution 326 - I already get around by using Racket's identifiers and free-identifier= 327 to easily implement capture-avoiding subst 328 - debruijn indices for boundvars avoids having to convert to canonical form 329 to compare for alpha-equal 330 - using names for free vars avoids "shifting" of indices when adding or 331 removing binders, ie free vars dont rely on context 332 - two main operations: 333 - open: converts some bound vars to free vars 334 - eg subst into lambda body 335 - conversion and subst can be done in one pass? 336 - close: converts some free vars to bound vars 337 - eg wrapping a term in a lambda 338 - similar to subst 339 - both operations involve traversing the term 340 - but can do straight-subst (instead of renaming subst) because 341 shadowing is not possible 342 - multiple binders are more complicated 343 - require both depth and offset index 344 345 Previous: ----------------- 346 347 macro system requirements: 348 - depth-first expansion, i.e., localexpand, and stop-lists 349 - language form hooks, e.g., #%app, etc 350 - literal types, e.g. integer syntax class, ie compile time literal type tag 351 - identifiers and free-identifier=? 352 - syntax-parse or other pattern matching 353 354 Type constructors must be prefix (and not infix) and must be functions 355 - because in order to support type aliases: 356 - types must be expanded, 357 - and having a macro identifier (ie, an alias) in the function position 358 makes the expander error (constructor is ok bc it is run time identifier) 359 360 Type expansion problem: what to do about #%app? 361 1) use the #%app in scope: 362 - may do type checking and error bc types dont have types 363 2) use the racket #%app: 364 - may work but how to do this without ruining context of other 365 identifiers (ie types) 366 Solution: do #1, but 367 1) stop at the #%app 368 2) manually drop it and continue expanding rest 369 370 Types must be identifiers, but not macros 371 - cannot be macros if we want to use expansion for type aliases 372 - because then what does a base type like Int expand to? 373 - if we define Int as a runtime identifier, then expansion will stop at Int 374 375 376 debugging notes ------------- 377 - "datum" error: 378 379 ?: literal data is not allowed; 380 no #%datum syntax transformer is bound in: #f 381 382 - happens when you try to syntax->datum or local-expand a #f value 383 - likely indicates use of wrong version of some overloaded form 384 - eg, using stlc:lambda instead of racket's lambda 385 - could also be trying to ty-eval a (#f) expected-type 386 387 - vague "bad syntax" error 388 - means a syntax-parse #:when or #:with matching failed 389 - ideally would have better err msg at that spot 390 391 - #%datum: keyword used as an expression in: #:with 392 - missing a #:when in front of a printf 393 394 - one of type=? arguments is false 395 - term missing a type 396 - type missing a kind 397 - need to transfer syntax properties, eg subst