let-aliasing + removing let imps #2

pnwamk · 2014-12-14T16:03:34Z

First draft of proposal to remove implications from the let typing judgment (replaced by a logically equivalent or) and add aliasing for let-bindings where the expression being bound has an object (e.g. x, (car y), etc...).

This speeds up type checking (e.g. the 'filters-more' function from http://bugs.racket-lang.org/query/?cmd=view&pr=14838) and adds the ability to typecheck expressions that utilize simple let bindings of pure expressions, such as the following function:

lang typed/racket

(: foo (Any -> Number))
(define (foo x)
(match x
[(? number?) x]))

The current implementation has 2 errors when running the unit tests at the moment, which relate to usages of types with '...' such as:

(let: ((f : (All (b ...) (Any ... b -> Any)) (lambda x (quote x)))) (lambda xs (apply f (quote y) xs)))

Obviously I need to work out these errors before this is pulled, but this is what it looks like at the moment, FYI.

samth · 2014-12-14T22:24:51Z

typed-racket-lib/typed-racket/env/lexical-env.rkt

 (provide/cond-contract
- [lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))])
+ [lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
+ [lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))]


What does this do on failure?

It acts like an identity function, returning -id-path applied to the input

samth · 2014-12-14T22:34:11Z

Things still to do here:

new tests
fix the remaining bugs
maybe doc changes?
write a blog post

pnwamk · 2014-12-16T15:07:52Z

Now supports aliasing for identifiers and arbitrary car/cdr paths. All tests are passing. On my machine it also looks like this sped up the time it took to run all the internal TR tests ('racket run.rkt --all' in the test suite), but if someone else could sanity check me on that I'd be much obliged -- maybe I'm just imagining it =) [Note: timing looks consistent/unchange from before this PR so, nevermind =) ]

samth · 2014-12-16T18:05:33Z

typed-racket-lib/typed-racket/env/type-env-structs.rkt

