-
Notifications
You must be signed in to change notification settings - Fork 76
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The output of a function in the component model is itself not a valid component model type #349
Comments
That's an interesting point and indeed this is an aspect of the design where we've oscillated over time between having a unit type vs. having possibly-empty-lists-of-types. IIRC, the most recent switch to the current design was discussed in #41 which has some of the reasons to move away from a unit type. Ultimately, I think there are tradeoffs in either case. In the 0.2.*/0.3 timeframe, we're trying not to make any incompatible changes to the C-M, but this is something we could reconsider (based on way more experience) after that when we consider make breaking changes. Having a component-integrated scripting language with component-level values as first-class values sounds really cool, btw. In the short term, to represent the return value of a function call as a single value, I think you're right that, for case 3, |
Functions have both n-ary parameters and n-ary results in the current design, so at least they are symmetric: both are not first-class values (tuples). The form of closure you are referring to would require that they both are (like in some functional languages). Right now, the language is still closed under (well-typed) function composition f∘g, which it wouldn't be anymore if you broke that symmetry and changed only the structure of results. Hence, that would in fact make matters worse from the closure perspective. |
@lukewagner Thanks, we will approach it as you say for now. We do hope to make Rib a standalone crate, embeddable for the many diverse applications of scripting (extension points in databases, proxies, etc.). @rossberg That's a great point! However, it still doesn't change the fact that the output (nor, as you point out, the full input) can be given a type in the component model. So in a scripting language, what do you do with Of course, we can solve this with In our ideal world, we could ascribe a component model type to the return value of a (non-void-returning) function. However, I think we have enough to workaround the issue for now, so feel free to close if this is only interesting to us. (As a Haskell programmer, of course, I'd love for complete inputs of a function to be typeable, but that's extremely rare in any programming language and I don't think the lack of this will confuse any developers; in fact, the opposite.) |
The classic counter-example would be Scheme and friends, with their multiple values. You can only destructure them or compose with another function taking as many arguments. You get a runtime error if you e.g. try to bind them to a single variable. There is no problem with typing either, it's just not a value type. For example, in Typed Racket you can define a function (define (f) (values 1 2)) and it will have a type (let ((x (f))) x) ;; type error: Expression should produce 1 values, but produces 2 values
I'd say it is pretty much the norm in the camp of typed functional languages, see e.g. Haskell, OCaml, SML, Agda, Idris. |
@rossberg In most formal language semantics I have looked at, typing rules apply to type constructors and terms. No doubt, one could give typing rules for things which are not terms (e.g. multiple parameters or multiple return values). However, that would be a separate context than that of terms, which is the only one we're concerned about for Rib. I didn't know Typed Racket has a precedent for disallowing variable binding on multi-return function invocation. I think we'll probably follow Typed Racket's lead here, and force destructuring on any assignment or attempt to use the result of a multi-return function as an expression. However, in my view, it still leads to some non-uniformity. Ordinarily, you can write It's not the end of the world, for sure, but if no one had ever brought up these issues before, I at least wanted to kick-start a discussion here. Thanks for your input! |
@jdegoes, just a nit: typing rules apply to all expressions, terms = expressions, so these are terms and they have types. There are merely no variables of these types, as their "values" live in a domain distinct from plain values. It is true that you cannot write |
@rossberg Thank you! And since you're giving a free lesson (🙏 😉 ), should the proper way to express what I am looking for be something along the lines of:
??? |
It does have a type in the domain of expressions, but not values, so I'd rather say something like
|
@rossberg I do not see how multi-values qualify as expressions. They can be eliminated through destructuring but there are no operators on them. One could say that import statements are 'expressions' if one works hard enough, but it seems not to match the common meaning of the term. I think multi-values are not values (in the sense that every expression must evaluate to a value), and while they could be ascribed a type (though it's hard to imagine any typing rules or judgements), that "type" exists in a different domain than the types that are ascribed to expressions. |
There is no law that requires all expressions to have types from the same domain (or operators on them). Many languages have multiple type domains. For example, in C++ we have array expressions with array types yet no first-class array values that you could e.g. return from a function. Here is a little toy language with multi-values: 𝑒 ::= 𝑥 | 𝑛 | 𝑒+𝑒 | λ(𝑥,...,𝑥).𝑒 | 𝑒 𝑒 | (𝑒,...,𝑒) | let (𝑥,...𝑥) = 𝑒 in 𝑒 and a type grammar for it: 𝑡 ::= 𝑣𝑡 | 𝑚𝑡 (expression types) Here are possible typing rules, which assign a type 𝑡 to each expression 𝑒: 𝑥 : 𝑣𝑡 iff Γ(𝑥) = 𝑣𝑡 Expression forms like let or application can produce both a single or multiple values, others only either one of them. This roughly corresponds to Scheme / Typed Racket, only slightly generalised in that it treats function arguments as multi-values as well, hence allowing f(g(x)). Many variations of this are possible. |
The output of a function can be:
Note that (2) and (3) are not valid types in the component model, in the sense that it is not possible to type the parameter of a function as having types (2) or (3), because they are not valid types.
We have a scripting language called Rib that is designed to natively work on component model types (similar to Claw), and the existence of (2) and (3) causes some complication.
How?
Because it means that when you invoke a function (a natural thing to want to do within a scripting language), you cannot take the result and store it into a variable that has a component model type.
In essence, the possible return types of a function are "bigger" than the possible input types to the function. This results in the lack of a mathematical property called "closure", and we could say that component model types are not closed under the operation of function application.
It may be that it is too late to effect any change here (in which case, feel free to close the ticket). But also, (2) is very similar to
()
, and (3) is vary similar torecord
—so similar, I would argue, that perhaps from a semantic perspective, (2) could be regarded as "syntax sugar" for()
, and (3) as "syntax sugar" for an anonymous (?) record.With these interpretations, it would be possible to state that the return of a function is a valid component model type, which can be utilized as the type of any parameter of any function, thus achieving closure.
The text was updated successfully, but these errors were encountered: