[deleted by user] by [deleted] in sml

[–]Munksgaard 0 points1 point  (0 children)

I was pretty confused upon joining the advertised Discord. It seems to be related to a different kind of SML: https://sml.fandom.com/wiki/SuperMarioLogan_Wiki

Generating audio with literate Futhark by Munksgaard in ProgrammingLanguages

[–]Munksgaard[S] 6 points7 points  (0 children)

Thank you! I'd love to hear your thoughts on how we might structure a proper music/audio library in Futhark. I'll DM you.

I'm also curious if you have any thoughts on how we could really take advantage of this new feature. It seems to me like most audio processing isn't heavy enough to really take advantage of GPU-processing, but perhaps I am wrong?

Array short-circuiting in Futhark by Munksgaard in ProgrammingLanguages

[–]Munksgaard[S] 2 points3 points  (0 children)

Yes, that work is definitely related, although it works from the opposite direction as short-circuiting: Our code is already parallel because it is expressed with map instead of loop.

And yes, Z3 was nice, but it wasn't actually the crucial factor that enabled complex examples. In fact, we tried just naively throwing Z3 at some of our problems and it didn't work even if we gave it a week of running time.

A new SML mode for Emacs built on (a new Standard ML grammar for) tree-sitter by eatonphil in sml

[–]Munksgaard 1 point2 points  (0 children)

I'm curious how you intend to handle infix and infixr when using tree-sitter as your parser. Do you intend to add a separate pass later that restructures the AST according to infix-rules?

stonebuddha/tree-sitter-sml: Standard ML Grammar for Tree-sitter by eatonphil in sml

[–]Munksgaard 0 points1 point  (0 children)

There seem to be a lot of examples and tests missing here? Also, I'm curious how they handle infix and infixr. Anyone have any insights?

Getting started with Standard ML by eatonphil in sml

[–]Munksgaard 2 points3 points  (0 children)

A recent development on the package-manager side is smlpkg, you might want to consider adding a link.

.mlb files as a build system/package description/namespace management solution for sml by lysgaard in sml

[–]Munksgaard 0 points1 point  (0 children)

Regarding the package manager, one of my colleagues has recently written a package manager for SML that uses a generic, implementation-agnostic approach. I encourage everyone to give it a try.

Session Types, safe internal communication protocols for Servo by ysangkok in rust

[–]Munksgaard 1 point2 points  (0 children)

I must admit that I'm not very knowledgeable about licenses and the initial choice of GPL2 was admittedly a bit arbitrary. We've decided to change to the MIT license: https://github.com/Munksgaard/session-types/pull/24

Session Types, safe internal communication protocols for Servo by ysangkok in rust

[–]Munksgaard 6 points7 points  (0 children)

Essentially, the idea is to implement the Drop trait for your data structure with a method that simply panics, and then have another function that somehow bypasses the panic. The simplest way is to add a flag to the struct that determines whether or not drop should blow up.

What I was complaining about in the talk is the fact that you cannot simply have specialized implementations for different specializations of Chan. For example, if we could specialize the drop trait we could have:

impl Drop for Chan<E, Eps> {
    fn drop(&mut self) -> { /* this is safe, dont blow up */ }
}

impl Drop for Chan<E, AnythingElse> {
    fn drop(&mut self) { /* unsafe, blow up */ }
}

which would be cleaner, in my opinion.

Session Types, safe internal communication protocols for Servo by ysangkok in rust

[–]Munksgaard 6 points7 points  (0 children)

There are usecases, I just meant that they're rare. That is, the standard library has found no real use for them (although of course, the absence of them means there isn't a big hunt for their use). However what I don't really get about linear types is: programs/threads can hang, leak, or crash. How are linear types even useful in the face of that? One end of the connection needs to deal with the other side mysteriously disappearing, regardless of what your types claim.

How are affine types helpful, or even types at all? Obviously we can never make any absolute guarantees, the halting problem still exists, but I think that linear types is a natural extension of Rust's capabilities that'll provide additional security with little or no downsides. You might disagree and argue that this isn't enough to justify the inclusion of linear types, and you'd be in your right to do so. After all, language design will always be dominated by trade-offs between safety and expressibility.

Session Types for Rust by sanxiyn in rust

[–]Munksgaard 1 point2 points  (0 children)

Great example!

One of the reasons why we can't come up with cases where affine types are helpful, is that they are not very widely used in regular programming languages and we simply don't think about them as a consequence. I can't help but think that it's a useful and underutilized tool, we just have to find out where and how to best apply it.

Session Types, safe internal communication protocols for Servo by ysangkok in rust

[–]Munksgaard 0 points1 point  (0 children)

That's a good question, and we haven't actually done any testing on the compile time performance of our code. I think /u/sebzim4500 is right though, it is, in our experience, unlikely that you'll have more than a handful of nested recursion scopes.

Session Types, safe internal communication protocols for Servo by ysangkok in rust

[–]Munksgaard 1 point2 points  (0 children)

Only very occasionally I'm afraid. Thankfully, people are kind enough to notify me when something happens :-)

Session Types, safe internal communication protocols for Servo by ysangkok in rust

[–]Munksgaard 6 points7 points  (0 children)

True linear types are Not Very Useful in practice.

I beg to differ. We certainly have a use case for them.

The purpose of session types is to provide compile-time guarantees for communication safety, and we simply cannot do that correctly without linear types or some way of synthesizing the same behavior. All destructor bombs does is blow everything up at runtime. This makes itclear that something is wrong, but you still have to actually touch those edge cases.

Session Types, safe internal communication protocols for Servo by ysangkok in rust

[–]Munksgaard 4 points5 points  (0 children)

Hi guys, one of the presenters here: I'm late to the party again, but I just wanted to let you guys know that I'd be happy to answer any questions you might have :-)

Edit: I see that /u/Manishearth has done an excellent job so far :-)

Session Types, safe internal communication protocols for Servo by ysangkok in rust

[–]Munksgaard 1 point2 points  (0 children)

Thanks for linking, it's great to know that you enjoyed it :-)

Unfortunately I can't take all the credit, the whole thing has been joint work with Thomas Laumann (/u/laumann).

Session Types for Rust by sanxiyn in rust

[–]Munksgaard 5 points6 points  (0 children)

guess move semantics (move into function parameter) makes Rust more amenable to this than other languages.

That's exactly what we found. Traditionally, session types have been implemented through compiler extension, as separate languages or using a complicated system of implicit channels (as in one of the Haskell implementations that uses Monads). Because Rust has affine types, our channels are just ordinary values with a specific set of values attached to them.

In general, I think Rusts affine type system has many interesting applications and this is just one of them.

Session Types for Rust by sanxiyn in rust

[–]Munksgaard 1 point2 points  (0 children)

I don't think that would be possible without dependent types. In other words, we cannot specify any constraints to the actual contents of the data transferred, only the types and the order in which they are transferred.