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
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
>
> (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
