[racket] Polymorphic types and curried functions

That's really cool.

Sam

On Thu, Nov 13, 2014 at 6:28 PM, Jack Firth <jackhfirth at gmail.com> 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 <matthias at ccs.neu.edu>
> 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
>