search

sanctuary-js / sanctuary-def

Run-time type system for JavaScript
MIT License
294 stars 23 forks source link

types: define Void #280

Closed davidchambers closed 4 years ago

davidchambers commented 4 years ago

I struggled with the description, and I'm not completely satisfied with the first sentence of the second paragraph. Suggestions are welcome. :)

Avaq commented 4 years ago

What's the motivation behind the addition of this type?

davidchambers commented 4 years ago

What's the motivation behind the addition of this type?

While @voxbono and I were working on a functional server we decided to use futures for HTTP responses. We then realized we had no use for the first type parameter: even if the database was inaccessible we could resolve with a Response value for a server error. I was about to suggest using Future Null Response but realized that Future Void Response would convey more information.

Avaq commented 4 years ago

Hmm, usually Future a Response conveys just as much information - it is assumed that a completely unrestricted type variable has no concrete type.

The problem with Future a Response is that reject (42) is a valid member of it from the perspective of the type checker.

So you want a type that says "the type at this position must never become concrete". Maybe the description could be something like:

Indicates that the type will never become concrete. For example, a future of type Future Void String will never be rejected.

davidchambers commented 4 years ago

Indicates that the type will never become concrete.

I'm not completely satisfied with this sentence either. I'm struggling to use a type to indicate that no value will ever be present at the position in question as I lack terminology for associating values with type parameters.

Avaq commented 4 years ago

the type at this position must never become concrete

will ever be present at the position in question

I guess we both think of it as "position". Maybe we can use this word?

Avaq commented 4 years ago

When talking in terms of "concreteness" we can refer to the type, however.

davidchambers commented 4 years ago

I like “position”. The current description refers to position, albeit indirectly:

May be used to convey that a type parameter of an algebraic data type will not be used.

This, for example, refers to the positional arguments a and b in Future a b.

I'll merge this pull request in its current form, but I'd like to improve the description in the future.