-
Notifications
You must be signed in to change notification settings - Fork 87
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
User-defined types #422
Comments
I’d really like to see this solved, as it’s making it utterly hard to use typed code in real-life. I suppose #420 could get us a long way if we allow
|
Sorry, I missed this. But I think @litchipi is now on it, right? |
Yes, he is :) We’re supposed to discuss this offline next week |
We’ve had a bit of chat with @litchipi about that. This is actually a bit more involved than what I initially though, in particular because the built-in types are currently hardcoded whithin the interpreter − the definition of types explicitly lists the existing builtin types − meaning that the issue is not just a syntactical one (define new type aliases), but also a typing one (extend the typechecking to also handle type aliases). As a rough implementation plan, this would mean something like:
Another option would be to inline all the type aliases before starting the actual type-checking, but that might not make things simpler, and that means forbidding recursive types altogether (because they would expand to an infinite type), which is probably too restrictive in practice (well, I guess it is, maybe I’m wrong here). (@litchipi don’t hesitate to correct me if there’s anything wrong or missing) |
One idea would be to have a unified type definition, and create pre-defined types |
After some experimentations, I arrive to a form like this which I find satisfactory:
This way, a user-defined type would be just an alias for a static type applied to some contracts (or not), no need to reinvent the wheel, just taking profit from the "power" of contracts. Note: It doesn't work yet, I just propose a syntax / grammar here |
I'm not sure to understand the semantics of this. What does it means to apply a contract to type? I don't think |
It's not about applying a contract to a type, it's about telling that any field of type |
Let me explain a bit why contracts over types, the original example still stands, but is a bit less elegant:
would become
However that allows using contracts to craft user aliases and abstractions, to allow the user to have a type gathering all the checks he wants on it, and all the data he wants in it. I thought that would fit into the original intent of the feature request, allowing data checking using simple type annotations with user-defined types |
Yes, but the syntax Intersections are completely out of the scope of this issue, because the original problem faced is not to have an alias for several contract at once. For those issues, relevant discussions are #420 and more recently #461. If we just want to give an alias to "several contracts", we could allow users to just define value with metadata but without content, like:
But it's a different matter. Once again, here, we just want to give a name to a type expression. Not meta-data, no contracts involved, just an alias to reduce verbosity. Second, how do you typecheck this?
This example doesn't really makes sense, because we don't know how to typecheck this currently. Maybe you meant to use the What we want is rather:
|
Okay so in other words, what I was talking about is already possible and implemented. |
My example above is not supported today, so not really. It could make sense to have in some form, someday. But the point is that it is a different matter than this issue, which is about type aliases.
This, plus also handling type aliases for contract generation, which means you need to keep those type aliases around at runtime. An alternative would be to substitute type aliases and erase the mat program transformation time. But we already handle a bunch of different delayed substitutions as environments already, so I think it would make sense to do the same for type aliases, and keep them around at runtime. |
I have a problem dealing with a line in the
It checks for unbound type variables, which is what user-defined types are. However I cannot pass the information "This type is bound elsewhere" to the function Is type-bonding something really meant to be ran at a grammar level ? Why not moving it from the grammar to the type checking section (somewhere in the |
It's done at parsing time for the following reasons:
However, it is indeed more involved when some type variable may be bound by Otherwise, we can do as we do for standard variables: only check at usage points (in typechecking and in contracts elaboration) that all type variables are indeed bound. For typechecked terms the checks will be duplicated, but that is not a terribly costly check to do. This is already what we do for normal variables. |
A little update on this old issue: we're one step away from implementing this in a straightforward way, given the infrastructure put in place for checking for contract equality (#834 and follow-ups) and the soon to be merged #1442. We don't event need new syntax, the idea being that in On the other hand, something that you might want to do is to export types as a part of a library. I believe this will prove harder, because what I propose would be slightly fragile if you add records, record accesses and indirection: at some point, Still, in the meantime, I don't think trying to use existing information to extract a static type from a value would hurt. Worst case, we later get a more principled construct such as |
@yannham: coming back to this after quite some time, I'm a bit confused by your last comment. As I understand it, something like
What did I get wrond there? |
Sorry if that wasn't clear, but my last comment implied that we're one step away from having this to work, because everything is in place. However, I think further discussions unveiled that this might not be a great idea to do that silently. There is always this tension between having something magic and automatic, trying to be smart, but which then breaks unexpectedly when the typechecker has reached the limit of its smartness. That is, this is ergonomic, but no very reliable (I'm talking about keeping the exact same syntax but just having the typechecker trying to "unfold" variables as static types) Although I don't like to introduce a myriad of new keywords, today I tend to prefer the idea of making it explicit that something is to be considered as a type at typechecking time with this I believe this is straightforward to implement and backward compatible (this doesn't require Thanks for putting this back on our radar. It's been a long standing issue, and would surely be a very useful addition. I'll try to move it forward. |
Is your feature request related to a problem? Please describe.
Maybe I just missed it, but it seems that there’s no way to define (name) custom static types.
Describe the solution you'd like
A syntax allowing me to (for example):
Describe alternatives you've considered
Use contracts everywhere instead, something like:
But that’s a bit of a shame
The text was updated successfully, but these errors were encountered: