[racket] Polymorphic types and curried functions

On Nov 13, 2014, at 6:36 PM, Jack Firth wrote:

> Thank you :) I think the existence of a statically typed language with such heavy support for macros means there's a lot of interesting new directions to experiment in. You could probably build half the syntactic features of Haskell on top of Typed Racket with surprisingly little effort.


If you can I am interested and so is the rest of the world! 

Do note that if Sam or Asumu add a new basic type, your macro fails. 


-- Matthias





> 
> On Thu, Nov 13, 2014 at 3:31 PM, Sam Tobin-Hochstadt <samth at cs.indiana.edu> wrote:
> 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
> >
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20141113/07788351/attachment-0001.html>