#idris2 — Public Fediverse posts

@[email protected] considering getting back to #Idris2 for my first #AdventOfCode. I mostly use #Agda nowadays

Readings shared September 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/20-readings_shared_09-19-25 #Agda #CoqProver #ITP #Idris2 #LeanProver #Rocq

Theorem provers: One size fits all? ~ Harrison Oates, Hyeonggeun Yun, Nikhila Gurusinghe. https://arxiv.org/abs/2509.15015 #ITP #CoqProver #Idris2

Did this manic 20 slide lightning talk reimplementing part of @ParslProject using #Rust #Idris2 #Elixir

https://parsl-project.org/parslfest/2025/benc-3lang-interchange.pdf

valgrinding the #idris2 ffi again when i should really be making slides

@benc

#idris2 felt less polished|stable than #idris 1 .
& with non-unix builds.
& with IDE support.

Idris2 forced me to compile, install, learn nvim (neovim), to just get IDE features that were available 10 years ago in idris1 VSCode plugin.

i was actually hoping to get #idris2 C backend working because I thought i might get nicer valgrind stack traces out than out of the scheme backend.

I fixed up holes (which wouldn't compile) and now I get FFI missing headers for my own libraries.

So back to the scheme version. which doesn't run properly in this debian inside valgrind unless I set some path, which might be a scheme bug from years ago not yet propagated.

teenage fun.

I owe a lot to a few programming languages that taught me how to design a language, both from an engineering standpoint and computer science.

#Lisp & #haskell for what a good programming language might look like.

#Agda, #Idris2, #lean4 to show me how useful dependent types are.

#C++, to teach me what to avoid

#python, #javascript to be such giant examples of shitty languages and give me hope that I can do better. 😂

#Idris2 is one of the languages that I consider to be superb. Unfortunately, though, it's tooling is not great, but that can change in the future.

#Idris2 is, definitely, one of the best langs out there. Alas, the environment is not mature yet. But I like it regardless. Among languages with dependent types, it is the most practical one for a software engineer.
I use #agda and #lean as well. However, Idris2 is something else.

rebuilt to a recent version of #Idris2 and now I'm getting an error Control.App.(>>) not existing -- it's not the upgrade breakage I was expecting...

#idris2 compiles to scheme, right?

chez scheme IIRC.

I wonder what a port to #guile would look like.

off on a little sidetrack wondering if I could get the #idris2 C backend going, but it doesn't like holes, so then down a 2nd-order sidetrack wondering if I could implement holes in that code generator (I could not, at least not in lazytime).

this is because i want the stack traces coming out of valgrind to be a bit more meaningful than "somewhere inside chezscheme", and the generated C code looks great for that.

so i will have to go write my program properly.

i am enjoying trying to use linear types in #Idris2 to actually do something, and i have only patched the source code once

does #Idris (#Idris2) have a named record constructor syntax? like this?

```
example = Person{ name = "John Doe", admin = True }
```

Reached the point in my #idris2 Pickle decoder that I should implement equality of Python objects but instead I'll rely on the encoder never sending a set with duplicates. (This is for keys of Python dicts where it looks like there's no protocol requirement that dictionary keys be unique in the pickle even though it would be pretty much a fancy no-op - because it does define how one overrides another)

( #JSON doesn't have that requirement either and doesn't define a meaning for duplicates)

@dysfun @BoydStephenSmithJr #neovim #vim

I really am! Nvim-lspconfig supports #idris2-lsp out of the box, and @edwinb's [plugin](https://github.com/edwinb/idris2-vim) is a nice integration to that. It's a neat setup.

Reimplementing parts of @ParslProject in #Idris2 for "fun" has stirred up my language-brain enough to realise there is probably also some fun to be had for "serious" using Python async (but not in the asyncio sense) there too... So will now use some paid time to fuck around with that...

Working on my #idris2 reimpl of part of @ParslProject today but I am still doing a bunch of C interfacing so actually I'm getting mad at all my C coding errors that would have been caught by ... using a language with a nice type system

did a bit of poking at reimplementing one component of @ParslProject in #Elixir (also in #Rust and #Idris2) - for "professional development" rather than to achieve something maintainable...

this component interfaces to other bits with ZMQ and I got a bit frustrated trying to figure out the best way to be dealing with messages to/from both ZMQ and Erlang processes...

a replay of what I've seen a few times of "I want poll, but I want poll on multiple peoples messaging systems".

@dysfun

Collected [here](https://github.com/lucat1/visimp/issues/58) my ideas to integrate #idris2 support in my @neovim setup (currently on #visimp).

There's a #lsp server, a #treesitter grammar, and a third misc plugin written in #lua.

@dysfun

Collected [here](https://github.com/lucat1/visimp/issues/58) my ideas to integrate #idris2 support in my @neovim setup (currently on #visimp).

There's a #lsp server, a #treesitter grammar, and a third misc plugin written in #lua.

@dysfun

Collected [here](https://github.com/lucat1/visimp/issues/58) my ideas to integrate #idris2 support in my @neovim setup (currently on #visimp).

There's a #lsp server, a #treesitter grammar, and a third misc plugin written in #lua.

@dysfun

Collected [here](https://github.com/lucat1/visimp/issues/58) my ideas to integrate #idris2 support in my @neovim setup (currently on #visimp).

There's a #lsp server, a #treesitter grammar, and a third misc plugin written in #lua.

@dysfun

Collected [here](https://github.com/lucat1/visimp/issues/58) my ideas to integrate #idris2 support in my @neovim setup (currently on #visimp).

There's a #lsp server, a #treesitter grammar, and a third misc plugin written in #lua.

One of the fundamental errors of our moment is the idea that #programming is primarily a scientific activity. Its important that we remind ourselves that it is truly more art than #science in order to assume an antagonistic distance from those who presume to speak from positions of scientific objectivity while equating the scientific production of knowlege with what is in actuality commodity production.

This assumed equality of the incentives of commodity production & science is precisely the ideology of #ElonMusk & #tech billionaires. Its the same ideology that dominates a moment in history characterized by total neglect towards threats of existential proportions, where we sail head first towards the worst of possible worlds, not out of necessity, but due to the absolute greed and nihilism of those with wealth and power. I have no doubt that if every decent #hacker were given control of our time & provided the resources we need, we could autonomously and adaptively solve the climate crisis, rather than waste away creating meaningless webapps that are the result of the galaxy brained thought experiments of reactionary dude-bros at #vc incubators. But not its bcs we're scientific, although we employ cutting edge science as means to ends; no, its rather
because we're crafty.

As hackers, you are rarely either scientists or engineers, but rather writers producing some of the most novel writing of your time, a truly new writing uniquely suited to collaboration; writing that allows wordsmiths to amass infrastructure from mere letters & words, granted adequate time. You're not engineers, but artists alienated under capital. #Haskell & #Agda programmers are not mathematicians, but rather poets among mathematics. Despite claims that Haskell shines in authoring compilers, the move of #Idris2 & #Unison to #Scheme suggests that type theory is perhaps too constraining for long term compiler development. Typed functional programming is writing in a constrained style -- poetry amongst programs -- programs that get down to the rithm of #formalism. Haskell isnt for writing programs like Idris2, but rather for those like #TidalCycles. Its simply that our idiom discourages creativity, so we play along to survive.

#WalterBenjamin described circumstances such as ours as "the aestheticization of politics", which was, according to him, the only trait to distinguish fascism from capitalism. Our only hope would be for the text workers of the world to unite.

Scheme Workshop Keynote: Edwin Brady - https://www.youtube.com/watch?v=h9YAOaBWuIk&list=PLyrlk8Xaylp4pcRhsuZ0gEOmggCOd8GBz&index=10&t=0s

#idris #idris2 #blodwen #functionalProgramming #fp #chezScheme #scheme