Відео

could u tell me how to install Idris2-lsp(used for vscode) on windows?

just tell me how to install it natively....

Now it just needs an Ecto like thing to talk to Postgres! Or something more clever, of course

Yeah, I guess this is the path of least resistance for Win 10. If you have a chance to make a video for the Docker approach (from setup to running), that would be very useful.

Very cool! If you add codata & coinductive reasoning, you also can model stateful and other nice stuff, like objects, infinite lambda-calculi, and fixed-point algorithms :)

"Promo sm"

I hate Idris

I do wonder how this'd adapt once you move from a global server state towards something more "realistic" involving a database.

I think I am missing something here. You are splitting a string of length N into two parts of length N/2, then insert a bar, resulting in a string of length N+1. So how can you possibly mutate the buffer inplace, since it is too small? In the C example the buffer has length 32 so that happens to work for this specific example, but in general, it won't work, and cause of buffer overrun? Maybe it was more like a theoretical example?

21:34 great visualization of Lens type and their meaning. First time seeing it.

This is great, there should be one for Mac and Linux too 😀

5:37 the brackets are so faint that I almost thought there is a new syntax

Great talk! It would be nice if I get familiar with the server symbols (like slashes and :|:) defined in the lens module beforehand. Where do you recommend us to look at?

static reference counter? :)

Thanks for your talk! This is the first time I see linear types in a talk. Thanks for clarifying the difference bweteen linear types and quantitative type theory (yes, I watched every Idris2 video I could find). Your example and the open questions in the field reminded me a lot of how things are done in the programming language Rust. Have you by any chance had a look at it? If you did, how would you describe the gap between Rust (which is used in production) and the current state of the art in linear types research (which is what you are doing)?

Nice talk. Just curious as to whether you might have looked at the Formality language much (also Cedille / Juvix to some extent) and if you had any thoughts on it? It appears to be a reasonable attempt to build a performant proof language. I’d also be interested to hear what you think of their claim of “No Garbage Collection”. The language appears to be based on affine lambdas and I’m very keen to find out what the programming experience would be like writing large-ish programs using only those.