Various wild and domesticated creatures for writing safe eDSLs in (Idris2)
First off the bat it's indexed linear monads which can eliminate a whole slew of bad programs with helpful messages from the typechecker.
Maybe we can do all the state machine stuff in QTT, so do we really need indexed monads1? But if its an eDSL we are after then the do notation is nice and then there's the Free structure etc 2.
But initially all this was inspired by Qimaera which set the agenda3 and got me to learn Idris2
So far we have a linear version of Conor's DVDDrive example from SO.
As well as the relevant interfaces in Idris2.
There were some Haskell versions using linear types as well but there's not a load of difference other than more explicit types in Idris.
Watch this space for more lolipops and zoo creatures. Not sure where this is going but it's cool enough that we can delegate even more correctness to the type checker.
Actually I'm working on some Complex number abstractions and of course Qimeara work already did proof of injectivity of wires and operators etc.
I'd like rationals with a few trancsendental constants thrown in and no need for floating point except to trivially simulate things which means some more math which may or not exist in Idris2 but proofs can be nicked/inspired from/by beautiful Agda libraries.
There's a general idea of a eDSL for linear algebra and (quantum) computation and machine learning lurking.
Might go off on another tangent if I can grok this paper on Clifford algebra based approach4.
The bait is taken and I'm looking as geometic algebra as a foundation now.
Primary References: