Re: [racket-users] Types for formlets
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
Re: [racket-users] Types for formlets
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
On Mon, Feb 24, 2020 at 10:28 AM Marc Kaufmann
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
