#idris2 — Public Fediverse posts

building pack...

#idris2

@[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...