[racket] Polymorphic types and curried functions

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20141113/71039fc5/attachment.html>