+               [(Empty:)
+                (values (free-id-table-set tys id t) als)]
+               ;; id is aliased to an identifier, record the alias and type of that alias id
+               [(Path: '() id^)


What does the ^ suffix indicate?

In that case I need to talk about the original identifier (id) and the id it is aliased to (id^), so the ^ only serves to give me a different name.

That case is when the id we're looking at is being aliased and that alias is an id we possibly have not recorded the type of before. Without that second part (recording the type for the alias as well) we fail some typechecking that currently works. I didn't think it was necc. originally but it turned out to be, so I added it.

Ah, ok. The usual convention is to use * as the suffix like "x prime" in math. In Racket, the ^ suffix is most commonly used for unit signatures.

pnwamk · 2014-12-18T18:30:43Z

arbitrary aliasing now supported. all tests passing.

I haven't implemented restrict's ability to do structural updates when updating one struct with another yet... however the current implementation with these changes can typecheck all the tests and things such as:

#lang typed/racket

(struct (α β) foo ([x : α] [next : foo]))

(define (bar [f : (foo Number Number)]) : (foo Integer Integer)
  (let* ([f* (foo-next f)]
         [fx* (foo-x f*)])
    (if (exact-integer? fx*)
        f*
        (error "oops"))))

(define (baz [f : (foo Number Number)]) : (foo Integer Integer)
  (let* ([f* (foo-next f)]
         [fx* (and f* (foo-x f*))])
    (if (exact-integer? (foo-x (foo-next f)))
        f*
        (error "oops"))))

Off the top of my head I'm not sure what additional programs would typecheck that do not with the current restrict implementation... I had thought the above might not typecheck with these changes - but they do.

samth · 2014-12-18T19:44:39Z

Wooo!

Why does foo have two type parameters, and why is it uninstantiated as the annotation on next? Any why is fx* dead in the second program?

samth · 2014-12-18T19:46:52Z

typed-racket-lib/typed-racket/env/lexical-env.rkt

+
+    ;; promise op
+    [((Promise: t) (list rst ... (ForcePE:)))
+     (path-type rst t)]


Need resolved as a 3rd argument here and in the cases above, I think

-- On fx* - no real reason, I was just tweaking around with it and didn't clean up the second version and was a little sloppy. Sorry.

-- On 'resolved as a 3rd argument', resolved here tracks what has been resolved at a given path. When we progress on the path (i.e. recur on a structural subpath of the current path) then we're free to resolve all we want again -- we just care about duplicate resolving when we're sitting at the same path location making no real progress. That was my reasoning anyway.

Ah, ok. Put the explanation of how it works in a comment, though.

In general, anything you need to explain in the discussion belongs in a
comment.

stamourv · 2014-12-18T21:50:54Z

LGTM.
Would definitely be an improvement. Implementation looks fine to me, modulo my minor comments.

takikawa · 2014-12-18T22:05:52Z

typed-racket-lib/typed-racket/env/lexical-env.rkt

@@ -53,9 +63,10 @@
                                          [(syntax-procedure-converted-arguments-property i)
                                           => (λ (prop)
                                                (define orig (car (flatten prop)))
+                                                (define alias (lookup-alias env orig (λ (_) #f)))


This definition doesn't appear to be referenced in this lambda expression. Is this called purely for effect?

pnwamk · 2014-12-20T03:47:50Z

I think I made all/most of the changes mentioned.

On the issue of having different functions that extend the environment - I agree it was a little confusing (it was not clear why exactly there was more than one by just the names), so I renamed them to be very explicit about their purposes to try and clear it up some. They each do different enough things and are required in different areas... so I don't think it makes sense to merge them all into one function (e.g. aliasing doesn't make sense in the other areas the environment is being extended, etc...).

samth · 2014-12-21T00:27:34Z

typed-racket-doc/typed-racket/scribblings/guide/occurrence.scrbl

+
+Typed Racket is able to reason about some cases when variables introduced 
+by let-expressions alias other values (e.g. when they alias non-mutated identifiers, 
+car/cdr/struct accesses into immutable values, etc...). This allows programs 


Use links for car: @racket[car] etc.

samth · 2014-12-21T00:36:23Z

The remaining comments are just small nits. You now have push access to this repository, so push when you're done (but please rebase first).

pnwamk · 2014-12-21T21:22:22Z

Roger - I'll make changes and push after rebasing later tonight... or tomorrow morning.

Here's a blog post that describes the motivation and approach of adding let-aliasing to TR: http://andmkent.github.io/blog/2014/12/20/let-aliasing-in-typed-racket/

samth · 2014-12-21T21:36:30Z

Oh, awesome, I didn't know you had a blog. :)

pnwamk · 2014-12-21T21:42:14Z

You haven't been missing out on much so far =)

It's on my to do list.
On Dec 21, 2014 4:36 PM, "Sam Tobin-Hochstadt" notifications@github.com
wrote:

Oh, awesome, I didn't know you had a blog. :)

—
Reply to this email directly or view it on GitHub
#2 (comment).

let-aliasing + removing let imps

samth reviewed Dec 14, 2014
View reviewed changes

pnwamk mentioned this pull request Dec 16, 2014

TR performance tweaks (implied-atomic? and let) racket/racket#830

Closed

samth reviewed Dec 16, 2014
View reviewed changes

samth reviewed Dec 18, 2014
View reviewed changes

takikawa reviewed Dec 18, 2014
View reviewed changes

samth reviewed Dec 21, 2014
View reviewed changes

Andrew Kent added 3 commits December 22, 2014 12:34

printer fix for paths

683ebb1

restrict structural recursion

53d1d8a

initial let-aliasing addition

e1b8eff

pnwamk pushed a commit that referenced this pull request Dec 22, 2014

Merge pull request #2 from andmkent/master

ca88457

let-aliasing + removing let imps

pnwamk merged commit ca88457 into racket:master Dec 22, 2014

samth mentioned this pull request Mar 11, 2015

Add aliases to lexical environment racket/racket#706

Closed

samth pushed a commit that referenced this pull request Nov 7, 2019

Correct type of file/md5 (#2)

7588f23

Uh oh!

let-aliasing + removing let imps #2

let-aliasing + removing let imps #2

Uh oh!

Conversation

pnwamk commented Dec 14, 2014

lang typed/racket

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

samth commented Dec 14, 2014

Uh oh!

pnwamk commented Dec 16, 2014

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pnwamk commented Dec 18, 2014

Uh oh!

samth commented Dec 18, 2014

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

stamourv commented Dec 18, 2014

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pnwamk commented Dec 20, 2014

Uh oh!

Choose a reason for hiding this comment

Uh oh!

samth commented Dec 21, 2014

Uh oh!

pnwamk commented Dec 21, 2014

Uh oh!

samth commented Dec 21, 2014

Uh oh!

pnwamk commented Dec 21, 2014

Uh oh!

Uh oh!