Passing procedures of unknow arity across typed/untyped boundary

Questions & Answers
1

Hello,

I need to pass a function of unknown arity to another function in Typed Racket, in particular because the approach using polymorphic functions from this thread does not completely fit my use case, and also because I don't know how to write this type (-> Boolean ... Boolean) correctly.

I tried writing untyped code and adding a type a posteriori:

#lang typed/racket

(module untyped racket
  (provide do)
  (define (do f x) (f x)))

(require/typed 'untyped
  [do (-> Procedure Any Any)]
  )

(do (λ (x) x) 2)

This gives the following error:

; g5: arity mismatch;
;  the expected number of arguments does not match the given number
;   given: 1

Indeed, the documentation for Procedure says:

Because this type encodes only the fact that the value is a procedure, and not its argument types or even arity, the type-checker cannot allow values of this type to be applied.

I hoped that this constraint would not propagate over to untyped code, but obviously I was wrong. Also, this means that Procedure cannot be used as a direct replacement for procedure?.

If I replace the type of do by (-> Any Any Any), I get the following error:

; Attempted to use a higher-order value passed as `Any` in untyped code

I also tried (All (b a ...) (-> (-> a ... b) Any Any)) as the type for do, but this of course gives me:

Type Checker: Type (All (b a ...) (-> (-> a ... a b) Any Any)) could not be converted to a contract: cannot generate contract for variable arity polymorphic type

Finally, the type (-> (-> Any Any) Any Any) works obviously, but I need to pass a function of unknown arity as the first parameter.

Is there a way to pass a function of unknown arity across the typed/untyped boundary?

Alternatively, for my use case, is there a way to write the type (-> Boolean ... Boolean)?

2

You say a function of unknown arity, but your example (define (do f x) (f x)) requires f to have an arity that includes 1? So I’m not
sure if by « unknown » you mean « variable » as in « has multiple
arities » or truly « unknown » as in « the number of possible
arguments is unknown ». For the latter case I would have a look at the
procedure-arity (?) functions.

1 Like
3

You are right @benknoble , the meaning of "unknown arity" is ambiguous in my original post. What I want is a function—e.g. do—which takes as an argument another function—e.g. f—whose arity do does not know in advance.

To give some context, I have a collection of functions for tabulating other functions, i.e. producing a list of the values these functions take on a given set of inputs. My final goal is constructing truth tables.

Writing this in untyped Racket is really easy: just loop over the functions and over the possible inputs and apply the functions to the inputs. Things become more difficult in Typed Racket, as apply is treated specially and so I cannot reuse its type.

Right now I am looking for ways to write weaker types which would still allow me to type tabulating functions.

My fallback solution now is using types like (-> Boolean * Boolean) and supplying the arity of the tabulated function as an argument, but I'd be glad to have something more elegant.

4

I think the first thing to think about is "why is it impossible for your function to encounter an arity error". If it doesn't rule this out, then the question is "what constraints on the input are needed to make sure that there are no arity errors". Unfortunately, Typed Racket doesn't let you talk about the number of arguments to a procedure, so some constraints aren't allowed, but answering those questions is the first step.

1 Like
5

You may have a good reason for wanting to use typed racket, but from what you have written I can't really guess what your reason is.

Overall I would keep it in normal racket, unless there are big performance improvements, but I also might be biased, because I have barely used typed racket directly (writing it myself), mostly because all those messages about "how do I type x" and "that isn't supported or has to be done differently" on the mailing list, have given me the impression that it would cost me a big chunk of my productivity, compared to defensive programming with contracts.

Mostly wanted to give a nudge in the direction: "Are you sure you are using the right tool for the job?"
Why? Because it seems your code is quite runtime-dynamic so why not use dynamic-runtime-checks (contracts), which may fit the problem better.

That said you may have valid reasons, that I am not aware of, so take this with a grain of salt...

1 Like
6

Thank you @samth for your suggestions.

That's because my function is essentially a loop calling apply, which cannot encounter an arity error (if the list is of the right size).

That would be something similar to apply: all functions in the list of functions (argument 1) should be of the same arity, and there should be enough elements in the list of inputs (argument 2). I suspect something like that may be expressible with dependent types, but from some brief former exposure I find that dependent types are generally an overkill for my use cases. I am not doing proof assistants after all :slight_smile:

The good news is that your questions made me realize clearly that my function is essentially a wrapper around apply, and so I can just replace it with a macro and therefore avoid needing to replicate the type of apply. If it works, it should be good enough for my use case.

7

Thank you @simonls for your question about Typed Racket being the right tool! I have indeed thought very lengthy thoughts about it, and I settled on one major reason which convinces me for now. As a former Haskeller, I love expressing myself with types. Writing a function without a type signature feels like writing half of it to me :slight_smile: When I took up Racket in 2020, I immediately jumped on to use contracts because they seemed more widespread and more mature, but I quickly realized that I was abusing them to try and replace types. Over time, I think I learned how to use contracts more properly, but this usage is still unsatisfying to me personally.

The strategy I have currently is to use Typed Racket as much as I can, and then throw in some untyped code to which I give a type signature a posteriori. This allows to learn more of Typed Racket and will hopefully help me contribute to it one day. (I keep asking questions about contributing, people answer, but I have never had the time to actually do anything :innocent: )

You are completely right, I am abusing Typed Racket a little with my attempts. I am totally aware that I wouldn't even think about typing anything of variable arity in Haskell for example. However, such abuse attempts help me learn more, and I'm quite happy with that :innocent:

Your answer makes me realize clearer that I lost my old Haskell style and started gaining some more Racket programming style, but I am still figuring my way around. I am very happy to receive helpful guidance from the community for my adventures :slight_smile:

1 Like
8

Experimenting, stretching the limits of what seems possible, is definitely a good thing. My answer was mostly meant as one additional perspective, have fun with what you are doing and let us know if you find interesting ways of using the language! :smiley:

So far I haven't gone down the rabbit hole of "complex"/powerful type systems very far, maybe I will do that eventually... :thinking:

1 Like
9

You might find this program useful or instructive:

#lang typed/racket

(: apply-list (All (A B ...)
                   (-> (-> B ... A) (Listof (List B ... B)) (Listof A))))
(define (apply-list f ls)
  (map (lambda ([l : (List B ...)]) (apply f l)) ls))


(apply-list (λ ([x : Integer] [y : Integer]) (+ x 1))
            (list (list 1 4) (list 2 3)))
1 Like
10

Thank you very much @samth. I did indeed write a type very similar to this one for my tabulating function. Then I wanted to specialize apply-list to Boolean functions and generate the domains—ls in your code—automatically, based on the arity of the f. Since I can't write (-> Boolean ... Boolean), the type of the specialized tabulating function must stay something like

(All (B ...) (-> (-> B ... B Boolean) (Listof Boolean)))

Then, when I wrote my code, I had trouble converting (Listof Boolean) generated by make-list to (List B ... B), but when I tried reproducing this with your function, I ran into something else:

(: apply-list-auto (All (B ...) (-> (-> B ... B Boolean) (Listof Boolean))))
(define (apply-list-auto f)
  (define arity (cast (procedure-arity f) Integer))
  (define ls (make-list arity #f))
  (apply-list f (list ls ls)))

; Internal Typechecker Error: Got non-dcons: #(struct:dcon-dotted () #(struct:c Nothing B) B) #(struct:dcon-exact () #(struct:c False Any))
; while typechecking:
; (#%app apply-list f (#%app list ls ls))
; originally:
; (apply-list f (list ls ls))

I have never had this error yet, not sure what to make of it :slight_smile: