Two things I learned from this:

  1. If you write objects with values encoded at both runtime and compile time, you can use type classes to guide Idris through induction on them rather than having to reimplement it as proof code. Not only that, but the compiler can act as a better proof assistant by letting you know exactly what implementations are required and which ones are missing. That helped a lot.
  2. Encoding data in type level lists that can mutate is hard, but it’s actually not the hardest thing I’ve tried to do in idris. …

A perennial source of angst for me is dealing with plans and deadlines in software. While there are many takes on this from #NoEstimates to good old blame, it’s a common experience that neither the people making the estimates, nor those receiving them are making any use of the information, instead allowing it to become a waste stream with no outlet that slowly toxifies relationships, becoming its own justification and justifying pressure that very often is strictly self imposed.

I’m going to expand here on a basic idea from here

An experience most people who have worked for medium…

Hot take: has made ← a simple static build of libclang that allows you to bust your libtooling and other clang related code out of llvm build tree jail and api version hell.

One of my previous lives involved writing a lot of C++ and I became very opinionated on some practices in C++. For larger programs, I tended toward a java style that put an abstract base (ISomeObject) when appropriate in front of objects conferring nontrivial functionality (network protocol clients, db adapters, even coupling to the filesystem) and so wrote a tool that helped enforce these kinds…

I’ve been deep diving idris for a while, and the way certain dependently typed structures change type over time has been something I haven’t had a great handle on. I have a tutorial on the ST monad coming, but I’d like to first talk about the way (as I understand it) idris’ dependent types apply to monads which we mutate (at least conceptually) through the flow of imperative-like code.


For lack of better ways of stating it, I’m going to use the terminology used in pursecript and think of the effect list as a collection of independent row…

I had something on my mind earlier and admittedly i wasted precisely 37 minutes just now advancing a proof target I’m working on.

I’d had trouble with proofs like “a < b implies f a b = []” for some a and b. The problem comes when you case split and have to contend with (S a) and Z (for example) as values. You know this is impossible, but how to dismiss these proof targets?

Consider this:

lteMagnitudeObvIsImpossible : (b : Nat) -> (v : Bin) -> LTE (magnitude (O b v)) 0 -> Void lteMagnitudeObvIsImpossible Z v = succNotLTEzero…

Recently, in order to give a coworker an easier way to interact with some code we deliver as javascript, I ported something from bucklescript to fable so that it’d be visible in a .net IDE. Admittedly, the result is pretty swank. Since F# branched from ocaml linguistically, it wasn’t a huge effort (roughly 1 full day of work), but something interesting happened running the resulting javascript on nashorn (note, a late addition here is that I notice that this is mainly due to the es5ification from babel).

Constructing unions in F# would sometimes work and sometimes not, whereas the code…

I’ve been working through a formal proof of a BTree implementation in small amounts of spare time in Idris, and both getting better at working with proofs and discovering new parallels between the imperative and functional universe. In this case, I’m going to detail how I think about proofs of imperative code in Idris.

Last time I wrote, I had come up with what amounts to a Free monad that could be used to simulate imperative systems, and therefore expose those systems to the mercy of requirements to prove things.

As an aside, one reason I write these is that…

I’ve been thinking and working a lot on some code, and stealing tiny amounts of time here and there thinking about and trying out Idris with regard to helping with some real code. In this case, some Kotlin code that implements an offline BTree. It is necessary to use a side-effecting external store for this both because the size of the tree can be considered to be infinite over a long time, and also because RAM is at a bit of a premium.

I’ve written pretty good tests, so I’m confident that the code is mostly correct, and the tests…

I’m not very bright, but even I was able to get a bit comfortable with proofs. Here are my notes on actually using the Idris type system to prove things. Next time I’ll write about how I think proofs fit practically in software development after exploring minikanren last year and compare them both to traditional unit testing. I’m still a noob at this, so those experienced might want to avert their eyes. …

Although no google results ever turned it up, there’s a pdf with a lot of proof related exercises in idris:

This comment on a tragically uninformed post by me on reddit explains the use of the contra argument to DecEq’s No constructor well, as well as introducing the above pdf. Hopefully dropping it on medium will make this stuff more visible.

Also don’t do what I tried to do :-)

art yerkes

An old programmer learning new tricks.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store