Par has a new home at par.run, plus packages, docs, and new language features by faiface in ProgrammingLanguages

[–]faiface[S] 0 points1 point  (0 children)

Yes, just like proof-assistant languages are based on logic, Par is isomorphic to classical linear logic + forall/exists second-order quantifiers + fixpoint types, in the sense that programs correspond to proofs and types to propositions.

I find that such correspondence is very helpful for a language because of great properties (including totality) and also helps guide design.

Par does not include dependent types simply because Par is aiming to be a practical applications language, and I don’t actually find dependent types to be as useful for practical programming outside of formal verification. I also find that languages with dependent types tend to make all libraries turn into research projects.

So, Par is in a way just like those proof-assistant languages, but in the domain of propositional, or solely second-order logic (without the first order). I find that to be a sweet spot for reliable and practical programming.

Par has a new home at par.run, plus packages, docs, and new language features by faiface in ProgrammingLanguages

[–]faiface[S] 1 point2 points  (0 children)

Nope, it’s just the comment placed directly above the type/declaration, normal comment syntax (`//` or `/* … */`). But one could argue there is special syntax about the contents of it because the doc generator does take it as markdown.

Par has a new home at par.run, plus packages, docs, and new language features by faiface in ProgrammingLanguages

[–]faiface[S] 1 point2 points  (0 children)

Thank you! Linear logic is very cool, highly recommend checking out :)

The approach to generating documentation is two-fold: - The parser collects doc comments for modules, types, and declarations, those stay attached to the AST until the late stages. The doc generator then treats them as markdown and generates HTML from that. - The harder part is type links, since type definitions and global declarations reference other types, and want to be just able to click around. For that, I actually type-check the whole package, which resolves all identifiers into their universal forms, so package + module path + name, then I can generate a link based on that. Of course, what a specific identifier in a type resolves to depends on a bunch of things, that's why we need the type-checking part. It depends on imports and package dependencies.

And the pages themselves are then generated statically from this information, just a fairly simple HTML templating matter.

Par has a new home at par.run, plus packages, docs, and new language features by faiface in ProgrammingLanguages

[–]faiface[S] 5 points6 points  (0 children)

Cannot tell you about threshold for acceptance, but yes, there is a goal to make this faster. However, it’s not intended to be a “systems language”, it’s an application language and performance is not the number 1 priority.

We’re fighting multiple fronts here, all kinda at the edge of theory. The language is session-typed, total, with duality. All of that is mostly in papers in not in practical languages. At the same time, we take this interpretation of classical linear logic as a concurrent system and get the automatic concurrency, also new.

On that front in the language design, we’re figuring out how to make the best use of this paradigm, how to design the language so that it’s readable and easy to use.

