[dan-robertson]

Question: 1. Can a GET request have a non-empty request body?

2. Assuming you don’t know the answer to that question, will the type system you use be able to tell you the answer to that question?

This is a pretty simple constraint one might want (a constraint that only certain requests have a body) but already a lot of static type systems (e.g. the C type system) cannot express and check it. If you can express that constraint, is it still easy to have a single function to inspect headers on any request? What about changing that constraint in the type system when you reread the spec? Is it easy?

The point isn’t that type systems are pointless but that they are different and one should focus on what the type system can do for you, and at what cost.

[lkitching]

Any statically-typed language with generics can express that by parameterising the request type with the body type. A bodiless request is then just Request[Nothing] (or Request[Unit] if your type system doesn't have a bottom type). Accessing the headers just requires an interface which all static languages should be able to express.

[dan-robertson]

(1) note that “statically-typed language with generics” excludes a lot of statically typed languages, including C and Go (at least pre generics).

(2) this misses the meat of the question which is how to express that (eg) a GET request doesn’t come with a body and a POST request does. I suppose that you’re suggesting that one registers a url handler with a method type and that forces the handler to accept responses of a certain type. Or perhaps you are implicitly allowing for sun types (which aren’t a thing in many static type systems.)

(3) even in C++, isn’t this suggestion hard to work with. That is, isn’t it annoying to write a program which works for any request whether or not it has a body because the type of the body must be a template parameter that adds templates to the type of every method which is generic to it. But maybe that is ok or I just don’t understand C++.

[lkitching]

1) Looking at the TIOBE index, all the static languages I recognised on there are: C,C++,C#,Visual Basic,Go,Fortran,Swift,Delphi,Cobol,Rust,Scala,Typescript,Kotlin,Haskell and D. Of these C and Go are the only two that don't appear to support generics so I don't think this approach excludes a lot of static languages.

2) If you want to distinguish GET and POST requests statically then you just need a type for them e.g.

    GetRequest<TBody> implements Request<TBody> { }

if you don't need to do this then you can just add a method field and use a single type for both. Either way you don't need to use sum types so a language like Java can express it.

3) Yes you'll have to make functions that don't care about the body type generic so this approach could become unwieldy if you have a few such properties you want to track.

[xapata]

How about values restricted to identifiers currently in the database table? There's always something the type system can't do.

[jolux]

F# has a feature called type providers that make this sort of bookkeeping between the database and the code less tedious, but even if you mess it up, static typing still gives you more safety than dynamic. If your code blew up because it should have accepted an identifier it didn’t, you know that the code has not been written to handle that case and can fix it. Alternatively, you can just choose to ignore this, and do what a dynamic language does. There is nothing stopping you from being dynamic in a static language, passing everything around as a map, etc.

[dharmaturtle]

A demo of a SQL type provider in action: https://youtu.be/RK3IGYNZDPA?t=2539

It requires a bit of elbow grease to make it work with a CICD system... but it works :D

[xapata]

That's nifty.

[twic]

1. Yes. It's weird, but it's legal HTTP.

2. Sure. The request type has a body property.

[dan-robertson]

Does “the request type has a body property” actually imply (1) though? In a language like C or C++ or Java, you could have a protocol like “body is always null on GET requests.” The question isn’t really about HTTP, that was just an easy-to-reach-for example, it is really about what having explicit types allows one to deduce about a program.