Sometimes you have disjoint but covering class instances for a type in idris. TLDR: you can use idris’ proof language and the curry-howard correspondence to both statically bind the instances and prove that disjoint class instance types are total in the same way that writing a total function is a self evident proof of its own totality.
module Mainimport System
import Data.Bool
import Decidable.EqualityisEven : Nat -> Bool
isEven Z = True
isEven (S Z) = False
isEven (S (S x)) = isEven xdata EvenOrOddNumber : (n : Nat) -> (b : Bool) -> Type where…
why things are kind of awful and perhaps a way toward away from awfulness
tldr; Often, we’re working to a deadline that should be a “delivery timebox”, and our narrow focus on “outcomes” often blinds us to the ways we can get more smarter without breaking everything.
My theses:
- We assign deadlines because we’re worried we won’t get some more distant need serviced in time.
- We prioritize in a style that’s conceptually too strict and too coarse grained in time, which forces us to make everything “high priority”. When everything is high priority, nothing is.
- The soft work people often…
I wanted alists with guaranteed unique values, and finally decided to sit down and work out how this functions in idris. For those not as old as dirt, an alist in lisp is a list of pairs where the (car) of each is considered to be the key, so it functions like Dict or Map in most languages (functions like assoc and mem in lisp act on these). …
Two things I learned from this:
- 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.
- 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
https://twitter.com/prozacchiwawa/status/1302394289800933376
An experience most people who have worked for medium…
Hot take: https://twitter.com/deech/ has made https://github.com/deech/libclang-static-build ← 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.
Example: https://github.com/prozacchiwawa/idris-effect-example/blob/master/Artyssert/Assert.idr
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 =…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…
art yerkes
An old programmer learning new tricks.