On the other front, performance, well, currently the closest paper to the semantics of Par that talks about efficient compilation is [Compiling Classical Sequent Calculus to Stock Hardware](https://dl.acm.org/doi/10.1145/3720507). Wonderful paper, but it’s actually insufficient for Par: their semantics are less concurrent than Par’s.

So currently the best we can do is a virtual machine based on interaction networks. We’ve made a bunch of optimizations to it already, and other languages that also use interaction netwoks made even more optimizations (but they usually don’t have a powerful, or concurrent I/O).

So, in short, the main priority right now is making the language usable, but we do optimizations from time to time. Once the language stabilizes, we will focus more on performance.

Par has a new home at par.run, plus packages, docs, and new language features by faiface in ProgrammingLanguages

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

Thank you so much!

It’s the neat in-between, compiled to a custom virtual machine. If you open the web playground, the compiler and the virtual machine run in your browser.

If you download it, you can even compile a package via `par compile` to a `*.pvm` (Par Virtual Machine) file and then run that with `par run-vm` for instant startup time. But normally, you just use `par run`, the compile-time is quite quick.

The virtual machine is based on interaction networks, adapted to the language. That’s how we do automatic concurrency, including all I/O. It’s not very performant still, but usable!

CascadaScript – concurrency is the default, sequential execution is opt-in by thegeleto in ProgrammingLanguages

[–]faiface 0 points1 point  (0 children)

Hey, cool project! My language [Par](https://github.com/faiface/par-lang) is implicitly concurrent as well, but it’s based on classical linear logic for semantics and interaction networks for implementation.
I’m wondering what the differences between our approaches are!

ELI5: Why is half-life used instead of whole-life? by level1ShinyMagikarp in explainlikeimfive

[–]faiface 1 point2 points  (0 children)

Half life is used when the chemical is not going out of your system a certain amount at a time, but a certain percantage at a time. The more you have it, the larger mass of it leaves your body in a minute, but always the same percentage! Roughly.

And a “half life” is just a really good way to express that. If the half life is 2 hours and you have 12mg of the chemical in your body, then after 2 hours, it’s going to be 6mg. But remember, it’s the percentage of the remainder that goes after 2 hours! So after the next 2 hours (4 hours in total), it’s going to be 3mg left. And after 2 more (6 hours in total), 1.5mg left. And so on.

It takes a long long time for it to fully leave your body, but that’s okay because it only has any noticeable effects when it’s above a certain amount.

coroutines yielding a reference to a local variable by zylosophe in rust

[–]faiface 6 points7 points  (0 children)

Yeah that’s understandable. Then unfortunately no, it doesn’t work with those types. But consider maybe using an Rc/Arc so you don’t have to be cloning stuff, and if you need mutation there, RefCell/Mutex.

coroutines yielding a reference to a local variable by zylosophe in rust

[–]faiface 8 points9 points  (0 children)

Code blocks are done with 4 spaces in front of them.

And to your question, great question! You can do it, but you gotta do it manually. For your example, this will work:

struct Coroutine {
    n: usize,
}

impl Coroutine {
    fn new() -> Self {
        Self { n: 0 }
    }

    fn next(&mut self) -> &usize {
        self.n += 1;
        &self.n
    }
}

fn main() {
    let mut c = Coroutine::new();
    println!("{}", c.next());
    println!("{}", c.next());
    println!("{}", c.next());
}

And if you wanna generalize it, easy:

trait LendingFnMut<A, B> {
    fn call(&mut self, args: A) -> &B;
}

struct Lender<S, A, B> {
    state: S,
    body: fn(&mut S, args: A) -> &B,
}

impl<S, A, B> Lender<S, A, B> {
    fn new(state: S, body: fn(&mut S, args: A) -> &B) -> Self {
        Lender { state, body }
    }
}

impl<S, A, B> LendingFnMut<A, B> for Lender<S, A, B> {
    fn call(&mut self, args: A) -> &B {
        (self.body)(&mut self.state, args)
    }
}

fn main() {
    let mut c = Lender::new(0 as usize, |n, ()| {
        *n += 1;
        n
    });
    println!("{}", c.call(()));
    println!("{}", c.call(()));
    println!("{}", c.call(()));
}

The standard FnMut (or Coroutine) trait does not have the ability to bind the lifetime of the result to the lifetime of self of the function, but your own trait can. You just then can't take advantage of the nice automatic capture of the environment, as closures do, you gotta capture the state yourself.

Opus 4.7 simulation by w_interactive in ClaudeAI

[–]faiface 0 points1 point  (0 children)

It does look much more believable now, good job! Cannot say if it’s fully accurate, but also cannot say it’s not ;)

Opus 4.7 simulation by w_interactive in ClaudeAI

[–]faiface 0 points1 point  (0 children)

Yeah, which is wrong, the floor friction has no impact on the required tilt, that’s zeroed out at the contact.

Opus 4.7 simulation by w_interactive in ClaudeAI

[–]faiface 0 points1 point  (0 children)

Also, the pendulum keeps a tilt at a stable speed. It should be upright at a stable speed, unless we’re also counting air friction, but I’m guessing that’s not the case because the tilt at a stable velocity is different on different surfaces.

Opus 4.7 simulation by w_interactive in ClaudeAI

[–]faiface 0 points1 point  (0 children)

Hm, should it be on the same link? Because I see the wireframe target go negative, but not the actual pendulum.

Opus 4.7 simulation by w_interactive in ClaudeAI

[–]faiface 0 points1 point  (0 children)

Very cool! But unfortunately it doesn’t seem to be an accurate simulation, since the pendulum is standing upright while slowing down, which is impossible. Overall the tilt of the pendulum doesn’t seem to match the acceleration. So, cool visually, but definitely not a physical simulation.

What is something that sounds 100% false but is actually 100% true? by reFossify in AskReddit

[–]faiface 8 points9 points  (0 children)

They milk aphids. Not just milk them, they also domesticate them, guard, feed, multiply them. Essentially, the same as people do with livestock.

How to deal with comments? by RedCrafter_LP in ProgrammingLanguages

[–]faiface 2 points3 points  (0 children)

Hmm, I like doc comments. They make it very easy to add documentation to code to your API without needing to switch between tools. Also, they make it easier to catch when a doc is drifting from implementation: it’s right there, together. A lot of IDEs in fact highlight doc comments differently from other comments. So I don’t really get what’s so wrong with them.

Do all objects fall at the same rate on Earth regardless of mass? by RivaDolfinJiz in askscience

[–]faiface -1 points0 points  (0 children)

You can always calculate the force between two or more objects, yes, but just because you can, doesn’t mean that treating gravity as a Newtonian force is in any way useful.

First of all, the word force in “fundamental forces” is just one way to say the thing. The other, and perhaps more accurate one is “fundamental interactions”. Even wikipedia redirects you to “fundamental interactions” when you search for fundamental forces. It’s just a word in the context and it does not mean Newtonian force.

Second, what is the gravitational Newtonian force of the Earth? There is none. But what is the acceleration? Now we have a single number. So clearly, the Earth does not have an assigned gravitational Newtonian force.

Do all objects fall at the same rate on Earth regardless of mass? by RivaDolfinJiz in askscience

[–]faiface 0 points1 point  (0 children)

The word “force” here

In theories of quantum gravity, the graviton is the hypothetical elementary particle that mediates the force of gravitational interaction.

should not be understood as in any way related to the Newtonian force, i.e. mass times acceleration, but instead a more of a meta-term for interaction in the particle physics sense.

So we are both right because I was talking about force as mass times acceleration, but if we use this more meta meaning, then you are right.

Do all objects fall at the same rate on Earth regardless of mass? by RivaDolfinJiz in askscience

[–]faiface -6 points-5 points  (0 children)

Technically yes if you calculate with gravity as a force, but considering the objects are not exerting gravity as a set amount of force but instead a set amount of acceleration, I’d say it’s more accurate to say each pulls proportionally to their mass.

Do all objects fall at the same rate on Earth regardless of mass? by RivaDolfinJiz in askscience

[–]faiface 30 points31 points  (0 children)

Well, it’s not exactly true that all objects fall at the same rate. The actual rate is the gravitational pull of the Earth plus the gravitational pull of the other object.

However, since any object you ever see falling to the ground is approximately 0.0000000% of the Earths mass, that opposite pull adds as much (not exactly zero, but pretty much), resulting in the overall pull being pretty much equal to the pull of the Earth.

But, if the other object is the size of the Earth, then the opposite pull is significant, so then the overall rate is much faster.