Discussion:
[racket] Is this function typeable in Typed Racket?
Alexis King
2015-03-04 08:18:07 UTC
Permalink
Disclaimer: this question is both a real question and me trying to push the type system to its limits, so I’m not really expecting to get a satisfactory answer.

I posted a question on Stack Overflow here <http://stackoverflow.com/q/28849475/465378>, but I’m guessing that this is unfortunately far too localized to be answered there, so I’m posting it here as well. The original question is as follows:

I can write a simple function in untyped Racket called curry-all that takes a list of functions, all of which accept the same kind of value for their first argument, and produces a list of functions with their first arguments curried.

(define (curry-all fs arg)
(map (λ (f) (curry f arg)) fs))
For a running example of the above function, see this snippet on pasterack <http://pasterack.org/pastes/88150>.

This is a valid function, but I'm not sure if it's even possible to type in Typed Racket given its polymorphic typing constructs. The type of curry itself is already fairly complex, and obviously the type of curry-all would need to be necessarily more complex.

I made a relatively simple attempt at typing this function, though I was quite aware that it would not function as I liked:

(: curry-all
(All [a c b ...]
(Listof (-> a b ... b c)) a
-> (Listof (-> b ... b c))))
(define (curry-all fs arg)
(map (λ ([f : (-> a b ... b c)])
(curry f arg))
fs))
Obviously, this works if all the functions have identical types (which isn’t worthless!), but it fails if they have different arities, even if their first arguments’ types are shared.

Is there any way to specify this function’s type so that it will work in a more general case?
Alexander D. Knauth
2015-03-04 13:02:42 UTC
Permalink
I wonder if something like this could bring it closer to being possible?:
https://github.com/plt/racket/pull/564
Post by Alexis King
Disclaimer: this question is both a real question and me trying to push the type system to its limits, so I’m not really expecting to get a satisfactory answer.
I can write a simple function in untyped Racket called curry-all that takes a list of functions, all of which accept the same kind of value for their first argument, and produces a list of functions with their first arguments curried.
(define (curry-all fs arg)
(map (λ (f) (curry f arg)) fs))
For a running example of the above function, see this snippet on pasterack.
This is a valid function, but I'm not sure if it's even possible to type in Typed Racket given its polymorphic typing constructs. The type of curry itself is already fairly complex, and obviously the type of curry-all would need to be necessarily more complex.
(: curry-all
(All [a c b ...]
(Listof (-> a b ... b c)) a
-> (Listof (-> b ... b c))))
(define (curry-all fs arg)
(map (λ ([f : (-> a b ... b c)])
(curry f arg))
fs))
Obviously, this works if all the functions have identical types (which isn’t worthless!), but it fails if they have different arities, even if their first arguments’ types are shared.
Is there any way to specify this function’s type so that it will work in a more general case?
____________________
http://lists.racket-lang.org/users
Loading...