Skip to content
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

Adding documentation for subtyping #1990

Merged

Conversation

Eckaos
Copy link
Contributor

@Eckaos Eckaos commented Jul 8, 2024

In this pull request, I will add the manual documentation for subtyping(Record/Dictionary, Array/Array, Dictionary/Dictionary) and an integration test to chain functions on records.

@Eckaos Eckaos marked this pull request as ready for review July 17, 2024 11:30
Comment on lines 260 to 262
Subtyping is a relation between two types where
you can use one of the type in place of the other one.
In Nickel, there is :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The beginning is a bit dry. The best way to introduce a notion is to motivate it, with an example. For example, start by saying something like:

While distinct types are usually incompatible, some types might actually be safely converted to some other types. Take the following example:

let extended : {_ : Number} =
 let initial = {foo = 1} in
 std.record.insert initial

And then go on to explain that technically the types don't match, but it's legal to "forget" some information to go from a record type to dictionary type.

And go on to explain why this is accepted while the types don't really match specifically.

doc/manual/typing.md Outdated Show resolved Hide resolved
Eckaos and others added 4 commits July 18, 2024 15:01
@Eckaos
Copy link
Contributor Author

Eckaos commented Jul 19, 2024

I added motivation for subtyping. I was wondering do I add constructors(Array, Dictionary) in this pull request too or do I make another pull request to update the manual ? @yannham

@yannham
Copy link
Member

yannham commented Jul 19, 2024

I think you can add it to this PR. It feels a bit artificial to split this in several ones, given the small changes all focused on the same file.

@Eckaos Eckaos changed the title Subtyping/record dictionary documentation tests Adding documentation for subtyping Jul 22, 2024
@Eckaos
Copy link
Contributor Author

Eckaos commented Jul 22, 2024

I don't understand why my array example does not work.

I didn't add to the manual Record/Record and Dyn subtyping for now because it is not implemented.

@Eckaos
Copy link
Contributor Author

Eckaos commented Jul 25, 2024

I added a generic example for expanding a function to work around the fact that we don't have arrow subsumption.
Do you think, the documentation miss something else ? @yannham

In this example, there is a silent conversion from `{foo : Number}` to `{_ :
Number}`. This is safe because `foo` is of type `Number`, and it's the only
field, which means that a value of type `{foo : Number}` is effectively
dictionary of numbers. In the typing jargon, `{foo : Number}` is said to be a
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
dictionary of numbers. In the typing jargon, `{foo : Number}` is said to be a
a dictionary of numbers. In the typing jargon, `{foo : Number}` is said to be a

doc/manual/typing.md Outdated Show resolved Hide resolved
doc/manual/typing.md Outdated Show resolved Hide resolved
@yannham yannham enabled auto-merge July 26, 2024 16:33
auto-merge was automatically disabled July 26, 2024 16:51

Head branch was pushed to by a user without write access

@Eckaos Eckaos requested a review from yannham July 26, 2024 17:28
doc/manual/typing.md Outdated Show resolved Hide resolved
@yannham yannham enabled auto-merge July 29, 2024 10:50
@yannham yannham added this pull request to the merge queue Jul 29, 2024
Merged via the queue into tweag:master with commit 699cf5d Jul 29, 2024
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants