[racket] Polymorphic types and curried functions

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.

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/4b87f49a/attachment.html>