art yerkesModule organization in functional languagesHaving spent the past 2 1/2 years writing almost exclusively typed functional code in a variety of languages (F# and elm dominate, followed…Jun 2, 2018Jun 2, 2018
art yerkesA Quick and dirty start in idris: how to add arbitrary type restrictions in only 7 stepsMinimal type constraint in idrisJun 19, 2018Jun 19, 2018
art yerkesIdris: Software Foundations PDFAlthough no google results ever turned it up, there’s a pdf with a lot of proof related exercises in idris:Jul 14, 2018Jul 14, 2018
art yerkesBeginner Notes on proofs in IdrisI’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…Jul 20, 2018Jul 20, 2018
art yerkesProbably the worst monad example in Idris; using monads to simulate side effectsI’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…Sep 22, 2018Sep 22, 2018
art yerkesBridging your code with formal proof via monadsI’ve been working through a formal proof of a BTree implementation in small amounts of spare time in Idris, and both getting better at…Oct 27, 2018Oct 27, 2018
art yerkesByte sized idris: How to handle impossible cases.I had something on my mind earlier and admittedly i wasted precisely 37 minutes just now advancing a proof target I’m working on.Nov 13, 2018Nov 13, 2018
art yerkesEffects in Idris: how to create them and a use for them to force proofsI’ve been deep diving idris for a while, and the way certain dependently typed structures change type over time has been something I…Jan 28, 2019Jan 28, 2019
art yerkesEncoding a whole computer in a type in IdrisTwo things I learned from this:Jan 15, 2021Jan 15, 2021
art yerkesidris proofs: a tale of alists with guaranteed unique values and a bunch of miscI wanted alists with guaranteed unique values, and finally decided to sit down and work out how this functions in idris. For those not as…Apr 18, 2021Apr 18, 2021
art yerkesType classes in idris: proving away constraints and ensuring totalitySometimes you have disjoint but covering class instances for a type in idris. TLDR: you can use idris’ proof language and the curry-howard…Jun 8, 2021Jun 8, 2021
