Types for formlets

[Marc Kaufmann]

Hi all,

I wonder what the best way is to integrate formlets into typed programs. I simply `require/typed` formlet-display  as type (-> Any Any), which is not illuminating, but the display part is rarely the problem.

formlet-process is tricky. The earliest point at which I 'know' the type of processing a given formlet is directly when formlet-process is called, so that's the best time to start typing to get most of the types checked. Ideally I would do something like:

(define s-formlet
  (formlet (div (label "Enter a string:")
                ,{=> input-string a-string})
           [a-string : String]))

and be done with it. Of course I cannot type it this way. One solution is to define

(define (s-formlet-process a-formlet a-request)

  (formlet-process a-formlet a-request))

provide it, and then require it with the correct type in the next file. That's sort of what I am doing right now, but it requires quite a bit of boiler-plate everywhere. The problem is that I don't see how I would even start typing s-formlet itself, since (I think) it is a macro that changes how formlet-process deals with it, so I don't even know where to start typing any of it. When I expand formlet-process in the macro stepper, it turns into the application of some idY11 with something lifted (none of which I understand), and I don't see how I would make the type of (formlet-process a-formlet ...) dependent on which formlet it is that I am processing.

One idea I had is to define my-formlet-process which takes the name as a symbol, rather than as an id, and uses different type signatures depending on the symbol, using case->:

#lang racket

;; UNTYPED

(define (my-formlet-process name req)

  (cond [(eq? name 'integer-formlet) (formlet-process integer-formlet req)]

            [(eq? name 'string-formlet) (formlet-process string-formlet req)]

...

and then require/typed this via (case-> (-> 'integer-formlet Integer) (-> 'string-formlet String)). This cuts down on having to define all the intermediaries, and puts all the types for formlets in one place. It still feels more tedious than it has to be, but it is probably not trivial to make this much easier.

Any thoughts on if the above is an OK if not best practice, or ideas for improvements? I guess using types with some rather sophisticated macros may in general be a little tricky - any pointers to other places on how to do this and how to figure out how to type it are appreciated.

Cheers,
Marc

[Philip McGrath]

Hi Marc,

You're right that there will be some challenges in using formlets in Typed Racket. The easiest approach will probably be to keep defining formlets in untyped modules and importing them with `require/typed`, perhaps with helper functions or macros to eliminate some of the boilerplate. Pragmatically, you aren't even loosing much type safety here: formlets are processing raw bytes from the outside world, and there is an inherent possibility for dynamic failure. Using `require/typed` will enforce with contracts that the values dynamically coming in have the right types and raise an exception otherwise.

But you asked about how to type formlets. I don't have a worked-out answer, but I'll try to point you to some of the implementation details that would be relevant.

To start, in your example:

(define s-formlet
  (formlet (div (label "Enter a string:")
                ,{=> input-string a-string})
           [a-string : String]))

the `formlet` form is indeed a macro defined here (and also here, sadly basically by copy and paste, because that seemed easier than properly abstracting over the shared parts when I added the unsafe version).

The `s-formlet` itself, though, is a normal runtime value, as is `formlet-process`: my guess is that what you were seeing from the macro stepper was some of the implementation of enforcing the contract on `formlet-process`.

The `formlet` syntax is built on a functional layer. This is discussed in the docs, and in more detail in the paper and a technical report. (You may be interested to note that the papers present formlets in a version of OCaml, a statically typed language: the challenge for Typed Racket, as usual, isn't the types but the typed–untyped interaction.) Formally, a formlet value is an "applicative functor" or "idiom."

Concretely, a formlet is represented as a function. In Typed Racket syntax, we might try to write:

(define-type (Formlet A)
  (-> Natural (Values (Listof Xexpr) (-> (Listof Binding) A) Natural)))
(: s-formlet (Formlet String))

That type looks pretty strange! Here's what's going on. The formlet is called with a numeric counter, which is used to generate field ids. Its three results are some HTML to display, a function

to process the bindings from the request, and the new value for the counter. (There is an unchecked invariant that the new counter value should not be less than the old value.) The `formlet` syntax expands to uses of the combinators `pure`, `cross`, and `cross*` to assemble compound formlets from smaller pieces. This functional interface can also be used directly.

That may be enough to illustrate some of the problems. Typed Racket can have trouble generating contract for polymorphic functions like `(: formlet-process (∀ (A) (-> (Formlet A) Request A)))`. Furthermore, the `Formlet` type I wrote is a simplification: formlets are actually allowed to produce multiple values from the processing function, which again is a problem for typing. (I think it would be reasonable to eliminate that feature from a Typed Racket interface: I don't think it is used often, especially since `formlet/c` was broken for a while for the multiple-return-values case.) Because of the way `cross` is implemented, there is a great deal of function composition, which could mean many, many crossings of the typed–untyped boundary with contract enforcement costs.

An approach I might consider would be re-implementing the core combinators—essentially this module—in Typed Racket and writing a typed version of the `formlet` macro that expands to them. You could still use the library formlets by importing them with `require/typed` at some concrete type.

I'm happy to talk more if you're interested.

-Philip

--
You received this message because you are subscribed to the Google Groups "Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/6241af3c-4b2d-43a5-a76a-2a14b02bc153%40googlegroups.com.

[Marc Kaufmann]

Hi Philip,

thanks for your extensive write-up -- due to Racketfest I didn't have the time to digest it earlier. Yeah, I don't see why I would want to type the formlet creating code itself, that seems like it will not be useful. What I really want is to type the output from a formlet in the formlet definition to avoid some boilerplate, but for now I can live with it, and won't try to add macros doing the typing for me, as I'm sure to screw it up. Maybe later.

How do static type systems deal with input/output in languages that don't have contracts? I guess they use code that is guaranteed to work or throw exceptions if the input isn't of the correct type? At the end of the day, typing concrete formlets in this way isn't that different.

I admit that after 2 years of avoiding formlets and cousins like the plague, I am coming to like them again. I grokked them so little that the code to make them work was a huge blob that made no sense.

Cheers again,

Marc