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
On Mon, Feb 24, 2020 at 9:31 PM Philip McGrath <phi...@philipmcgrath.com>
wrote:
> 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
> <https://github.com/racket/web-server/blob/master/web-server-lib/web-server/formlets/syntax.rkt>
> (and also here
> <https://github.com/racket/web-server/blob/master/web-server-lib/web-server/formlets/unsafe/syntax.rkt>,
> 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 <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
> <https://github.com/racket/web-server/blob/master/web-server-lib/web-server/formlets/unsafe/lib.rkt>—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
>
> On Mon, Feb 24, 2020 at 10:28 AM Marc Kaufmann <marc.kaufman...@gmail.com>
> wrote:
>
>> 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
>>
>> --
>> 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
https://groups.google.com/d/msgid/racket-users/CAD7_NO7tNK3AmJ2n_4C8aBmU%3D%2B2HznvdQ2d_9bmW2%2BhMYaTYPQ%40mail.gmail.com.
