In the #idris stdlib, Control.Relation.Closure.TransClosure.(::) captures the intermediate index/element as a relevant, but implicit argument.

My approach https://gitlab.com/bss03/type-aligned/-/blob/main/src/Type_aligned.idr?ref_type=heads#L94 erases the indexes/elements.

The definitions of `transitive` and `reflexive` from the stdlib also require relevant (but implicit) index arguments ... which means those stdlib interfaces don't really mesh well with my library.

But! It _is_ possible to implement versions of transitive that takes ERASED (and irrelevant) index arguments for both/all relations in the stdlib. That means keeping the indexes around at runtime is wasteful at least _sometimes_.

And! Some relations allow you to derive one or both indexes from the value. The stdlib LTE allows you to recover the first index (lesser number) from it's structure, so there's some sense that saving the index for that is redundant (or a premature optimization, at least).

It's clear the stdlib authors of those modules did know about erasure and chose to use it in some cases. Can anyone reveal reasoning behind those decisions, or point me to a set of guidelines for making my own decisions?

In any case, I need to figure out some way to test what I have, or start the re-write toward relevancy.

#idris experts, is there a reasonable way to write a single `Show` implementation for a type like:
```idris
public export
data Sum : (0 p, q : a -> a -> Type) -> a -> a -> Type where
Left : {0 p : a -> a -> Type} -> p x y -> Sum p q x y
Right : {0 q : a -> a -> Type} -> q x y -> Sum p q x y
```

I'm pretty sure I can do it in GHC, but it would require some extensions.

If not, is there a way to do zero-cost wrapper types (like Haskell `newtype`) so that I can write 3-4 implementations for the specific ways I'm using this sum?

QQ: Is it a good sign or a bad sign when they type of one of your hole doesn't fit on (one screen of) your terminal?

#idris

#Idris erasure experts why does this work:
```
0 Equal0 : (0 x : a) -> (0 y : b) -> Type
Equal0 x y = Equal x y
```

But, I can't pass `Equal` into a `(0 p : (0 x, y : a) -> Type)` parameter to a function/type?

In general, I'm not sure when I should be aggressive about erasing parameters (or indexes!) that _might_ be types.

For example, when dealing with encoding nested or recursive data structures as fixed-points of functor( familie)s I can use certain folding functions both to create types AND to create non-type values, and there are standard functions that make for fine types when invokes correctly (e.g. `const Unit`).

Right now, I'm doing type-aligned sequences (for "reflection without remorse" on proofs in the form of transitive [or transitive+reflexive] closures of relations) so I think erasure might not be what I want but it works so far, and thinking about it up front seems "easier". Trying to add erasure/linearity later tends to result in cascading error messages that I get tangled in.

`Can't solve constraint between: uncurry Snoc cgvArgs and Snoc (fst cgvArgs) (snd cgvArgs)`

This feels wrong. `uncurry` (either version) is `public export` from the stdlib, so it should expand.

#idris

Hey, #idris people, is there a well-known (to someone not me) reason why (automatically generated) record accessors aren't linear in their record argument?

In particular, it feels like fst (both for Pair and DPair) and snd (at least for Pair) should be linear but they aren't so I needed:
```idris
public export
fst1d : {0 p : a -> Type} -> (1 _ : (x : a ** p x)) -> a
fst1d (x ** _) = x

public export
fst1 : (1 _ : (a, b)) -> a
fst1 (x, _) = x

public export
snd1 : (1 _ : (a, b)) -> b
snd1 (_, y) = y
```

For a bit the compiler seemed to be accepting local `let` assignments to do the same thing, but once I started overloading the names (of the functions containing said lets) too much, I found it easier to write these functions instead of switch to local `case` blocks (or `with` stuff).
?

I'm not confident it's good enough to go into any standard library, but these are the most refined versions of the dependent equality for #idris I have:

```
public export
0 Equal1 : a -> (0 _ : Equal a b) -> b -> Type
Equal1 x Refl y = Equal x y

public export
sym1 : (0 _ : Equal1 x eqt y) -> Equal1 y (sym eqt) x
sym1 {eqt=Refl} = sym

public export
trans1 : (0 _ : Equal1 x eqtl y) -> (0 _ : Equal1 y eqtr z) -> Equal1 x (trans eqtl eqtr) z
trans1 {eqtl=Refl} xy {eqtr=Refl} yz = trans xy yz

public export
coerceEqual1 : (1 _ : Equal1 x eqti y) -> (0 eqto : a = b) -> Equal1 x eqto y
coerceEqual1 {eqti=Refl} eq1 Refl = eq1

||| Adapted from https://martinescardo.github.io/dependent-equality-lecture/DependentEquality.html
public export
0 EqualI : (0 f : i -> Type) -> f a -> (0 _ : Equal a b) -> f b -> Type
EqualI f x eqi y = Equal1 x (cong f eqi) y

public export
congi :
(0 g : i -> i) -> (0 fun : (x : i) -> f x -> f (g x)) ->
EqualI f x p y -> EqualI f (fun a x) (cong g p) (fun b y)
congi _ _ {p=Refl} Refl = Refl

public export
coerceEqualI : (1 _ : EqualI f x p y) -> (0 q : a = b) -> EqualI f x q y
coerceEqualI eqi q = coerceEqual1 eqi (cong f q)
```

The fact that I have to use coerceEqualI a couple of times is, I think, reflective that idris stdlib has non-reducing equality proofs that I use, but could be a problem with the above.

Current Status: Pairs / uncurrying and linearity are harshing the vibe in my #idris code.

Is there a simple way to "sample" a #idris #hedgehog `Gen`erator to see what kinds of values it might output?

