-
Notifications
You must be signed in to change notification settings - Fork 37
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
Designing a Type System for Passerine #36
Comments
Idris provides inline syntactic sugar for changing one field of a larger record: |
Thanks for that great idea! Here are my thoughts on it: In Passerine, we use the
As tuples are just records indexed by position rather than by name:
I think a generalized syntax to modify ADTs without having to mutate them is a great idea. I'm not entirely sure how we should do this - we could go with either a macro, an operator, or a function. Here's how a macro could work:
where
This, of course, is just one option of many. Another option is to expose these ADT mutations as functions. Say we want to construct a tuple with a modified second field:
This is honestly a bit cumbersome. I think your solution, to introduce a generalized syntax, also works well. We'd just have to figure out the exact semantics in all cases, and how it relates to pattern matching. Perhaps we could define an operator like
Again, a lot of options. My favorite one so far is probably the |
There's four different ways you might want to change a data structure: you might replace a field with a new value, or you might pass its old value through a function to get the new one, and then for both of those you can either return a new data structure or mutate it in-place. There should be similar syntaxes for all four, and ideally those syntaxes would be like how you read a value as well. Field replacement is a special case of passing a field through a function (because you can use a function that returns the same thing no matter its argument) but it's important enough that it should be easy. As I see it, you want composability for sure. Lenses let you say "in the 'name' field of the fourth item of the first item of my data, read/change that." The problem is mutability, which lenses provide no inspiration for: only one level of that nested structure should ever mutate at once. Maybe you wanted to edit the topmost tuple by generating a new edited version of what was inside it. Maybe you only want to mutate the name string itself. I say only one level should mutate at once, but a way to combine changes is also necessary. If a programmer want to make two changes to different parts of that 'name' field, she shouldn't need to specify where it is within the two tuples each time — that would be redundant. I like the Lastly, there's something to be said for ease of nesting. Pattern matching is so beloved by functional programmers because it takes something sequential and imperative — accessing nested parts of a tree structure — and makes it declarative — describing a tree structure with holes. Gone are the days where we only index everything in an array: we create recursive structures. Getter and setter functions are chained in a sequence, yet getters are better as recursive pattern matching (internal rhyme not intended). Setters are marked for the same fate as getters: replacement by something declarative. That's my thought process behind copying pattern matching for the various ways to set things. Granted, we'd still make short chains like |
Before I move on to the meat of my ideas regarding the points you brought up, I'm just going to put the 'ways you can mutate things' into a little list:
By the way, all that local mutation means is that the lifetimes of variables that are mutated can't exceed the scope in which they are defined; in other words, any variables that cross function boundaries must cross boundaries as owned values, and can not exist inside reference cells. With that out of the way: First thing to note is that mutating a value is the same thing as creating a new value and overwriting the old. Of course, this doesn't mean that the implementation need to make a copy of the value (vaporization, when fully implemented, accounts for this with reuse analysis), because we can infer that
We could also introduce a macro that expands to this statement. This cuts away half of our table; realistically, we only need to define a way to create a new value from an old one; the mutation can be handled with reassignment. So the question becomes, how do we:
As you succinctly pointed out, 1 is a special case of 2; we can always make a function that returns a value no matter what, e.g.
What we basically want is pattern matching for selective construction:
I think it's possible to 'extend' pattern matching to support selective construction. Like how pattern matching 'describ[es] a tree structure with holes', if we 'describing a tree structure where the holes, instead of being variables to bind, are ways to update values', we can selectively construct new values. We'll call these patterns where the holes are update rules Construction Patterns. In other words, a construction pattern First, consider we define a struct named
Here's what pattern matching on the
Let's introduce a construction pattern:
After this,
So, to recap:
And we can now fill in the two-way table:
Of course, we could use the
I think the idea of Construction Patterns scratch that itch - we'd have to work out the exact semantics, but I think I like this skeleton. What do you think @IFcoltransG? |
This matches what I had hoped for, if you'll excuse the pun. The plan is set out logically and workably. |
Here's what I'm imagining:
This could be useful, say if you have defaults:
And again, the keyword
Anyway, I'm still thinking about homoiconicity. The general idea is as follows: A pattern, in general, takes the form:
For normal construction, Actually, on the topic of functions in pattern constructions: perhaps we can make the argument implicit:
I think that's a lot nicer - it also disambiguates fields that are functions. For pattern construction,
Does this make sense? Anyway, I think we need a more general vocabulary for describing patterns. |
If we return to one of the example I gave above, "in the 'name' field of the fourth item of the first item of my data, read/change that." For a start, tuple construction patterns haven't been nailed down yet, but I presume it could be something like Oh, and looking at your general pattern form, the website uses semicolons for enums, because otherwise a record would be ambiguous with an enum full of 'is' patterns. |
So we're facing a bit of a dilemma:
I think option number 2 is the way to go. We can formalize it as follows:
This is nice because it means we can nest construction patterns until we reach a terminal lambda. With the introduction of
This is a bit of an aside, but I think if we:
The use of a comma isn't ambiguous.
With the new semantics above and the removal of implicit lambdas, we can make it I realize we have to make some tradeoffs here, and there is more discussion to be had. We have the Weekly meeting today at 14 UTC if you want to hop in. What are your thoughts? |
For implicit lambda syntax, you could replace the |
I just want to say thankyou @slightknack for making this such a joy to read! I adore your prose 😍 ever thought of putting together a blog? |
@IFcoltransG: Oh gosh, I thought I had written a response, but I guess I didn't send it. I forgot what I wrote specifically, but here's a loose summary:
Until we've implemented construction patterns, I think what we have now; i.e. basically just normal patterns delimited with I don't expect the additional arrow shorthand to be strictly necessary because I expect transformations to primarily be named functions; in other words, instead of writing
This is a great point! I didn't even realize this, thanks for bringing it up. In Passerine, this would be written as:
And could be included in the standard prelude. I believe the reason I didn't respond initially is because I had started elaborating on another topic, then never got around to sending the response. If I remember what other topic I addressed, I'll write out another response with what I remember. |
I'm glad you enjoy my writing! I used to keep a blog, but never got around to finishing anything; it was more a loose collection of notes than anything else. There's an archive of it here: https://website.slightknack.workers.dev/writings. The blog was hosted at https://slightknack.dev/, but I've changed that to a placeholder page for now. I plan to flesh it out and add a blog to it at some point. |
So the typechecker would implicitly decide whether it's a Perhaps it's a contrived example, but what if your record held a |
This is not ambiguous, and can be resolved using standard judgement rules: If we know the type of
As we can see, natural has a defined type, because it is an associated value. Next, we'll define
What's important to note is that because we know the type of
No! We know that the
From this, we have a generalized update rule. If we try to apply it to our previously defined
As explained, the reason this works is because we can infer the update rule to be of type
In short, because we have well defined judgements for the types of update rules, we can infer the types as needed. Does that make sense? (To reiterate, the judgement is:
|
I like that this looks like it could feasibly be a function with a signature like |
I'm unsure if that solves the syntax problem. Let's say I have a record with a If Let's say instead that
However, we can also imagine treating These are two different behaviours. A user could supply the identity function hoping not to change their incrementer, then find it has replaced itself with the identity and become useless. Another user could supply the identity function because they don't want their |
Thanks for your detailed response!
if foo is
The identity function would always produce no change. To replace the function with the identity function, you'd have to do |
I think I understand: you've removed the There are a few reasons to name your parameters. Pointful style is closer to how an imperative programmer thinks, and it avoids the mess of combinators that come from chaining lots of functions pointfree. It's a matter of style, after all. So suppose you're writing pointful code:
The Using
Much clearer. Thoughts? |
If we were to introduce a syntax to turn operators into functions, say, something like
Yeah, that's true. Even with the old style, I'm not sure you'd write it out inline though:
It's not ideal, for sure.
This is pretty nice! it reminds me of the
Of course, I'd imagine we should have things like |
Support a system like the following: Note: Collapsed by @slightknack for length; click to expand a list of typing rules.
Support of sub and super typing
|
The above related to contemporary language:
Following can be supported in the type system:
Also ability to freely define sub and super types. |
Hey @sirinath, I appreciate the work you put into describing a list of typing rules and ideas! I note that you introduce some additional syntax, like You also introduce the notion of sub/super typing via
This is extremely fairly fine-grained control, and not something we should expose to the user directly: the current model of all types being structural unless wrapped in an outer Thanks! |
I have:
Also,
If you say If the type hierarchy is open
Many languages do not expose this. But this flexibility will make the type system more powerful. The language also would be nearly flexible as a dynamic language but fully type checked. The syntax I used is for illustration purposes only. You can adopt it as needed as long as the concept is fully supported. |
Alright. I don't think that explicitly stating whether names are structural or nominal is the best solution, for reasons I'll explain in a later section.
Yes, that's a given. :P
I'd argue that many languages do not expose this for good reason: this makes it non-obvious as to how types match in all circumstances: you have to manually parse out the definition in your head. Something like if it's a Such a system would also imply that it's possible to have types of the same name but different structure, which while technically making sense, just wouldn't work well in practice. |
In structural types one need some labeling to refer and reuse type definitions. Also for tuple elements it is a convenience to address them by a lable. I feel it is better to have a lable with the ability to specify if it is significant or not. |
In structural types one need some labeling to refer and reuse type
definitions.
I think I need to clarify as to how structural typing works in Passerine,
and how labels constrain this type system to allow for nominal typing where
needed. In short, base product types, such as records and tuples, are
structurally typed: records by field names, tuples by index and arity.
These types are used in pattern matching:
{ age: old_age } = { age: 70 }
If we wanted to embed this struct inside another, with "labeling to refer
and reuse type definitions" we'd have to explicitly declare them. Using the
latest revision of type definition syntax, this would look something like:
Person = type { age: Natural }
`Person`, then, would be a Label that represents `{ age: Natural }` Note
that Person is no longer directly structurally typed. You'd have to first
match on name, then match on the structure itself.
jeff = Person { age: 70 }
{ age: old_age } = jeff -- this is invalid
Person { age: old_age } = jeff -- this is valid, match on person first
If we have a struct, we can make it nominal by wrapping it in a Label; the
type's definition ensures that it is correct upon construction.
Also for tuple elements it is a convenience to address them by a lable.
A tuple whose elements are addressed by label is called a *record*.
I feel it is better to have a lable with the ability to specify if it is
significant or not.
I disagree, for reasons I have laid out in the previous post. The current
typing scheme provides a nice dichotomy:
- We don't have a structure, and use a Label for typing (nominal types)
- We don't have a label, and use structure for typing (structural types)
We only have to worry about one or another, there's a clean separation of
concerns. This also works well with row polymorphism, as record types whose
fields are a superset of another are matched.
I hope this response helped! In the future, @sirinath, please rationally
explain the reasoning behind an idea or suggestion, rather than just
posting uncontextualized examples or links to semi-related articles. Thanks!
|
Goals of a Type System
Passerine's type system is a bit fuzzy at the moment, due to it's dynamic nature in terms of implementation. However, Passerine is a functional programming language, and in that vein I'd like it to have an ergonomic albeit flexible type system. Here are the goals we should try to meet:
|
) that are total (verified through algebraic effects) and verified upon construction.What we need to know
For each of these points, we need to decide the following:
TL;DR and how you can help
I'm not going to answer these questions in this first post, rather, I hope to start a discussion on the topic. I'll try to formalize most of the type system tomorrow, including rules for structuring/destructuting, type definitions, algebraic effects, and so on. I'd really like some input on what you think are needed features of the type system.
The goal of the type system is a simple one: make it feel as flexible as a dynamic type system while still providing the guarantees and speed of a static one. Either way, Passerine is strongly typed.
It doesn't matter if you have 10 years of experience with type systems or 10 minutes - This is the first time I've designed a full-on type system, and I'd like to get it right, from both a theoretical and practical point of view - so don't worry, any feedback is appreciated. Please reply to this issue with any thoughts, issues, comments, questions, suggestions, etc. If there are features in other languages you think have merit, bring them up. Thanks!
The text was updated successfully, but these errors were encountered: