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

The `formlet` syntax is built on a functional layer. This is discussed in
the docs <https://docs.racket-lang.org/web-server/formlets.html>, and in
more detail in the paper
<https://links-lang.org/papers/formlets-essence.pdf> and a technical report
<http://homepages.inf.ed.ac.uk/slindley/papers/formlets-tr2008.pdf>. (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
<https://github.com/racket/web-server/pull/29> 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
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.


On Mon, Feb 24, 2020 at 10:28 AM Marc Kaufmann <marc.kaufman...@gmail.com>

> 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
> (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
> --
> 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+unsubscr...@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
> <https://groups.google.com/d/msgid/racket-users/6241af3c-4b2d-43a5-a76a-2a14b02bc153%40googlegroups.com?utm_medium=email&utm_source=footer>
> .

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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 

Reply via email to