I wrote the generator, so I have some idea, but I find it comforting to see some of the values.

I probably should be using `classify` / `collect` / `cover` too, but it's not easy to figure out the right groupings for heap / contexts other than size, and since I'm just getting the size from a provided generator, I think that coverage will be fine.

So many more steps to go, but I think I might have gotten comfortable enough with the #idris syntax and type system to get to where I want to do.

I have code that generates CEK machine states with a specific term head, with the heap being well-typed and the term being well-scoped (unnamed, DeBruijn indexed). Terms are very simple for now, though, but it's nice to be able to start doing property-based testing, instead of just "golden" testing.

A few #idris equalities:

```idris
public export
complementFZ : (n : Nat) -> finToNat (complement (the (Fin (S n)) FZ)) = n
complementFZ Z = Refl
complementFZ (S p) = cong S (complementFZ p)

public export
weakenNatEq : (x : Fin n) -> finToNat (weaken x) = finToNat x
weakenNatEq FZ = Refl
weakenNatEq (FS fp) = cong S (weakenNatEq fp)

public export
complementFS : {n : Nat} -> (x : Fin n) -> finToNat (complement (FS x)) = finToNat (complement x)
complementFS FZ = weakenNatEq _
complementFS (FS _) = weakenNatEq _
```

Do these already exist (modulo naming) in base or contrib? I couldn't find them. If not, are any of them worth opening a PR against contrib (or base?).

I'm using `finToNat (complement x)` as the length of the remaining / interesting part of a context-like thing when inspecting extracting the DeBruijn index `x`.

Hey, any #idris or #agda people also see that "simple trick" for carrying around the index equalities necessary for a hetrogenous equality?

EDIT (found it!): https://martinescardo.github.io/dependent-equality-lecture/DependentEquality.html

Like, the equality proof I'm building is something like [not real syntax] (x : RVect n Mine) = (y : RVect (n + 0) Mine).

Trying to pattern-match on the recursive proof directly is a K-axoim violation (IIRC), and in any case it's making the type checker unhappy (for, reasons I am _sure_ are good). Trying to apply cong / depCong to the recursive proofs is a type mismatch.

I think it was "as simple" as having as carrying around the equality proof on indexes (?) and I think the presentation I saw also used mixfix to make the syntax look quite nice.

I might be able to recapitulate it myself, but it would be easier and better to just crib from my betters.

Idris for the Atari ST also runs on the MiSteryNano, a reimplementation of the ST on a 30€ Tang Nano 20k FPGA board. Here's a screenshot of the X10 (not a typo!) window system running in glorious 640x400 mono resolution on a modern HDMI LCD. We initially had some trouble running Idris in the Hatari emulator, but on the FPGA everything works right away!

https://github.com/MiSTle-Dev/MiSTeryNano
https://github.com/9nut/IDRIS-OS-for-Atari-ST
https://virtuallyfun.com/2025/12/31/whitesmiths-idris-os-for-atari-st-virtualized/
https://wiki.sipeed.com/hardware/en/tang/tang-nano-20k/nano-20k.html

#retrocomputing #fpga #atarist #idris

Build times in #idris are frequently fairly long, and I can certainly understand why. But, does anyone have experience (or better benchmarks) that would indicate whether I should use #ShezScheme or #Racket as the backend for low compilation times?

I've got both easily available through the Debian repositories and both seem to work, but I'm using them on such different systems that my experience isn't enough to compare.backends.

In #Idris can you have mutual recursion between types that are in separate namespaces?

One of the constructors for my WF type takes an argument of the Ty type, and most of the constructors from Ty take an argument of the WF type. A mutual block or some forward-declarations would work fine if they were in the same namespace.

But, I want WF and Ty to be in their own namespaces, because I want to reuse constructor names (between Ty and Tm and between WF, Ctx, and others) but I still want the "fully-qualfiedi" constructor names to be unambiguous and something I can write in the surface language, if needed.

Naming things is hard.

Current status: compiling #idris

Advent of Code 2025 in Lean 4, day 4: https://hamberg.no/erlend/posts/2025-12-04-aoc-2025-day4.html

“Fuel for the termination checker!” – in which I get to apply a method I learned from @edwinb's book on #Idris.

#AdventOfCode #Lean4

New pre-print out: "Types, equations, dimensions and the Pi theorem".

We formalized the covariance principle (physical laws must be independent of units) as a homomorphism between the algebra of physical quantities and real numbers.

While the Pi Theorem from Dimensional Analysis (DA) is non-constructive, we introduce a constructive method for applying it. This could enable DA-driven program derivation where the type checker helps identify valid physical laws.

📝 Blog: https://patrikja.owlstown.net/posts/4887
📄 Paper: https://arxiv.org/abs/2308.09481
💻 Repo: https://gitlab.pik-potsdam.de/botta/papers/-/tree/master/2023.Types,%20equations,%20dimensions%20and%20the%20Pi%20theorem

#Idris #Agda #TypeTheory #Math #Physics

@Alonely0 @hackernoon If one wants a modern language a la generics (i.e. not a computer abstraction), I would say that #Idris or some other "new" dependently typed language is the future. But C++ will probably incorporate real dependent types or first class types, before any of those languages go mainstream (if it hasn't already).

The Start of a new Org? - Air Traffic Control on the Idris - Star Citizen
https://youtube.com/watch?v=m7mUnQnJBGg&si=IMjbwCMPK2Qjki03

#citizenKateAndWill #StarCitizen #RobertsSpaceIndustries #CloudImperiumGames #SpaceGame #PCGaming #NewOrg #idris #airtrafficcontrol #Gameplay