That's really cool. Sam
On Thu, Nov 13, 2014 at 6:28 PM, Jack Firth <[email protected]> wrote: > That was my general approach, however I had to do a bit more analysis. That > macro expands (:/c f (A B) (-> B (-> A B)) to (: f (All (A) (-> B (All (B) > (-> A B))))). I’ve come up with something that checks the argument types in > a basic function contract and only provides the polymorphic variables that > are used, then wraps the returned function type with any unused type > variables. It's combined with some useful syntax for complex function types. > The source is available at https://github.com/jackfirth/compact-annotations > and it’s available as a package in the catalog. Let’s you write polymorphic > types much more neatly: > > (:: map-list-to-vector A B => (Listof A) -> (A -> B) -> (Vectorof B)) > (define ((map-list-to-vector lst) f) > (list->vector (map f lst))) > > If anyone’s interested in this, or if there’s any other shortcuts for type > annotations people are interested in, I’d love some feedback. > > > On Wed, Nov 12, 2014 at 7:20 PM, Matthias Felleisen <[email protected]> > wrote: >> >> >> Sorry that was a superfluous (premature) require: >> >> #lang typed/racket >> >> ;; syntax >> ;; (:/c f (α β γ) (-> A B (-> C (-> D E)))) >> ;; ==> >> ;; (: f (All (α) (-> A B (All (β) (-> C (All (γ) (-> D E))))))) >> (define-syntax (:/c stx) >> (syntax-case stx (All/c) >> [(_ f (A ...) τ) (let ([σ (All/c #'(A ...) #'τ)]) #`(: f #,σ))])) >> >> ;; [List-of Syntax/id] Syntax -> Syntax >> ;; distributes type variables along the right-most spine of a curried -> >> type >> ;; given: >> ;; (α β γ) (-> A B (-> C (-> D E))) >> ;; wanted: >> ;; (All (α) (-> A B (All (β) (-> C (All (γ) (-> D E)))))) >> (define-for-syntax (All/c α* C) >> (syntax-case α* () >> [() C] >> [(α) #`(All (α) #,C)] >> [(α β ...) >> (syntax-case C () >> [(-> A ... B) #`(All (α) (-> A ... #,(All/c #'(β ...) #'B)))] >> [(_ (α ...) A) #'(All (α ...) A)])])) >> >> ;; >> ----------------------------------------------------------------------------- >> >> (:/c compare-projection (A B) (-> (-> A A Boolean) (-> (-> B A) (-> B B >> Boolean)))) >> (define (((compare-projection a<) b->a) b1 b2) >> (a< (b->a b1) (b->a b2))) >> >> (define symbol<? >> ((compare-projection bytes<?) (compose string->bytes/utf-8 >> symbol->string))) >> >> (symbol<? 'a 'b) >> >> >> >> On Nov 12, 2014, at 9:58 PM, Matthias Felleisen wrote: >> >> > >> > You cannot write macros that expand within types (yet). >> > >> > But you can write macros for : like this: >> > >> > #lang typed/racket >> > >> > (require (for-template (only-in typed/racket All ->))) >> > >> > ;; syntax >> > ;; (:/c f (α β γ) (-> A B (-> C (-> D E)))) >> > ;; ==> >> > ;; (: f (All (α) (-> A B (All (β) (-> C (All (γ) (-> D E))))))) >> > (define-syntax (:/c stx) >> > (syntax-case stx (All/c) >> > [(_ f (A ...) τ) (let ([σ (All/c #'(A ...) #'τ)]) #`(: f #,σ))])) >> > >> > ;; [List-of Syntax/id] Syntax -> Syntax >> > ;; distributes type variables along the right-most spine of a curried -> >> > type >> > ;; given: >> > ;; (α β γ) (-> A B (-> C (-> D E))) >> > ;; wanted: >> > ;; (All (α) (-> A B (All (β) (-> C (All (γ) (-> D E)))))) >> > (define-for-syntax (All/c α* C) >> > (syntax-case α* () >> > [() C] >> > [(α) #`(All (α) #,C)] >> > [(α β ...) >> > (syntax-case C () >> > [(-> A ... B) >> > (let ([rst (All/c #'(β ...) #'B)]) >> > #`(All (α) (-> A ... #,rst)))] >> > [(_ (α ...) A) #'(All (α ...) A)])])) >> > >> > ;; >> > ----------------------------------------------------------------------------- >> > >> > (:/c compare-projection (A B) (-> (-> A A Boolean) (-> (-> B A) (-> B B >> > Boolean)))) >> > (define (((compare-projection a<) b->a) b1 b2) >> > (a< (b->a b1) (b->a b2))) >> > >> > (define symbol<? >> > ((compare-projection bytes<?) (compose string->bytes/utf-8 >> > symbol->string))) >> > >> > (symbol<? 'a 'b) >> > >> > >> > >> > On Nov 12, 2014, at 8:56 PM, Jack Firth wrote: >> > >> >> I've been mucking around with Typed Racket some and was writing a >> >> polymorphic curried function when something I found counter-intuitive >> >> popped >> >> up. I had this function: >> >> >> >> (: compare-projection (All (A B) (-> (-> A A Boolean) (-> (-> B A) >> >> (-> B B Boolean))))) >> >> (define (((compare-projection a<) b->a) b1 b2) >> >> (a< (b->a b1) (b->a b2))) >> >> >> >> The purpose of this function was to let me compare things by converting >> >> them to some other type with a known comparison function, so something >> >> like >> >> symbol<? (which is defined in terms of bytes<? according to the docs) >> >> could >> >> be implemented directly like this: >> >> >> >> (define symbol<? ((compare-projection bytes<?) (compose >> >> string->bytes/utf-8 symbol->string))) >> >> >> >> The problem I was having was that the first initial argument, bytes<?, >> >> only specifies the first type variable A. The other type variable B can >> >> still be anything, as it depends on what function you use to map things to >> >> type A in the returned function. The All type therefore assumes Any type >> >> for >> >> B, making the returned type non-polymorphic. >> >> >> >> I expected something like currying to occur in the polymorphic type, >> >> since the returned type is a function. I thought that if a polymorphic >> >> function 1) returns a function and 2) doesn't have enough information from >> >> it's arguments to determine all it's type variables, that it should then >> >> automatically return a polymorphic function. In other words, I thought >> >> this >> >> type would be equivalent to this automatically: >> >> >> >> (All (A) (-> (-> A A Boolean) (All (B) (-> (-> B A) (-> B B >> >> Boolean))))) >> >> >> >> This is most certainly not the case, though I wonder - would it be >> >> terribly difficult to define some sort of polymorphic type constructor >> >> that >> >> *did* behave like this? I'm fiddling with some macros for syntactic sugar >> >> of >> >> type definitions and it would be a boon to not have to worry about this. >> >> ____________________ >> >> Racket Users list: >> >> http://lists.racket-lang.org/users >> > >> > >> > ____________________ >> > Racket Users list: >> > http://lists.racket-lang.org/users >> > > > ____________________ > Racket Users list: > http://lists.racket-lang.org/users > ____________________ Racket Users list: http://lists.racket-lang.org/users
