or
or
By clicking below, you agree to our terms of service.
New to HackMD? Sign up
Syntax | Example | Reference | |
---|---|---|---|
# Header | Header | 基本排版 | |
- Unordered List |
|
||
1. Ordered List |
|
||
- [ ] Todo List |
|
||
> Blockquote | Blockquote |
||
**Bold font** | Bold font | ||
*Italics font* | Italics font | ||
~~Strikethrough~~ | |||
19^th^ | 19th | ||
H~2~O | H2O | ||
++Inserted text++ | Inserted text | ||
==Marked text== | Marked text | ||
[link text](https:// "title") | Link | ||
 | Image | ||
`Code` | Code |
在筆記中貼入程式碼 | |
```javascript var i = 0; ``` |
|
||
:smile: | ![]() |
Emoji list | |
{%youtube youtube_id %} | Externals | ||
$L^aT_eX$ | LaTeX | ||
:::info This is a alert area. ::: |
This is a alert area. |
On a scale of 0-10, how likely is it that you would recommend HackMD to your friends, family or business associates?
Please give us some advice and help us improve HackMD.
Syncing
xxxxxxxxxx
Reading club: Linear types
tags:
reading-club
Link: https://blog.yoshuawuyts.com/linear-types-one-pager/
Different Designs
Note: I (Yosh) don't really like
linear
as a keyword, so it's more for illustration purposes. Imoleak
seems better, but that would imply!leak fn
, which maybe is a bit weird - but again idk. Exact syntax is sort of the least important thing here imo.(eholk) Nice seeing options laid out like this. Opt-in or opt-out. Opt-in would probably be less disruptive.
(yosh) Would be nice if we could start with an empty set of effects (
total
), and make all other effects opt-in on top of that. But that's not really what we have today, but maybe something to strive for? idkKoka paper: https://arxiv.org/pdf/1406.2061.pdf
Fork the Compiler?
(eholk) This seems like the kind of language change where (temporarily) forking the compiler makes sense. It means we can have a trial period before adding an insta-stable
+ ?Leak
bound to everything in std, but also would give people a chance to try using the language to get a sense of how usable it is.(As far as I [eholk] know, no one has shown that true linear types work ergonomically at scale, so this would give us a chance to demonstrate that.)
Yosh: the changes you would need to make to the stdlib is disallow:
ManuallyDrop
(mem::forget
)UnsafeCell
-based (Rc
,Arc
,Mutex
, channels)thread::spawn
Eholk: Do we need
UnsafeCell
for1:1
channels?Yosh: that's a good question!
eholk: an implication of channels needing
UnsafeCell
is that linear types cannot beSend
? Maybe we need a linear channel?Yosh: I think we can make linear types
Send
, but I don't know if we can create linear channels?Shared Ownership, Interior Mutability, Guaranteed Destructors - Choose Two
(eholk) If I remember right from the leakpocalypse, the problem was that
Rc
/Arc
combined with interior mutability was how we got in to trouble. It seems like maybe the primary contribution of this type is that it lets us annotate eitherRc
orUnsafeCell
with!Leak
to let us choose another side of the triangle, but which one should we pick?(eholk) Is Interior Mutability + Guaranteed Destructors possible? Yes!
Box<RefCell<T>>
can't make cycles by itself.(eholk) Can't make cycles with just
Arc
, except if you use the cyclic constructors.new_cyclic
Gankra's safe forget code:
Eholk: you need both
Rc
andRefCell
to make a cycle. That means interior mutability + shared ownership.Yosh: does that then mean that we can leave
Arc
alone and only disallow theUnsafeCell
-basedMutex
etc types?Eholk: I think so!
Eholk: Do we want just interior mutability without shared ownership? No! If you have unique ownership you can already mutate, so interior mutability is only interesting with shared ownership.
Yosh: There seems to be a connection between tree shaped data and tree shaped computation (structured concurrency) - exactly what that connection is is unclear.
Connection to async drop
Yosh: had a chat with Niko on this a few weeks ago. We sort of settled on that async Drop and linear Drop probably shouldn't be the same feature?
Yosh: we also discussed what a full async drop would look like - if it propagates the way current
Drop
propagates, then we'd probably need a way to tag structs as async. So if you nest a struct with an async destructor inside of another struct, the destructors are still run.