![\"\"](\"https://cdn-images-1.medium.com/max/481/1*XRVqDYIf0Lul86s2FdgC7A.png\")
An old C++ programmer, a new functional programmer. A curmudgeon recently tiring of cynicism.
A simple modal editor for ascii diagrams featuring shift-drag line drawing and box editing.
I'm what might be called a habitual coder. I'm somewhat prolific, and I tend to write an eclectic mix of stuff depending on my interests at the time.
In another life I wrote a lot of C++ and refactored large unruly code. I came up with this:
A style enforcer for a very disciplined flavor of C++ requiring the use of interfaces and dependency injection.
I’ve been following Gabriella Gonzalez’ HasCal for a while, and decided to spend a short time trying it out. It’s a bit weird (and has some weaknesses and blindspots for now) but works pretty well and may be more tractable for those who know haskell but not TLA+. What’s there is really promising.
The whole thing is based on a monad that allows a fairly concise representation of TLA+ code in do notation. I did a quick port of the code above based on the euclid’s algorithm test example and it’s even a bit more general than my attempt at TLA+ (admittedly I don’t know the pattern for testing just a function). I don’t claim to be any kind of expert in TLA+ but I think I’ll try it a bit more in the form of HasCal as it’s very familiar syntactically. I wonder how hard it’d be to port to idris and mix with dependent types :-)
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
import Control.Monad (when)
import HasCaldata Global = Global
{ _number :: Int
, _output :: Int
} deriving (Eq, Generic, Hashable, Show)
instance Pretty Global where pretty = unsafeViaShow
makeLenses ‘’Global
testNatDivision :: IO ()
testNatDivision = do
let startingLabel = ()
let startingLocals = pure ()
let nd2 = do
while (do v <- use (global.number) ; return (v >= 2)) do
global.output += 1
global.number -= 2
let process = do
initial_n <- use (global.number)
initial_o <- use (global.output)
global.output -= initial_o
nd2
my_output <- use (global.output)
assert (initial_n `div` 2 == my_output)
model defaultOptions { debug = True } Begin {..} (pure True) do
_number <- [ 1 .. 1000 ]
_output <- [ 0 ]
return Global {..}main :: IO ()
main = do
testNatDivision
Using this method you can basically emulate any kind of computation and TLA+ allows checking of ongoing process invariants via coroutine and property members of the model. Happily, it’s very easy to get started and try it out.
I’ve been interested in proof systems and proofs for a while. Recently, I took my first tiny step (a very bad example) in TLA+:
I’ve been following Gabriella Gonzalez’ HasCal for a while, and decided to spend a short time trying it out. It’s a bit weird (and has some weaknesses and blindspots for now) but works pretty well and may be more tractable for those who know haskell but not TLA+. What’s there is really promising.
The whole thing is based on a monad that allows a fairly concise representation of TLA+ code in do notation. I did a quick port of the code above based on the euclid’s algorithm test example and it’s even a bit more general than my attempt at TLA+ (admittedly I don’t know the pattern for testing just a function). I don’t claim to be any kind of expert in TLA+ but I think I’ll try it a bit more in the form of HasCal as it’s very familiar syntactically. I wonder how hard it’d be to port to idris and mix with dependent types :-)
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
import Control.Monad (when)
import HasCaldata Global = Global
{ _number :: Int
, _output :: Int
} deriving (Eq, Generic, Hashable, Show)
instance Pretty Global where pretty = unsafeViaShow
makeLenses ‘’Global
testNatDivision :: IO ()
testNatDivision = do
let startingLabel = ()
let startingLocals = pure ()
let nd2 = do
while (do v <- use (global.number) ; return (v >= 2)) do
global.output += 1
global.number -= 2
let process = do
initial_n <- use (global.number)
initial_o <- use (global.output)
global.output -= initial_o
nd2
my_output <- use (global.output)
assert (initial_n `div` 2 == my_output)
model defaultOptions { debug = True } Begin {..} (pure True) do
_number <- [ 1 .. 1000 ]
_output <- [ 0 ]
return Global {..}main :: IO ()
main = do
testNatDivision
Using this method you can basically emulate any kind of computation and TLA+ allows checking of ongoing process invariants via coroutine and property members of the model. Happily, it’s very easy to get started and try it out.
Among the first question I asked anyone about idris was about proofs that end in having to prove that two things aren’t equal. Idris itself stops being particularly helpful in those cases, giving the weird feeling that you’re just on your own. In some cases you can provide positive proof of the opposite of the required proof and save yourself. In some cases, some rewriting gives a contradiction that idris itself is able to turn into a self evident falsehood.
I wrote a function that, for bools, inverts a proof that two things aren’t equal into a proof that the opposite of one is equal to the other, and leveraged that plenty in the idris I’ve written.
Early on I received some advice that I definitely didn’t fully understand, but came in useful as the foundation of other proof code due to being able to somewhat magically help me combine deciadable cases on a constructor with two arguments.
I’ve been working on providing proof of more properties of this object recently and I finally understand this, and can explain it hopefully in plain language that’s helpful.
My nat-like binary numbers (ugly but functional proof of interop with nat)
https://github.com/prozacchiwawa/idris-binnum:
data Bin = O Nat Bin | BNil
First let’s start with what I was given:
— Thanks: https://www.reddit.com/r/Idris/comments/8yv5fn/using_deceq_in_proofs_extracting_and_applying_the/e2e8a6l/?context=3
O_injective : (O a v = O b w) -> (a = b, v = w)
O_injective Refl = (Refl, Refl)
total aNEBMeansNotEqual : (a : Nat) -> (b : Nat) -> (v : Bin) -> Dec (a = b) -> Dec (O a v = O b v)
aNEBMeansNotEqual a b v (Yes prf) = rewrite prf in Yes Refl
aNEBMeansNotEqual a b v (No contra) =
No $ \\prf =>
let (ojAB, _) = O_injective prf in
contra ojAB
total vNEWMeansNotEqual : (v : Bin) -> (w : Bin) -> Dec (v = w) -> Dec (O Z v = O Z w)
vNEWMeansNotEqual v w (Yes prf) = rewrite prf in Yes Refl
vNEWMeansNotEqual v w (No contra) =
No $ \\prf =>
let (_, ojVW) = O_injective prf in
contra ojVW
I’d like to dissect what’s going on here and really dig into how this helps with many proof obligations one might run into on Bin (and really any constructor with multiple arguments).
O_injective is relying on idris to take a single proof step, namely that because a pairs with b and v pairs with w in a proof, then it can infer that a=b and v=w. Since the proof is a function, it conveniently returns both so we can destructure them. Without this, we’d need to use contradictions and either ‘with’ rules or induction to prove them.
The following decision rules follow from this, using the indicated destructured part of the proof to refute the clause with the given contradiction (either the shift or the tail), giving us an easy way to turn a decision about inequality in one part of the constructor to a decision about equality in the constructor as a whole.
It didn’t occur to me at the time why the function is called ‘injective’ because my math is very rusty, but upon refreshing, I realized two things:
O_bijective : (a = b) -> (c = d) -> (O a c = O b d)
O_bijective Refl Refl = Refl
With these, we can compose and decompose proofs about constructors without having to go through labor to show the outcome of each case. I wanted to call it out specifically because it’s very useful and might be missed unless one knows this pattern can be used.
Among the first question I asked anyone about idris was about proofs that end in having to prove that two things aren’t equal. Idris itself stops being particularly helpful in those cases, giving the weird feeling that you’re just on your own. In some cases you can provide positive proof of the opposite of the required proof and save yourself. In some cases, some rewriting gives a contradiction that idris itself is able to turn into a self evident falsehood.
I wrote a function that, for bools, inverts a proof that two things aren’t equal into a proof that the opposite of one is equal to the other, and leveraged that plenty in the idris I’ve written.
Early on I received some advice that I definitely didn’t fully understand, but came in useful as the foundation of other proof code due to being able to somewhat magically help me combine deciadable cases on a constructor with two arguments.
I’ve been working on providing proof of more properties of this object recently and I finally understand this, and can explain it hopefully in plain language that’s helpful.
My nat-like binary numbers (ugly but functional proof of interop with nat)
https://github.com/prozacchiwawa/idris-binnum:
data Bin = O Nat Bin | BNil
First let’s start with what I was given:
— Thanks: https://www.reddit.com/r/Idris/comments/8yv5fn/using_deceq_in_proofs_extracting_and_applying_the/e2e8a6l/?context=3
O_injective : (O a v = O b w) -> (a = b, v = w)
O_injective Refl = (Refl, Refl)
total aNEBMeansNotEqual : (a : Nat) -> (b : Nat) -> (v : Bin) -> Dec (a = b) -> Dec (O a v = O b v)
aNEBMeansNotEqual a b v (Yes prf) = rewrite prf in Yes Refl
aNEBMeansNotEqual a b v (No contra) =
No $ \\prf =>
let (ojAB, _) = O_injective prf in
contra ojAB
total vNEWMeansNotEqual : (v : Bin) -> (w : Bin) -> Dec (v = w) -> Dec (O Z v = O Z w)
vNEWMeansNotEqual v w (Yes prf) = rewrite prf in Yes Refl
vNEWMeansNotEqual v w (No contra) =
No $ \\prf =>
let (_, ojVW) = O_injective prf in
contra ojVW
I’d like to dissect what’s going on here and really dig into how this helps with many proof obligations one might run into on Bin (and really any constructor with multiple arguments).
O_injective is relying on idris to take a single proof step, namely that because a pairs with b and v pairs with w in a proof, then it can infer that a=b and v=w. Since the proof is a function, it conveniently returns both so we can destructure them. Without this, we’d need to use contradictions and either ‘with’ rules or induction to prove them.
The following decision rules follow from this, using the indicated destructured part of the proof to refute the clause with the given contradiction (either the shift or the tail), giving us an easy way to turn a decision about inequality in one part of the constructor to a decision about equality in the constructor as a whole.
It didn’t occur to me at the time why the function is called ‘injective’ because my math is very rusty, but upon refreshing, I realized two things:
O_bijective : (a = b) -> (c = d) -> (O a c = O b d)
O_bijective Refl Refl = Refl
With these, we can compose and decompose proofs about constructors without having to go through labor to show the outcome of each case. I wanted to call it out specifically because it’s very useful and might be missed unless one knows this pattern can be used.
I wanted to make a vs-code extension that others might not simply rewrite or dismiss when seeing the inside of it not written in a mainstream language, so I was looking for a good elm-like framework. React is close to this but still tragically broken on state, so I wanted something cleaner. ts-elmish seemed the thing.
However I found it worrying that there are no 1-file, simple examples. Nothing really explaining the brass tacks of the typing and actually very permissive typing. You can pass literally anything down the message pipe, but that isn’t a deal breaker for me. At the boundaries I can use diagnostics. I’m much more concerned about making mutable state at least second class if not impossible.
I worked up the absolute simplest (as far as I can tell) example for ts-elmish, cribbed and drastically cut from the examples:
// main.tsx
import * as React from ‘react’
import { render } from ‘react-dom’
import { createElmishComponent } from ‘@ts-elmish/react’// Our callback needs the 'dispatch' function to send a message.
// We'll make our sender functions take it and yield a packaged
// up function that actually sends the message.
//
// Initially i was expecting callbacks to be wrapped in this kind
// of function automatically, but they aren't.
function sender(dispatch,f) {
return (e) => dispatch(f(e));
}
// Make a component that does something.
// note: although you control the state (left side of the
// init "tuple"), a "dispatch" function is added to it by the
// framework, thus the state type is Record<String,any>
const App = createElmishComponent({
init: () => [{count: 0}, []],
update: (state, action) => {
// Make a new state without mutation using the message content
// action is the list given below.
return [{
count: state.count + action[0].add
}, []];
},
view: state => {
return <div>
<h1>Hi there</h1>
<!-- View contains a function sending a message.
-- The function given to sender can use the event
-- argument if it needs.
-- Importantly, message is expected to be enlisted.
-->
<button onClick={sender(state.dispatch, () => [{add:1}])}>
{state.count}
</button>
</div>;
}
});
// And use the component!
render(<App />, document.getElementById(‘app’));
I don’t know if there are drawbacks to this minimalist approach apart from anything regarding code organization but hopefully if someone else is interested in ts-elmish, a simple start will be useful where everything needed is visible.
I wanted to make a vs-code extension that others might not simply rewrite or dismiss when seeing the inside of it not written in a mainstream language, so I was looking for a good elm-like framework. React is close to this but still tragically broken on state, so I wanted something cleaner. ts-elmish seemed the thing.
However I found it worrying that there are no 1-file, simple examples. Nothing really explaining the brass tacks of the typing and actually very permissive typing. You can pass literally anything down the message pipe, but that isn’t a deal breaker for me. At the boundaries I can use diagnostics. I’m much more concerned about making mutable state at least second class if not impossible.
I worked up the absolute simplest (as far as I can tell) example for ts-elmish, cribbed and drastically cut from the examples:
// main.tsx
import * as React from ‘react’
import { render } from ‘react-dom’
import { createElmishComponent } from ‘@ts-elmish/react’// Our callback needs the 'dispatch' function to send a message.
// We'll make our sender functions take it and yield a packaged
// up function that actually sends the message.
//
// Initially i was expecting callbacks to be wrapped in this kind
// of function automatically, but they aren't.
function sender(dispatch,f) {
return (e) => dispatch(f(e));
}
// Make a component that does something.
// note: although you control the state (left side of the
// init "tuple"), a "dispatch" function is added to it by the
// framework, thus the state type is Record<String,any>
const App = createElmishComponent({
init: () => [{count: 0}, []],
update: (state, action) => {
// Make a new state without mutation using the message content
// action is the list given below.
return [{
count: state.count + action[0].add
}, []];
},
view: state => {
return <div>
<h1>Hi there</h1>
<!-- View contains a function sending a message.
-- The function given to sender can use the event
-- argument if it needs.
-- Importantly, message is expected to be enlisted.
-->
<button onClick={sender(state.dispatch, () => [{add:1}])}>
{state.count}
</button>
</div>;
}
});
// And use the component!
render(<App />, document.getElementById(‘app’));
I don’t know if there are drawbacks to this minimalist approach apart from anything regarding code organization but hopefully if someone else is interested in ts-elmish, a simple start will be useful where everything needed is visible.
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 Main
import System
import Data.Bool
import Decidable.Equality
isEven : Nat -> Bool
isEven Z = True
isEven (S Z) = False
isEven (S (S x)) = isEven x
data EvenOrOddNumber : (n : Nat) -> (b : Bool) -> Type where
EON : (n : Nat) -> EvenOrOddNumber n (isEven n)
rawNat : EvenOrOddNumber n b -> Nat
rawNat (EON n) = n
implementation Show (EvenOrOddNumber _ True) where
show x = “even “ ++ (show (rawNat x))
implementation Show (EvenOrOddNumber _ False) where
show x = “odd “ ++ (show (rawNat x))
In the repl, we can try it out:
λΠ> show (EON 3)
“odd 3”
λΠ> show (EON 4)
“even 4”
But when we add:
main : IO ()
main = do
args <- getArgs
putStrLn $ show $ EON $ length args
Something a bit unexpected happens:
- + Errors (1)
` — src/Main.idr line 28 col 13:
While processing right hand side of main. Can’t find an implementation
for Show (EvenOrOddNumber (length args) (isEven (length args))).
src/Main.idr:28:14–28:38
24 |
25 | main : IO ()
26 | main = do
27 | args <- getArgs
28 | putStrLn $ show $ EON $ length args
^^^^^^^^^^^^^^^^^^^^^^^^
How does one fix this?
The answer is the curry-howard correspondence! Functional programs are proofs of type systems. We can use idris’ proof language to erase the constraint obligation and statically determine the instances to be used. We can start with a skeleton that asks whether isEven is true in proof form.
showEON : {n : Nat} -> EvenOrOddNumber n (isEven n) -> String
showEON _ with (decEq (isEven n) True)
showEON _ | Yes prf = ?showT
showEON _ | No contra = ?showFAnd then we can ensure that each of these cases does show on an instance whose type is statically determinable to be implemented.
In this case, we’ll declare a local variable with a type that matches one of our cases:
showEON _ | Yes prf =
let
toShow : EvenOrOddNumber n True
toShow = ?showT
in
show toShow
This doesn’t have a constraint obligation because it trivially has the same shape as an instance of show for our EvenOrOddNumber.
We can use the language of proofs to construct this value by changing the result type back to what we get from the EON constructor.
showEON _ | Yes prf =
let
toShow : EvenOrOddNumber n True
toShow =
rewrite sym prf in
?eon_n -- Main.eon_n : EvenOrOddNumber n (isEven n)
in
show toShow
Shows that we can replace ?eon_n with EON n and this works.
The No case is trickier as is tradition with decEq, but we can start to sketch the proof like this:
showEON _ | No contra = -- contra : isEven n = True -> Void
let
notEven : (isEven n = False)
notEven =
?notEvenEven
toShow : EvenOrOddNumber n False
toShow = ?showF
in
show toShow
So how do we get notEven from contra? Our new friend invertContraBool and some helpers.
invertBoolFalse : {a : Bool} -> not a = True -> a = False
invertBoolFalse {a = True} prf impossible
invertBoolFalse {a = False} prf = ReflAnd done:
let
invertedContra : (not (isEven n) = True)
invertedContra = invertContraBool (isEven n) True contra
notEven : (isEven n = False)
notEven = invertBoolFalse invertedContra
toShow : EvenOrOddNumber n False
toShow =
rewrite sym notEven in
EON n
in
show toShow
And finally:
$ idris2 --build ./tc.ipkg
$ ./build/exec/tc
odd 1
$ ./build/exec/tc foo
even 2
$ ./build/exec/tc `ls -1`
even 4
So what have we learned?
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 Main
import System
import Data.Bool
import Decidable.Equality
isEven : Nat -> Bool
isEven Z = True
isEven (S Z) = False
isEven (S (S x)) = isEven x
data EvenOrOddNumber : (n : Nat) -> (b : Bool) -> Type where
EON : (n : Nat) -> EvenOrOddNumber n (isEven n)
rawNat : EvenOrOddNumber n b -> Nat
rawNat (EON n) = n
implementation Show (EvenOrOddNumber _ True) where
show x = “even “ ++ (show (rawNat x))
implementation Show (EvenOrOddNumber _ False) where
show x = “odd “ ++ (show (rawNat x))
In the repl, we can try it out:
λΠ> show (EON 3)
“odd 3”
λΠ> show (EON 4)
“even 4”
But when we add:
main : IO ()
main = do
args <- getArgs
putStrLn $ show $ EON $ length args
Something a bit unexpected happens:
- + Errors (1)
` — src/Main.idr line 28 col 13:
While processing right hand side of main. Can’t find an implementation
for Show (EvenOrOddNumber (length args) (isEven (length args))).
src/Main.idr:28:14–28:38
24 |
25 | main : IO ()
26 | main = do
27 | args <- getArgs
28 | putStrLn $ show $ EON $ length args
^^^^^^^^^^^^^^^^^^^^^^^^
How does one fix this?
The answer is the curry-howard correspondence! Functional programs are proofs of type systems. We can use idris’ proof language to erase the constraint obligation and statically determine the instances to be used. We can start with a skeleton that asks whether isEven is true in proof form.
showEON : {n : Nat} -> EvenOrOddNumber n (isEven n) -> String
showEON _ with (decEq (isEven n) True)
showEON _ | Yes prf = ?showT
showEON _ | No contra = ?showFAnd then we can ensure that each of these cases does show on an instance whose type is statically determinable to be implemented.
In this case, we’ll declare a local variable with a type that matches one of our cases:
showEON _ | Yes prf =
let
toShow : EvenOrOddNumber n True
toShow = ?showT
in
show toShow
This doesn’t have a constraint obligation because it trivially has the same shape as an instance of show for our EvenOrOddNumber.
We can use the language of proofs to construct this value by changing the result type back to what we get from the EON constructor.
showEON _ | Yes prf =
let
toShow : EvenOrOddNumber n True
toShow =
rewrite sym prf in
?eon_n -- Main.eon_n : EvenOrOddNumber n (isEven n)
in
show toShow
Shows that we can replace ?eon_n with EON n and this works.
The No case is trickier as is tradition with decEq, but we can start to sketch the proof like this:
showEON _ | No contra = -- contra : isEven n = True -> Void
let
notEven : (isEven n = False)
notEven =
?notEvenEven
toShow : EvenOrOddNumber n False
toShow = ?showF
in
show toShow
So how do we get notEven from contra? Our new friend invertContraBool and some helpers.
invertBoolFalse : {a : Bool} -> not a = True -> a = False
invertBoolFalse {a = True} prf impossible
invertBoolFalse {a = False} prf = ReflAnd done:
let
invertedContra : (not (isEven n) = True)
invertedContra = invertContraBool (isEven n) True contra
notEven : (isEven n = False)
notEven = invertBoolFalse invertedContra
toShow : EvenOrOddNumber n False
toShow =
rewrite sym notEven in
EON n
in
show toShow
And finally:
$ idris2 --build ./tc.ipkg
$ ./build/exec/tc
odd 1
$ ./build/exec/tc foo
even 2
$ ./build/exec/tc `ls -1`
even 4
So what have we learned?
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:
Time boxes are thought of as part of scrum practice in some circles, but only at the whole sprint level. I’d suggest they’re more useful at a smaller scale, often to replace items conceptually thought of as deadlines.
Imagine that you’re working on a project and the product owner pulls out the Steelcase® Mobile File Cabinet with Cushion Top beside your desk and says “I’m counting on you to deliver Low Priority Customer’s special features by next tuesday, but make sure to get High Priority Customer’s Full Sprint Issue done too, they’re much more important”. Maybe like me, instead of taking effort to imagine, it’s taking you much more effort to forget. Puzzling for most of these situations is exactly how long Low Priority’s feature has been patiently waiting at “Medium” priority in your “big Jira of failure and regret”. Why wasn’t this worked on in the 3 whole months between when Low Priority became your customer and when they wanted their thing? Because it wasn’t high like everything on High Priority’s list. Now it’s high because it’s almost comically and disastrously late, and still possibly worth a lot of money. It can easily be the case that all told, a full year of dev time would be paid for by the delivery of Low Priority; High is simply worth _more_.
Regardless, there’s a lot here, so let’s think about this request and what it means. Unfortunately there’s nothing you or I can do now, or even could have done at that moment, but I believe there’s something the next iteration of similar atoms coming together in a similar configuration can do in this infinite universe.
So if you could just Dr Strange your way to a better world, what should you do?
Enter: The “delivery timebox”.
Timeboxes haven’t been specialized in the scrum literature I’ve seen since every sprint is considered by itself to be a “delivery timebox”, but I’m going to make that explicit here to separate it from an “experiment timebox”.
An “experiment timebox” is where you try an experiment or make an honest effort to do something and the deliverable is the reported _experience_. A race can be an experiment timebox because you’re trying to cross the finish line faster than your last time, and the outcome is the amount of time. If your training is making you faster, it gets better, if not it might get worse. Ultimately, you’re not going to slow down or stop training regardless, but you might use the result for guidance. Similarly, timeboxing an experimental feature in software is similar. The outcome will inform decisions like “is this important enough to soldier through?” and “can we do it cheaply or should we buy it?”
A “delivery timebox” is a little sprint just for one or a few. The goal is simply to improve something in the scrum conception “potentially shippable” into something better and still “potentially shippable”. You don’t need anyone to kill themselves (hopefully) over all the features (you won’t get them anyway by waiting until the last week and then hot potatoing the whole thing on somebody). If you’ve got time, then you don’t need to set any deadlines yet, and you can still set “aspirational” goals for these experiments to see what’s left in the hopper, in fact it’s desirable (in my opinion) that a “delivery timebox” has about 1 1/2 times the amount of stuff in it that it actually needs, to make room for all outcomes to have some meaning. Too little and it just gets done without saying a lot; too much and you’re just going to encourage a feeling of hopelessness. There’s no point in picking up the second grain when the task is to move a mountain.
Going back to deadlines, why wasn’t this assigned earlier? Most likely because
Why do we use deadlines this way though? What’s the purpose? Often it’s to “show improvement”, “justify budgets” and “take to the board meeting”. While there’s no getting around a situation where a single URL will be on a super bowl ad, how often is that really the reason we have tight deadlines? Aren’t most of these just as well served by “delivery timeboxes” as well, leaving deadlines for the really important things?
If you’re a product owner, make room, not with deadlines, but with delivery timeboxes. Spread the work out so you can see what’s going on and so that, worst case, the person you finally do put a deadline on in the last week can be adding the last features, not the first. Use deadlines where there’s something external at stake and delivery timeboxes when you want to show something new to the board. Retain your capacity to respond to real emergencies _and_ avoid urgency.
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:
Time boxes are thought of as part of scrum practice in some circles, but only at the whole sprint level. I’d suggest they’re more useful at a smaller scale, often to replace items conceptually thought of as deadlines.
Imagine that you’re working on a project and the product owner pulls out the Steelcase® Mobile File Cabinet with Cushion Top beside your desk and says “I’m counting on you to deliver Low Priority Customer’s special features by next tuesday, but make sure to get High Priority Customer’s Full Sprint Issue done too, they’re much more important”. Maybe like me, instead of taking effort to imagine, it’s taking you much more effort to forget. Puzzling for most of these situations is exactly how long Low Priority’s feature has been patiently waiting at “Medium” priority in your “big Jira of failure and regret”. Why wasn’t this worked on in the 3 whole months between when Low Priority became your customer and when they wanted their thing? Because it wasn’t high like everything on High Priority’s list. Now it’s high because it’s almost comically and disastrously late, and still possibly worth a lot of money. It can easily be the case that all told, a full year of dev time would be paid for by the delivery of Low Priority; High is simply worth _more_.
Regardless, there’s a lot here, so let’s think about this request and what it means. Unfortunately there’s nothing you or I can do now, or even could have done at that moment, but I believe there’s something the next iteration of similar atoms coming together in a similar configuration can do in this infinite universe.
So if you could just Dr Strange your way to a better world, what should you do?
Enter: The “delivery timebox”.
Timeboxes haven’t been specialized in the scrum literature I’ve seen since every sprint is considered by itself to be a “delivery timebox”, but I’m going to make that explicit here to separate it from an “experiment timebox”.
An “experiment timebox” is where you try an experiment or make an honest effort to do something and the deliverable is the reported _experience_. A race can be an experiment timebox because you’re trying to cross the finish line faster than your last time, and the outcome is the amount of time. If your training is making you faster, it gets better, if not it might get worse. Ultimately, you’re not going to slow down or stop training regardless, but you might use the result for guidance. Similarly, timeboxing an experimental feature in software is similar. The outcome will inform decisions like “is this important enough to soldier through?” and “can we do it cheaply or should we buy it?”
A “delivery timebox” is a little sprint just for one or a few. The goal is simply to improve something in the scrum conception “potentially shippable” into something better and still “potentially shippable”. You don’t need anyone to kill themselves (hopefully) over all the features (you won’t get them anyway by waiting until the last week and then hot potatoing the whole thing on somebody). If you’ve got time, then you don’t need to set any deadlines yet, and you can still set “aspirational” goals for these experiments to see what’s left in the hopper, in fact it’s desirable (in my opinion) that a “delivery timebox” has about 1 1/2 times the amount of stuff in it that it actually needs, to make room for all outcomes to have some meaning. Too little and it just gets done without saying a lot; too much and you’re just going to encourage a feeling of hopelessness. There’s no point in picking up the second grain when the task is to move a mountain.
Going back to deadlines, why wasn’t this assigned earlier? Most likely because
Why do we use deadlines this way though? What’s the purpose? Often it’s to “show improvement”, “justify budgets” and “take to the board meeting”. While there’s no getting around a situation where a single URL will be on a super bowl ad, how often is that really the reason we have tight deadlines? Aren’t most of these just as well served by “delivery timeboxes” as well, leaving deadlines for the really important things?
If you’re a product owner, make room, not with deadlines, but with delivery timeboxes. Spread the work out so you can see what’s going on and so that, worst case, the person you finally do put a deadline on in the last week can be adding the last features, not the first. Use deadlines where there’s something external at stake and delivery timeboxes when you want to show something new to the board. Retain your capacity to respond to real emergencies _and_ avoid urgency.
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). I’m not aware of any library providing this functionality in idris, even though it’s useful for a lot of things (for example, many json formats use a list of objects with a name field each to reduce duplication in json, but they must be unique names).
Things one can learn from this:
module Data.AList
import Data.Bool
import Decidable.Equality
keyInList : Eq a => a -> List (Pair a b) -> Bool
keyInList k [] = False
keyInList k ((k1, v1) :: others) =
if k == k1 then
True
else
keyInList k others
allKeysUniqueInList : Eq a => List (Pair a b) -> Bool
allKeysUniqueInList [] = True
allKeysUniqueInList ((k, v) :: others) =
let
headIsUnique = not (keyInList k others)
tailsAreUnique = allKeysUniqueInList others
in
tailsAreUnique && headIsUnique
kvCons : a -> b -> List (Pair a b) -> List (Pair a b)
kvCons k v l = (k,v) :: l
appendBreak : Eq a => (k : a) -> (v : b) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True))
appendBreak k v l p with (decEq (keyInList k l) True)
appendBreak k v l p | Yes prf = (l ** p)
appendBreak k v l p | No contra =
let
cproof = invertContraBool (keyInList k l) True contra
in
(kvCons k v l ** outProof k l p cproof)
where
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
public export
proveList : Eq a => (l : List (Pair a b)) -> Maybe (DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True))
proveList l with (decEq (allKeysUniqueInList l) True)
proveList l | Yes prf = Just (l ** prf)
proveList l | No _ = Nothing
public export
addIfUnique : Eq a => (k : a) -> (v : b) -> (l : DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True)) -> DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True)
addIfUnique k v (l ** p) = appendBreak k v l p
Supported by a function I’ve PR’d for Data.Bool: invertContraBool
---------------------------------------
-- Decidability specialized on bool
---------------------------------------
||| You can reverse decidability when bool is involved.
-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
invertContraBool False True contra = Refl
invertContraBool True False contra = Refl
invertContraBool True True contra = absurd $ contra Refl
Something I’ve been confused by for a while is how to get any utility out of contra. Usually it’s taunting me with a function taking an impossible proof and yielding Void, but what can I actually do with that? What does it solve?
I think the use of the absurd could use concrete explanation here:
Reading these words, I thought I understood it, but didn’t really get what idris was doing mechanically, then I finally decided to look over every use I could see of absurd and try to see what they were doing. Ultimately, the important thing is that absurd is like idris_crash in that its result is an unpaired ‘a’ type variable so it can satisfy the result of any function, but more importantly, mechanically it is passing on the property of unhabitation to the thing that uses it, erasing the need to return a result for some case.
Since contra is a function taking a proof, if we can supply it with that proof, we can get a Void to plug into absurd:
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
Or more elaborately to show what’s happening:
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool a b contra = invertContraBool_ a b contra
where
fEf : False = False
fEf = Refl
tEt : True = True
tEt = Refl
invertContraBool_ : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool_ False False contra = absurd (contra fEf)
invertContraBool_ False True contra = Refl
invertContraBool_ True False contra = Refl
invertContraBool_ True True contra = absurd (contra tEt)
Since contra is the contradiction of a proof that a = b, a proof that a = b (such as True = True) when a and b are True, satisfies it and gives us the Void object, which we can use with absurd to satisfy this case (return a) without really knowing how. Idris knows that this code is unreachable due to absurd being satisfied.
So how do you use invertContraBool?
Take a look at appendBreak in the code (I use ‘break’ or ‘broken’ often to mean ‘with arguments separated out’)
appendBreak : Eq a => (k : a) -> (v : b) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True))
appendBreak k v l p with (decEq (keyInList k l) True)
appendBreak k v l p | Yes prf = (l ** p)
appendBreak k v l p | No contra =
let
cproof = invertContraBool (keyInList k l) True contra
in
(kvCons k v l ** outProof k l p cproof)
where
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
We’re building a dependent pair (more on that in a moment) that contains the list and a function yielding a proof about a list, and we start with the opposite of any kind of proof. In our case the only information we have is that we can use absurd if keyInList k l = True. Even worse, we already know that it isn’t, so this contra function would appear to be totally useless most of the time, when we’re dealing with concrete data.
Since Bool has only 2 values though, we can enumerate all the cases and show idris that the only sensible result is that a and b aren’t equal (since we have a function that shows idris that it can ignore the idea that they could be) and therefore show that the other cases work to show not a = b. The function is total and we haven’t missed any cases, therefore I believe this proof is sound.
So now, starting with the mess of a = b -> Void, we have the more useful (not a = b), which we capture here into
cproof : not (keyInList k l) = True
cproof = invertContraBool (keyInList k l) True contra
And from there, we can figure out a way to write the proof that the new list also has unique keys:
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
Using the very proof we were able to get, not (keyInList k l) = True
We rewrite with that and the proof given with the original list, that all its keys were unique and satisfy allKeysUniqueInList:
allKeysUniqueInList ((k, v) :: others) =
let
headIsUnique = not (keyInList k others)
tailsAreUnique = allKeysUniqueInList others
in
tailsAreUnique && headIsUnique
Now is the time to discuss how to use DPair. It has mechanics that are complicated and so in my view, situational.
What I found was that Idris is able to understand simple constructions using ** in types:
proofPair : (v : a) -> (f : a -> Bool) -> (p : f v = True) -> (v ** f v = True)
proofPair v f p = MkDPair v p
Idris definitely DWIM here:
λΠ> :t proofPair
Data.AList.proofPair : (v : a) -> (f : (a -> Bool)) -> f v = True -> DPair a (\\v => f v = True)
But other times I struggled to write the expression I wanted into the type, getting all sorts of generic-y errors. When this happens, declare the type more formally:
DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True)
You can use the ** data constructor to either pick apart a dpair (or you can name the constructor with MkDPair
addIfUnique k v (l ** p) = appendBreak k v l p -- Good
addIfUnique k v (MkDPair l p) = appendBreak k v l p-- also good
And you can of course construct them either way at runtime:
public export
proveList : Eq a => (l : List (Pair a b)) -> Maybe (DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True))
proveList l with (decEq (allKeysUniqueInList l) True)
proveList l | Yes prf = Just (l ** prf) -- (MkDPair l prf) works too
proveList l | No _ = Nothing
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). I’m not aware of any library providing this functionality in idris, even though it’s useful for a lot of things (for example, many json formats use a list of objects with a name field each to reduce duplication in json, but they must be unique names).
Things one can learn from this:
module Data.AList
import Data.Bool
import Decidable.Equality
keyInList : Eq a => a -> List (Pair a b) -> Bool
keyInList k [] = False
keyInList k ((k1, v1) :: others) =
if k == k1 then
True
else
keyInList k others
allKeysUniqueInList : Eq a => List (Pair a b) -> Bool
allKeysUniqueInList [] = True
allKeysUniqueInList ((k, v) :: others) =
let
headIsUnique = not (keyInList k others)
tailsAreUnique = allKeysUniqueInList others
in
tailsAreUnique && headIsUnique
kvCons : a -> b -> List (Pair a b) -> List (Pair a b)
kvCons k v l = (k,v) :: l
appendBreak : Eq a => (k : a) -> (v : b) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True))
appendBreak k v l p with (decEq (keyInList k l) True)
appendBreak k v l p | Yes prf = (l ** p)
appendBreak k v l p | No contra =
let
cproof = invertContraBool (keyInList k l) True contra
in
(kvCons k v l ** outProof k l p cproof)
where
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
public export
proveList : Eq a => (l : List (Pair a b)) -> Maybe (DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True))
proveList l with (decEq (allKeysUniqueInList l) True)
proveList l | Yes prf = Just (l ** prf)
proveList l | No _ = Nothing
public export
addIfUnique : Eq a => (k : a) -> (v : b) -> (l : DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True)) -> DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True)
addIfUnique k v (l ** p) = appendBreak k v l p
Supported by a function I’ve PR’d for Data.Bool: invertContraBool
---------------------------------------
-- Decidability specialized on bool
---------------------------------------
||| You can reverse decidability when bool is involved.
-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
invertContraBool False True contra = Refl
invertContraBool True False contra = Refl
invertContraBool True True contra = absurd $ contra Refl
Something I’ve been confused by for a while is how to get any utility out of contra. Usually it’s taunting me with a function taking an impossible proof and yielding Void, but what can I actually do with that? What does it solve?
I think the use of the absurd could use concrete explanation here:
Reading these words, I thought I understood it, but didn’t really get what idris was doing mechanically, then I finally decided to look over every use I could see of absurd and try to see what they were doing. Ultimately, the important thing is that absurd is like idris_crash in that its result is an unpaired ‘a’ type variable so it can satisfy the result of any function, but more importantly, mechanically it is passing on the property of unhabitation to the thing that uses it, erasing the need to return a result for some case.
Since contra is a function taking a proof, if we can supply it with that proof, we can get a Void to plug into absurd:
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
Or more elaborately to show what’s happening:
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool a b contra = invertContraBool_ a b contra
where
fEf : False = False
fEf = Refl
tEt : True = True
tEt = Refl
invertContraBool_ : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool_ False False contra = absurd (contra fEf)
invertContraBool_ False True contra = Refl
invertContraBool_ True False contra = Refl
invertContraBool_ True True contra = absurd (contra tEt)
Since contra is the contradiction of a proof that a = b, a proof that a = b (such as True = True) when a and b are True, satisfies it and gives us the Void object, which we can use with absurd to satisfy this case (return a) without really knowing how. Idris knows that this code is unreachable due to absurd being satisfied.
So how do you use invertContraBool?
Take a look at appendBreak in the code (I use ‘break’ or ‘broken’ often to mean ‘with arguments separated out’)
appendBreak : Eq a => (k : a) -> (v : b) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True))
appendBreak k v l p with (decEq (keyInList k l) True)
appendBreak k v l p | Yes prf = (l ** p)
appendBreak k v l p | No contra =
let
cproof = invertContraBool (keyInList k l) True contra
in
(kvCons k v l ** outProof k l p cproof)
where
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
We’re building a dependent pair (more on that in a moment) that contains the list and a function yielding a proof about a list, and we start with the opposite of any kind of proof. In our case the only information we have is that we can use absurd if keyInList k l = True. Even worse, we already know that it isn’t, so this contra function would appear to be totally useless most of the time, when we’re dealing with concrete data.
Since Bool has only 2 values though, we can enumerate all the cases and show idris that the only sensible result is that a and b aren’t equal (since we have a function that shows idris that it can ignore the idea that they could be) and therefore show that the other cases work to show not a = b. The function is total and we haven’t missed any cases, therefore I believe this proof is sound.
So now, starting with the mess of a = b -> Void, we have the more useful (not a = b), which we capture here into
cproof : not (keyInList k l) = True
cproof = invertContraBool (keyInList k l) True contra
And from there, we can figure out a way to write the proof that the new list also has unique keys:
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
Using the very proof we were able to get, not (keyInList k l) = True
We rewrite with that and the proof given with the original list, that all its keys were unique and satisfy allKeysUniqueInList:
allKeysUniqueInList ((k, v) :: others) =
let
headIsUnique = not (keyInList k others)
tailsAreUnique = allKeysUniqueInList others
in
tailsAreUnique && headIsUnique
Now is the time to discuss how to use DPair. It has mechanics that are complicated and so in my view, situational.
What I found was that Idris is able to understand simple constructions using ** in types:
proofPair : (v : a) -> (f : a -> Bool) -> (p : f v = True) -> (v ** f v = True)
proofPair v f p = MkDPair v p
Idris definitely DWIM here:
λΠ> :t proofPair
Data.AList.proofPair : (v : a) -> (f : (a -> Bool)) -> f v = True -> DPair a (\\v => f v = True)
But other times I struggled to write the expression I wanted into the type, getting all sorts of generic-y errors. When this happens, declare the type more formally:
DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True)
You can use the ** data constructor to either pick apart a dpair (or you can name the constructor with MkDPair
addIfUnique k v (l ** p) = appendBreak k v l p -- Good
addIfUnique k v (MkDPair l p) = appendBreak k v l p-- also good
And you can of course construct them either way at runtime:
public export
proveList : Eq a => (l : List (Pair a b)) -> Maybe (DPair (List (Pair a b)) (\\l => allKeysUniqueInList l = True))
proveList l with (decEq (allKeysUniqueInList l) True)
proveList l | Yes prf = Just (l ** prf) -- (MkDPair l prf) works too
proveList l | No _ = Nothing
Two things I learned from this:
So I’ve often run into hassles showing Idris that something like (a > b) => (a - b) > 0, and these grow when the complexity of the operations increases. Taking your code, decomposing what it does in proof code, then reassembling the result in the form of proof is a drag after the fact. What you need to do is have values that encode their value in their type, but working on those can be hard as well. You don’t know what to call their types and how to identify the type of things can get out of hand.
If you’ve tried naively to prove something that uses the Integer relational operators, you’ve likely run into idris not really having a lot of insight. Proof code can’t look inside these even when the values are statically known since the relational operators are provided by interfaces that are fulfilled by builtin functions (and idris doesn’t have any insight into these). You can try to complete these proofs by using LTE, but I find that I’m kind of not smart enough. I need more help than idris is capable of providing (i used to get by with the tactic based prover, but even then wrote absurdly dumb proof code) but there really is a better way.
Consider this type:
data SignedNat : Bool -> Nat -> Type where
Neg : (n:Nat) -> SignedNat True n
Pos : (n:Nat) -> SignedNat False n
It both contains a runtime representation of the value and encodes the corresponding value in its type. If you hold this then idris at least conceptually knows what its value is, so that’s one thing: you don’t need to worry about how you’ll figure out what it contains because you’ll be required at each level to keep track (it’s a magic proof assistant).
Now you might look at this and think: It’s just more a more complicated Nat! How does this help us with proofs?
So the general strategy is that any operation we want to provide here, we’ll do so with symbols in our idris code. This will allow this number representation to give us analytic power we haven’t had before:
public export
interface GreaterSN sna snb where
gtrSN : sna -> snb -> Bool
It doesn’t look like much but the types here carry helpful info. As long as a ?postpone isn’t used, idris has access to the implementation that goes along with a specific value and therefore any necessary induction via “auto variables” that declare interfaces needed:
public export
implementation (GreaterSN (SignedNat False a) (SignedNat False b)) => GreaterSN (SignedNat False (S a)) (SignedNat False (S b)) where
gtrSN (Pos (S a)) (Pos (S b)) = gtrSN (Pos a) (Pos b)
This takes “GreaterSN (SignedNat False a) (SignedNat False b)” and provides “GreaterSN (SignedNat False (S a)) (SignedNat False (S b))”, but it does some nice things. You can write this without specifying what implementations are required and idris will tell you if they’re missing (or if you specify them here and they can’t be fulfilled). So it’s very assisitant-y. Importantly, idris doesn’t need any help to know the outcome when these have nice base cases like:
public export
implementation GreaterSN (SignedNat False Z) (SignedNat False _) where
gtrSN _ _ = False
This works (you might be breathing a sigh of relief if you’ve tried proving things about numbers naively):
proveNeg15GreaterThanNeg30 : gtrSN (Neg 15) (Neg 30) = True
proveNeg15GreaterThanNeg30 = Refl
So you can provide even fairly complicated things this way and they’re 100% understood by idris:
public export
interface SubSN sna snb where
subSN : sna -> snb -> (Bool, Nat)
public export
implementation SubSN (SignedNat _ _) (SignedNat _ Z) where
subSN (Neg x) _ = (True, x)
subSN (Pos x) _ = (False, x)
public export
implementation SubSN (SignedNat True _) (SignedNat False _) where
subSN (Neg x) (Pos y) = (True, x + y)
public export
implementation SubSN (SignedNat False _) (SignedNat True _) where
subSN (Pos x) (Neg y) = (False, x + y)
public export
implementation SubSN (SignedNat False Z) (SignedNat False (S n)) where
subSN (Pos Z) (Pos (S n)) = subSN (Neg 1) (Pos n)
public export
implementation SubSN (SignedNat True Z) (SignedNat False (S n)) where
subSN (Neg Z) (Pos (S n)) = subSN (Neg 1) (Pos n)
public export
implementation SubSN (SignedNat False n) (SignedNat False m) => SubSN (SignedNat False (S n)) (SignedNat False (S m)) where
subSN (Pos (S n)) (Pos (S m)) = subSN (Pos n) (Pos m)
public export
implementation SubSN (SignedNat True n) (SignedNat True m) => SubSN (SignedNat True (S n)) (SignedNat True (S m)) where
subSN (Neg (S n)) (Neg (S m)) = subSN (Neg n) (Neg m)
I wrote proofs to ensure that idris knows the results come from this type, but I actually never needed to rewrite with these :-)
The type of a type level list is tricky because there’s a leap of faith involved:
data Memory : Bool -> Nat -> mem -> Type where
MWord : (s : Bool) -> (v : Nat) -> Memory t w rest -> Memory s v (Memory t w rest)
MEnd : (s : Bool) -> (v : Nat) -> Memory s v Unit
Note the “mem” here doesn’t specify its own structure and would only be able to do so to a fixed depth. So we can make lists of this kind:
mem : Memory False 3 (Memory False 2 (Memory False 5 Unit))
mem = MWord False 3 (MWord False 2 (MEnd False 5))
It might be tempting to use Void here but really don’t :-) Unit is _much_ better. You’ll thank me for this advice alone. Because Void is a bit special, idris can be frustrating to write in its presence, whether idris can figure out if a case is needed or extra may change with unrelated code, and other things I’m not smart enough to understand happen. Use Unit and be happy.
And the type knows the entire contents. It’s important to understand though that you can’t have “only” a type :-) The type must be backed with runtime values (you can’t cheat and just compute types), but you can require them to match all along, saving proof work at the end.
So you might ask: how do we read this if we don’t know a priori what type to call it by? The answer as before is interfaces:
interface TypeOfReadSign maddr mem where
typeOfReadSign : maddr -> mem -> Bool
interface TypeOfReadMag maddr mem where
typeOfReadMag : maddr -> mem -> Nat
These can tell us what the contents of a specific location are. I’ve used another type here,
data MemoryAddress : Nat -> Type where
MAddr : (n:Nat) -> MemoryAddress n
To carry the address at the type level so we can differentiate Z and (S n) nicely.
implementation TypeOfReadSign (MemoryAddress Z) (Memory s v rest) where
typeOfReadSign _ (MEnd False _) = False
typeOfReadSign _ (MEnd True _) = True
typeOfReadSign _ (MWord False _ _) = False
typeOfReadSign _ (MWord True _ _) = True
implementation TypeOfReadSign (MemoryAddress (S n)) (Memory s v Unit) where
typeOfReadSign _ _ = False
And of course we’ve got an empty implementation:
implementation TypeOfReadSign maddr any where
typeOfReadSign _ _ = False
That allows us to punt on proving that the list only contains Unit and “Memory s v rest”. Basically, it frees us from having to describe rest any further.
So now is the complicated bit I iterated on for a long time, how to compute the type of the list when modified and ensure that a parallel structure is built. I actually started by writing a simple interface induction as above that computed the type, and it went relatively well:
interface ModTypeInterface mem where
modTypeInterface : Maybe Nat -> mem -> SignedNat x v -> Maybe BrokenMemory
public export
implementation ModTypeInterface (Memory s t rest) where
modTypeInterface Nothing (MEnd s v) _ = Just (broken s v Nothing)
modTypeInterface Nothing (MWord s v r) _ =
let
t : Maybe BrokenMemory
t = modTypeInterface Nothing r (Pos 0)
in
Just (broken s v t)
modTypeInterface (Just Z) (MEnd s v) (Pos e) =
Just (broken s v Nothing)
modTypeInterface (Just Z) (MEnd s v) (Neg e) =
Just (broken s v Nothing)
modTypeInterface (Just Z) (MWord s v r) (Pos e) =
let
t : Maybe BrokenMemory
t = modTypeInterface Nothing r (Pos e)
in
Just (broken False e t)
modTypeInterface (Just Z) (MWord s v r) (Neg e) =
let
t : Maybe BrokenMemory
t = modTypeInterface Nothing r (Pos e)
in
Just (broken True e t)
modTypeInterface (Just (S n)) (MEnd s v) a =
Just (broken s v Nothing)
modTypeInterface (Just (S n)) (MWord s v r) (Pos e) =
let
t : Maybe BrokenMemory
t = modTypeInterface (Just n) r (Pos e)
in
Just (broken s v t)
modTypeInterface (Just (S n)) (MWord s v r) (Neg e) =
let
t : Maybe BrokenMemory
t = modTypeInterface (Just n) r (Neg e)
in
Just (broken s v t)
Long but not surprising, what came later though was not great, in that while the value that goes along with this is easy to compute, one runs into a problem; the “rest” returned may not have enough information to show idris that it is the same type as what’s claimed, despite that we’ve got two parallel implementations that do that, so that’s where this gets tricky. I needed to take my BrokenMemory which doesn’t encode the type, and use type level information available at each stage to ensure that the result is the type I claim.
modRamValue Nothing = ()
modRamValue (Just b) = unbrokenNext b
public export
modifyRam : ModTypeInterface mem => {n : Nat} -> MemoryAddress n -> (m : mem) -> (a : SignedNat q x) -> typeOfModRam (modTypeInterface (Just n) m a)
modifyRam ma m a = modRamValue (modTypeInterface (Just n) m a)
So the type here is returned from TypeOfRam and the value is created by modRamValue via a BrokenMemory list.
I had a bit of an inspiration though: since proofs are functions yielding (= a a) at the type level, I included a function in each broken that, given the computed type for the tail, produces the proof that the tail meets our requirement, allowing us to rewrite the return value of the function using the tail so that the requirement to match is elided at that level:
public export
intoMemory : (a : Bool) -> (b : Nat) -> (Type -> Type)
intoMemory a b = Memory a b
public export
proofIntoMemoryAddsMemory : (a : Bool) -> (b : Nat) -> (t : Type) -> intoMemory a b t = Memory a b t
proofIntoMemoryAddsMemory a b t = Refl
public export
proofOfIntoMemory : (a : Bool) -> (b : Nat) -> (f : Type -> Type) -> (f = intoMemory a b) -> (t : Type) -> f t = Memory a b t
proofOfIntoMemory a b f prf t =
rewrite prf in
Refl
broken b n r =
let
imp : (t : Type) -> (intoMemory b n) t = Memory b n t
imp = proofOfIntoMemory b n (intoMemory b n) Refl
in
Broken b n (intoMemory b n) imp r
The purpose of this proof is to tell idris that while what we’re giving is named by an opaque type variable, the result actually matches Memory s v rest to one more depth level, so by using this proof to rewrite the result from a function downstream, we can say “it’s ok, this thing matches so you don’t need to require the match in the result”. Once the result type is rewritten the value we gave matches.
And experimented with this assistant style until there were no holes :-O
convertTail : (b : BrokenMemory) -> typeOfBroken b -> Memory (getSignFromBroken b) (getMagFromBroken b) (getNextTypeFromBroken b)
convertTail b@(Broken s v mt prf x@(Just rr)) r =
rewrite sym (mwordSatisfiesTypeOfBrokenR b) in
let
ctail = convertTail rr (unbrokenNext rr)
res = MWord s v ctail
in
rewrite prf (typeOfBroken rr) in
rewrite mwordSatisfiesTypeOfBrokenR rr in
res
convertTail b@(Broken s v mt prf Nothing) r =
rewrite sym (mwordSatisfiesTypeOfBrokenR b) in
rewrite prf Unit in
let
res = MEnd s v
in
res
unbrokenNext b@(Broken s v mt prf Nothing) =
rewrite prf Unit in
MEnd s v
unbrokenNext b@(Broken s v mt prf (Just r)) =
let
next = unbrokenNext r
in
rewrite prf (typeOfBroken r) in
rewrite mwordSatisfiesTypeOfBrokenR r in
let
res = MWord s v (convertTail r next)
in
res
And applying this allows the memory to be mutated and tracked at the type level!
4/4: Building Main (src/Main.idr)
λΠ> mem
MWord False 3 (MWord False 2 (MEnd False 5))
λΠ> modifyRam (MAddr 1) mem (Neg 17)
MWord False 3 (MWord True 17 (MEnd False 5))
λΠ> :t (modifyRam (MAddr 1) mem (Neg 17))
modifyRam (MAddr 1) mem (Neg 17) : Memory False 3 (Memory True 17 (Memory False 5 ()))
λΠ>
That is some lambda pie indeed.
Two things I learned from this:
So I’ve often run into hassles showing Idris that something like (a > b) => (a - b) > 0, and these grow when the complexity of the operations increases. Taking your code, decomposing what it does in proof code, then reassembling the result in the form of proof is a drag after the fact. What you need to do is have values that encode their value in their type, but working on those can be hard as well. You don’t know what to call their types and how to identify the type of things can get out of hand.
If you’ve tried naively to prove something that uses the Integer relational operators, you’ve likely run into idris not really having a lot of insight. Proof code can’t look inside these even when the values are statically known since the relational operators are provided by interfaces that are fulfilled by builtin functions (and idris doesn’t have any insight into these). You can try to complete these proofs by using LTE, but I find that I’m kind of not smart enough. I need more help than idris is capable of providing (i used to get by with the tactic based prover, but even then wrote absurdly dumb proof code) but there really is a better way.
Consider this type:
data SignedNat : Bool -> Nat -> Type where
Neg : (n:Nat) -> SignedNat True n
Pos : (n:Nat) -> SignedNat False n
It both contains a runtime representation of the value and encodes the corresponding value in its type. If you hold this then idris at least conceptually knows what its value is, so that’s one thing: you don’t need to worry about how you’ll figure out what it contains because you’ll be required at each level to keep track (it’s a magic proof assistant).
Now you might look at this and think: It’s just more a more complicated Nat! How does this help us with proofs?
So the general strategy is that any operation we want to provide here, we’ll do so with symbols in our idris code. This will allow this number representation to give us analytic power we haven’t had before:
public export
interface GreaterSN sna snb where
gtrSN : sna -> snb -> Bool
It doesn’t look like much but the types here carry helpful info. As long as a ?postpone isn’t used, idris has access to the implementation that goes along with a specific value and therefore any necessary induction via “auto variables” that declare interfaces needed:
public export
implementation (GreaterSN (SignedNat False a) (SignedNat False b)) => GreaterSN (SignedNat False (S a)) (SignedNat False (S b)) where
gtrSN (Pos (S a)) (Pos (S b)) = gtrSN (Pos a) (Pos b)
This takes “GreaterSN (SignedNat False a) (SignedNat False b)” and provides “GreaterSN (SignedNat False (S a)) (SignedNat False (S b))”, but it does some nice things. You can write this without specifying what implementations are required and idris will tell you if they’re missing (or if you specify them here and they can’t be fulfilled). So it’s very assisitant-y. Importantly, idris doesn’t need any help to know the outcome when these have nice base cases like:
public export
implementation GreaterSN (SignedNat False Z) (SignedNat False _) where
gtrSN _ _ = False
This works (you might be breathing a sigh of relief if you’ve tried proving things about numbers naively):
proveNeg15GreaterThanNeg30 : gtrSN (Neg 15) (Neg 30) = True
proveNeg15GreaterThanNeg30 = Refl
So you can provide even fairly complicated things this way and they’re 100% understood by idris:
public export
interface SubSN sna snb where
subSN : sna -> snb -> (Bool, Nat)
public export
implementation SubSN (SignedNat _ _) (SignedNat _ Z) where
subSN (Neg x) _ = (True, x)
subSN (Pos x) _ = (False, x)
public export
implementation SubSN (SignedNat True _) (SignedNat False _) where
subSN (Neg x) (Pos y) = (True, x + y)
public export
implementation SubSN (SignedNat False _) (SignedNat True _) where
subSN (Pos x) (Neg y) = (False, x + y)
public export
implementation SubSN (SignedNat False Z) (SignedNat False (S n)) where
subSN (Pos Z) (Pos (S n)) = subSN (Neg 1) (Pos n)
public export
implementation SubSN (SignedNat True Z) (SignedNat False (S n)) where
subSN (Neg Z) (Pos (S n)) = subSN (Neg 1) (Pos n)
public export
implementation SubSN (SignedNat False n) (SignedNat False m) => SubSN (SignedNat False (S n)) (SignedNat False (S m)) where
subSN (Pos (S n)) (Pos (S m)) = subSN (Pos n) (Pos m)
public export
implementation SubSN (SignedNat True n) (SignedNat True m) => SubSN (SignedNat True (S n)) (SignedNat True (S m)) where
subSN (Neg (S n)) (Neg (S m)) = subSN (Neg n) (Neg m)
I wrote proofs to ensure that idris knows the results come from this type, but I actually never needed to rewrite with these :-)
The type of a type level list is tricky because there’s a leap of faith involved:
data Memory : Bool -> Nat -> mem -> Type where
MWord : (s : Bool) -> (v : Nat) -> Memory t w rest -> Memory s v (Memory t w rest)
MEnd : (s : Bool) -> (v : Nat) -> Memory s v Unit
Note the “mem” here doesn’t specify its own structure and would only be able to do so to a fixed depth. So we can make lists of this kind:
mem : Memory False 3 (Memory False 2 (Memory False 5 Unit))
mem = MWord False 3 (MWord False 2 (MEnd False 5))
It might be tempting to use Void here but really don’t :-) Unit is _much_ better. You’ll thank me for this advice alone. Because Void is a bit special, idris can be frustrating to write in its presence, whether idris can figure out if a case is needed or extra may change with unrelated code, and other things I’m not smart enough to understand happen. Use Unit and be happy.
And the type knows the entire contents. It’s important to understand though that you can’t have “only” a type :-) The type must be backed with runtime values (you can’t cheat and just compute types), but you can require them to match all along, saving proof work at the end.
So you might ask: how do we read this if we don’t know a priori what type to call it by? The answer as before is interfaces:
interface TypeOfReadSign maddr mem where
typeOfReadSign : maddr -> mem -> Bool
interface TypeOfReadMag maddr mem where
typeOfReadMag : maddr -> mem -> Nat
These can tell us what the contents of a specific location are. I’ve used another type here,
data MemoryAddress : Nat -> Type where
MAddr : (n:Nat) -> MemoryAddress n
To carry the address at the type level so we can differentiate Z and (S n) nicely.
implementation TypeOfReadSign (MemoryAddress Z) (Memory s v rest) where
typeOfReadSign _ (MEnd False _) = False
typeOfReadSign _ (MEnd True _) = True
typeOfReadSign _ (MWord False _ _) = False
typeOfReadSign _ (MWord True _ _) = True
implementation TypeOfReadSign (MemoryAddress (S n)) (Memory s v Unit) where
typeOfReadSign _ _ = False
And of course we’ve got an empty implementation:
implementation TypeOfReadSign maddr any where
typeOfReadSign _ _ = False
That allows us to punt on proving that the list only contains Unit and “Memory s v rest”. Basically, it frees us from having to describe rest any further.
So now is the complicated bit I iterated on for a long time, how to compute the type of the list when modified and ensure that a parallel structure is built. I actually started by writing a simple interface induction as above that computed the type, and it went relatively well:
interface ModTypeInterface mem where
modTypeInterface : Maybe Nat -> mem -> SignedNat x v -> Maybe BrokenMemory
public export
implementation ModTypeInterface (Memory s t rest) where
modTypeInterface Nothing (MEnd s v) _ = Just (broken s v Nothing)
modTypeInterface Nothing (MWord s v r) _ =
let
t : Maybe BrokenMemory
t = modTypeInterface Nothing r (Pos 0)
in
Just (broken s v t)
modTypeInterface (Just Z) (MEnd s v) (Pos e) =
Just (broken s v Nothing)
modTypeInterface (Just Z) (MEnd s v) (Neg e) =
Just (broken s v Nothing)
modTypeInterface (Just Z) (MWord s v r) (Pos e) =
let
t : Maybe BrokenMemory
t = modTypeInterface Nothing r (Pos e)
in
Just (broken False e t)
modTypeInterface (Just Z) (MWord s v r) (Neg e) =
let
t : Maybe BrokenMemory
t = modTypeInterface Nothing r (Pos e)
in
Just (broken True e t)
modTypeInterface (Just (S n)) (MEnd s v) a =
Just (broken s v Nothing)
modTypeInterface (Just (S n)) (MWord s v r) (Pos e) =
let
t : Maybe BrokenMemory
t = modTypeInterface (Just n) r (Pos e)
in
Just (broken s v t)
modTypeInterface (Just (S n)) (MWord s v r) (Neg e) =
let
t : Maybe BrokenMemory
t = modTypeInterface (Just n) r (Neg e)
in
Just (broken s v t)
Long but not surprising, what came later though was not great, in that while the value that goes along with this is easy to compute, one runs into a problem; the “rest” returned may not have enough information to show idris that it is the same type as what’s claimed, despite that we’ve got two parallel implementations that do that, so that’s where this gets tricky. I needed to take my BrokenMemory which doesn’t encode the type, and use type level information available at each stage to ensure that the result is the type I claim.
modRamValue Nothing = ()
modRamValue (Just b) = unbrokenNext b
public export
modifyRam : ModTypeInterface mem => {n : Nat} -> MemoryAddress n -> (m : mem) -> (a : SignedNat q x) -> typeOfModRam (modTypeInterface (Just n) m a)
modifyRam ma m a = modRamValue (modTypeInterface (Just n) m a)
So the type here is returned from TypeOfRam and the value is created by modRamValue via a BrokenMemory list.
I had a bit of an inspiration though: since proofs are functions yielding (= a a) at the type level, I included a function in each broken that, given the computed type for the tail, produces the proof that the tail meets our requirement, allowing us to rewrite the return value of the function using the tail so that the requirement to match is elided at that level:
public export
intoMemory : (a : Bool) -> (b : Nat) -> (Type -> Type)
intoMemory a b = Memory a b
public export
proofIntoMemoryAddsMemory : (a : Bool) -> (b : Nat) -> (t : Type) -> intoMemory a b t = Memory a b t
proofIntoMemoryAddsMemory a b t = Refl
public export
proofOfIntoMemory : (a : Bool) -> (b : Nat) -> (f : Type -> Type) -> (f = intoMemory a b) -> (t : Type) -> f t = Memory a b t
proofOfIntoMemory a b f prf t =
rewrite prf in
Refl
broken b n r =
let
imp : (t : Type) -> (intoMemory b n) t = Memory b n t
imp = proofOfIntoMemory b n (intoMemory b n) Refl
in
Broken b n (intoMemory b n) imp r
The purpose of this proof is to tell idris that while what we’re giving is named by an opaque type variable, the result actually matches Memory s v rest to one more depth level, so by using this proof to rewrite the result from a function downstream, we can say “it’s ok, this thing matches so you don’t need to require the match in the result”. Once the result type is rewritten the value we gave matches.
And experimented with this assistant style until there were no holes :-O
convertTail : (b : BrokenMemory) -> typeOfBroken b -> Memory (getSignFromBroken b) (getMagFromBroken b) (getNextTypeFromBroken b)
convertTail b@(Broken s v mt prf x@(Just rr)) r =
rewrite sym (mwordSatisfiesTypeOfBrokenR b) in
let
ctail = convertTail rr (unbrokenNext rr)
res = MWord s v ctail
in
rewrite prf (typeOfBroken rr) in
rewrite mwordSatisfiesTypeOfBrokenR rr in
res
convertTail b@(Broken s v mt prf Nothing) r =
rewrite sym (mwordSatisfiesTypeOfBrokenR b) in
rewrite prf Unit in
let
res = MEnd s v
in
res
unbrokenNext b@(Broken s v mt prf Nothing) =
rewrite prf Unit in
MEnd s v
unbrokenNext b@(Broken s v mt prf (Just r)) =
let
next = unbrokenNext r
in
rewrite prf (typeOfBroken r) in
rewrite mwordSatisfiesTypeOfBrokenR r in
let
res = MWord s v (convertTail r next)
in
res
And applying this allows the memory to be mutated and tracked at the type level!
4/4: Building Main (src/Main.idr)
λΠ> mem
MWord False 3 (MWord False 2 (MEnd False 5))
λΠ> modifyRam (MAddr 1) mem (Neg 17)
MWord False 3 (MWord True 17 (MEnd False 5))
λΠ> :t (modifyRam (MAddr 1) mem (Neg 17))
modifyRam (MAddr 1) mem (Neg 17) : Memory False 3 (Memory True 17 (Memory False 5 ()))
λΠ>
That is some lambda pie indeed.
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 to larger companies in software have is timeline as powerplay; another manager says they can do it faster, our manager thinks they’ll look better with a better estimate, announcing this feature on a certain date works nicely with our media and PR schedule. In any of these cases and many more, extrinsic forces put pressure on a software team to deliver on a specific date for reasons that aren’t related to a need for the functionality itself. This is not as uncommon as one would hope.
That timelines and planning are a necessary aspect of software development are taken as assumed. Somewhere there’s a big ledger and we have to know what each line item is. How is that information used? It’s complicated; meetings are had and the data are discussed as a backdrop. Negotiations, golf games, offsites and late night ungrammatical texts are had. Ultimately, decisions about this data are taken in the moment, according to gut feelings almost 100% of the time.
Even worse, let’s say a company is working to produce a single software title, such as a company producing an MMO, the company lives and dies by this release, but what is actually the purpose of tracking, of planning? Is there any expense the company wouldn’t go to to ship? Is there any circumstance anyone can foresee early in the process that would cause some definite change? We can try to control scope as we go, but development is likely already moving in a strictly priority based order, so it’s unclear what decisions can be made based on macro-scoped information about the project’s timeline that isn’t already covered simply by prioritization. We can ask to cut more corners earlier at times or crunch harder earlier, but it’s unclear what else macro-scale time planning can give us from a dev-team perspective, and those are arguably the least healthy responses one might have.
What I’m going to propose does 2 things:
If it’s ok that pushing for a shorter timeline without changing scope or scaling back the project is completely without risk, then there’s no need for any of this; you just assign every project a symbolic amount of time, roughly in the same order of magnitude to the actual effort and you just keep doing it until it gets done. This is by far the most common way projects are budgeted. Decisions about changes to the project are usually taken in the moment, either near the end of or after the original timeline. I’d argue that in this environment, the project only needs progress reports at the 3/4 point, at the end of the original timeline, and at every 25% overrun thereafter.
If on the other hand, there’s a desire for the overhead of timekeeping, tracking, producing estimates and plans, and for there to be risk associated with pushing for both shorter and longer time, then this is actually a sincere proposal.
To start, before any work is started, we must set a trailing stop for the project. This is the percent overrun that the organization is willing to accept without complaint, and it’d actually be fine for it to be anything from 1000% to -99%. Literally any value in this range can be accommodated since the rest is all math.
Now we make an honest effort to estimate the project as normal, and come up with an estimated time as normal. We try to scale the point values in this estimate so that we have a reasonable belief that we can keep the burndown chart curve above the straight line between 0 time and 0 completion at the beginning, and 100% +allowed_overrun and 100% completion at the end. We can use techniques that are rarely used today, such as building in rampup times when the team needs to change focus that estimate for low point delivery over that time to control the shape of the curve.
The important part is that when (or if) we start the project, with management approval for the indicated timeline, we all agree that we will stop working on the project and accept the idea that the project may fail or be shelved if the lines cross. The one hard and fast rule in this is that work on the project halts and we come back to the table when the burndown chart indicates that we have gone over our margin, regardless of the circumstances, because that distributes risk equally among the stakeholders when speaking about the project’s timeline, and forces a healthy choice (a short break at least) when the project is floundering.
There are two price discovery mechanisms at work here; one is point scaling. If we work on a project for a while and it halts due to this mechanism, we actually know a lot more about our estimates. The dev team has good evidence that the estimates are not conservative enough and we should scale them better. Managers, PMs C-levels know that pushing for unrealistic goals will only land them back in front of the board to try to sell the project again (most likely with a rescaled remaining timeline, since the project is already going over), so smooth operation is made preferable to optimism. We can discover hidden assumptions and flexibilities among the participants when we come back together to discuss restarting the project. Perhaps requirements are more flexible than was originally stated? Perhaps the organization wants to look good on paper in cost terms but ultimately has no option but to do what it takes to complete the project as described. In either scenario, we repeat a simple process to tease this out.
I believe applying a process like this on top of the considerable estimation and tracking work that are basically universal in software projects can help everyone involved and remove some of the tensions that develop between participants. Restarting a project can be healthy in order to discover the best way to estimate.
Imagine that a project is started, everyone is optimistic and the timeline seems reasonable, but early on we notice that we’ve systematically biased our estimates toward optimism without intending to. A few weeks in, the tripwire goes off and we look at the plan again. Unlike the more traditional scenario where the dev team would face a lot of scrutiny for inconveniencing everyone by making a promise (the original timeline) and then suddenly trying to change it, it’ll be understood that what’s happening is based on data, and is a real event. It’s an agreement everyone made at the beginning, and it’s an easy time for the dev team’s management facing people to say “we’re re-scaling the estimate because it looks like it wasn’t as realistic as we hoped before, and we can be glad we caught this early, not 3 or 6 months from now. The new one is better for having had the opportunity to respond to real world information.”
Ultimately, my hope is that when we have the possibility to impose a burden on one party, we impose risk on another, that’s the framework at play here, and I believe it is not only morally and ethically sound, but also contributes to greater understanding and cooperation between people who may otherwise have very opposed incentives and goals within organizations.
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 to larger companies in software have is timeline as powerplay; another manager says they can do it faster, our manager thinks they’ll look better with a better estimate, announcing this feature on a certain date works nicely with our media and PR schedule. In any of these cases and many more, extrinsic forces put pressure on a software team to deliver on a specific date for reasons that aren’t related to a need for the functionality itself. This is not as uncommon as one would hope.
That timelines and planning are a necessary aspect of software development are taken as assumed. Somewhere there’s a big ledger and we have to know what each line item is. How is that information used? It’s complicated; meetings are had and the data are discussed as a backdrop. Negotiations, golf games, offsites and late night ungrammatical texts are had. Ultimately, decisions about this data are taken in the moment, according to gut feelings almost 100% of the time.
Even worse, let’s say a company is working to produce a single software title, such as a company producing an MMO, the company lives and dies by this release, but what is actually the purpose of tracking, of planning? Is there any expense the company wouldn’t go to to ship? Is there any circumstance anyone can foresee early in the process that would cause some definite change? We can try to control scope as we go, but development is likely already moving in a strictly priority based order, so it’s unclear what decisions can be made based on macro-scoped information about the project’s timeline that isn’t already covered simply by prioritization. We can ask to cut more corners earlier at times or crunch harder earlier, but it’s unclear what else macro-scale time planning can give us from a dev-team perspective, and those are arguably the least healthy responses one might have.
What I’m going to propose does 2 things:
If it’s ok that pushing for a shorter timeline without changing scope or scaling back the project is completely without risk, then there’s no need for any of this; you just assign every project a symbolic amount of time, roughly in the same order of magnitude to the actual effort and you just keep doing it until it gets done. This is by far the most common way projects are budgeted. Decisions about changes to the project are usually taken in the moment, either near the end of or after the original timeline. I’d argue that in this environment, the project only needs progress reports at the 3/4 point, at the end of the original timeline, and at every 25% overrun thereafter.
If on the other hand, there’s a desire for the overhead of timekeeping, tracking, producing estimates and plans, and for there to be risk associated with pushing for both shorter and longer time, then this is actually a sincere proposal.
To start, before any work is started, we must set a trailing stop for the project. This is the percent overrun that the organization is willing to accept without complaint, and it’d actually be fine for it to be anything from 1000% to -99%. Literally any value in this range can be accommodated since the rest is all math.
Now we make an honest effort to estimate the project as normal, and come up with an estimated time as normal. We try to scale the point values in this estimate so that we have a reasonable belief that we can keep the burndown chart curve above the straight line between 0 time and 0 completion at the beginning, and 100% +allowed_overrun and 100% completion at the end. We can use techniques that are rarely used today, such as building in rampup times when the team needs to change focus that estimate for low point delivery over that time to control the shape of the curve.
The important part is that when (or if) we start the project, with management approval for the indicated timeline, we all agree that we will stop working on the project and accept the idea that the project may fail or be shelved if the lines cross. The one hard and fast rule in this is that work on the project halts and we come back to the table when the burndown chart indicates that we have gone over our margin, regardless of the circumstances, because that distributes risk equally among the stakeholders when speaking about the project’s timeline, and forces a healthy choice (a short break at least) when the project is floundering.
There are two price discovery mechanisms at work here; one is point scaling. If we work on a project for a while and it halts due to this mechanism, we actually know a lot more about our estimates. The dev team has good evidence that the estimates are not conservative enough and we should scale them better. Managers, PMs C-levels know that pushing for unrealistic goals will only land them back in front of the board to try to sell the project again (most likely with a rescaled remaining timeline, since the project is already going over), so smooth operation is made preferable to optimism. We can discover hidden assumptions and flexibilities among the participants when we come back together to discuss restarting the project. Perhaps requirements are more flexible than was originally stated? Perhaps the organization wants to look good on paper in cost terms but ultimately has no option but to do what it takes to complete the project as described. In either scenario, we repeat a simple process to tease this out.
I believe applying a process like this on top of the considerable estimation and tracking work that are basically universal in software projects can help everyone involved and remove some of the tensions that develop between participants. Restarting a project can be healthy in order to discover the best way to estimate.
Imagine that a project is started, everyone is optimistic and the timeline seems reasonable, but early on we notice that we’ve systematically biased our estimates toward optimism without intending to. A few weeks in, the tripwire goes off and we look at the plan again. Unlike the more traditional scenario where the dev team would face a lot of scrutiny for inconveniencing everyone by making a promise (the original timeline) and then suddenly trying to change it, it’ll be understood that what’s happening is based on data, and is a real event. It’s an agreement everyone made at the beginning, and it’s an easy time for the dev team’s management facing people to say “we’re re-scaling the estimate because it looks like it wasn’t as realistic as we hoped before, and we can be glad we caught this early, not 3 or 6 months from now. The new one is better for having had the opportunity to respond to real world information.”
Ultimately, my hope is that when we have the possibility to impose a burden on one party, we impose risk on another, that’s the framework at play here, and I believe it is not only morally and ethically sound, but also contributes to greater understanding and cooperation between people who may otherwise have very opposed incentives and goals within organizations.
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 of rules. I was pretty happy with the result but less so the workflow to build it; the official libtooling documentation basically tells you to build tooling programs in the llvm tree. When I’ve had the chance to recommend libtooling to someone to solve a problem (or to be like me and use my rules), I really can’t recommend it as a common workflow because of the lack of documentation for a normal dev workflow and the rate of change in the clang api… It’s a mess for anyone whose 9–5 isn’t packaging up clang for google or apple.
Enter https://github.com/deech/libclang-static-build .
It’s very self contained and you can incorporate it easily into cmake projects (and you’re probably building clang related stuff with cmake anyway).
While I’m not a cmake maven, using it went pretty simply
cmake_minimum_required(VERSION 3.13)
include(${CMAKE_ROOT}/Modules/ExternalProject.cmake)
set(LIBCLANG_INSTALL "libclang-copied")
ExternalProject_Add(libclang-static-build
\tDOWNLOAD_DIR "libclang-static-build"
\tINSTALL_DIR "${LIBCLANG_INSTALL}"
\tGIT_REPOSITORY "https://github.com/deech/libclang-static-build"
\tGIT_TAG "0cae8e85ef1ad951e1bb560e1eadcd64b2f0828e"
\tCMAKE_ARGS "-DCMAKE_INSTALL_PREFIX=${LIBCLANG_INSTALL}"
\t)
project(noglob)
add_compile_options("-fno-rtti")
add_executable(noglob
DisallowGlobals.cpp
DisallowNewDelete.cpp
DisallowNonAbstract.cpp
DisallowCoupling.cpp
tool.cpp
)
ExternalProject_Get_Property(libclang-static-build binary_dir)
include_directories(
\t${binary_dir}/_deps/clang_sources-src/include
\t${binary_dir}/_deps/libclang_prebuilt-src/include
\t)
add_dependencies(noglob libclang-static-build)
target_link_libraries(noglob "-L${binary_dir}" "-lclang_static_bundled" -lpthread)
Just a bit of hooking into libclang-static-build and you can ignore that your distro somehow manages to ship both with a libclang that’s newer than what you built with last time (with breaking api changes) but not new enough to take advantage of features you’ve recently read about in the docs.
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 of rules. I was pretty happy with the result but less so the workflow to build it; the official libtooling documentation basically tells you to build tooling programs in the llvm tree. When I’ve had the chance to recommend libtooling to someone to solve a problem (or to be like me and use my rules), I really can’t recommend it as a common workflow because of the lack of documentation for a normal dev workflow and the rate of change in the clang api… It’s a mess for anyone whose 9–5 isn’t packaging up clang for google or apple.
Enter https://github.com/deech/libclang-static-build .
It’s very self contained and you can incorporate it easily into cmake projects (and you’re probably building clang related stuff with cmake anyway).
While I’m not a cmake maven, using it went pretty simply
cmake_minimum_required(VERSION 3.13)
include(${CMAKE_ROOT}/Modules/ExternalProject.cmake)
set(LIBCLANG_INSTALL "libclang-copied")
ExternalProject_Add(libclang-static-build
\tDOWNLOAD_DIR "libclang-static-build"
\tINSTALL_DIR "${LIBCLANG_INSTALL}"
\tGIT_REPOSITORY "https://github.com/deech/libclang-static-build"
\tGIT_TAG "0cae8e85ef1ad951e1bb560e1eadcd64b2f0828e"
\tCMAKE_ARGS "-DCMAKE_INSTALL_PREFIX=${LIBCLANG_INSTALL}"
\t)
project(noglob)
add_compile_options("-fno-rtti")
add_executable(noglob
DisallowGlobals.cpp
DisallowNewDelete.cpp
DisallowNonAbstract.cpp
DisallowCoupling.cpp
tool.cpp
)
ExternalProject_Get_Property(libclang-static-build binary_dir)
include_directories(
\t${binary_dir}/_deps/clang_sources-src/include
\t${binary_dir}/_deps/libclang_prebuilt-src/include
\t)
add_dependencies(noglob libclang-static-build)
target_link_libraries(noglob "-L${binary_dir}" "-lclang_static_bundled" -lpthread)
Just a bit of hooking into libclang-static-build and you can ignore that your distro somehow manages to ship both with a libclang that’s newer than what you built with last time (with breaking api changes) but not new enough to take advantage of features you’ve recently read about in the docs.
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 types. This probably isn’t strictly accurate (for example, it’s possible for these “rows” to have ids named by types as I understand it, unlike purescript), but the analogy holds pretty well when they aren’t noted by IDs since each row type matches an item of compatible type in the collection of rows.
With Effect, there are basically these states:
That’s complicated, and I’ll try to explain the various parts necessary for this to function.
The form of the effects given in the idris examples have the following general outline:
whew!!*
After that, we’ve got an EFFECT we can use. You can write a do block in the regime of your effect.
Now I’ll explain the code in more detail. First, what was the goal of all this? I’m interested in idris as a venue for software verification and using formal proof for writing code. In particular, I was curious after my previous experiments with modelling dynamic state in monads (which, while successful, also makes for very complex proofs), I could simplify what needs to be done by requiring that imperative code containing assertions also contains proof that the assertions never fire. This take distributes proof obligations, and should make proofs more modular. I had to start by discovering how effects work in idris, since I wanted the state of the assertions to be kept track of by the type system. Since reading the ‘door’ examples and hangman examples existing for idris, an effect seemed a natural way to make idris aware of my intentions.
doTryAssert : Eff () [ASSERTION NotFailed] [ASSERTION NotFailed]
doTryAssert =
do
let x = True -- Not well typed if x is False
assert x (trueEqualsTrue x)
let y = 2 /= 3 -- Not well typed for 3 /= 3
assert y (twoIsLessThanThree)
In my case, I was interested in modelling assertions in imperative code as an effect that always has an expected state of ASSERTION NotFailed. Therefore, if any assert can get False, the outcome state will possibly be ASSERTION Failed and the code won’t compile. Idris must believe that each assertion receives True at the call site via proof.
It can be invoked by the ugly but usable:
runAssertions : Eff () [ASSERTION NotFailed]
runAssertions = do
doTryAssert
main : IO ()
main = run runAssertions
Figuring out the appropriate magic to set this up took a lot of time and punching compile errors. I still don’t fully understand the interplay between Default and Eff here.
So starting with (0)
data AssertionState = NotFailed | Failed
Nothing could be simpler than a piece of data we want idris to keep track of.
On to (1)
data AssertionInfo : AssertionState -> Type where
DI : AssertionInfo s
Very usual idris code to cause each state that can be taken by AssertionState to turn into a Type we can use for Type level code.
On to (2)
data AssertionEff : Effect where
FailAssertion :
sig AssertionEff ()
(AssertionInfo NotFailed)
(AssertionInfo Failed)
OkAssertion :
sig AssertionEff ()
(AssertionInfo NotFailed)
(AssertionInfo NotFailed)
This sets out the methods of our effect, that is; what it can do and the pre and post-conditions of each method. Note that there is a 3-argument form of sig that does not take a precondition. I did not need to use it here. Using a function to give the type of a GADT label isn’t common in most code, but a bit of thinking indicates that any function yielding Type would be fine.
(3)
ASSERTION : AssertionState -> EFFECT
ASSERTION t = MkEff (AssertionInfo t) AssertionEff
This heavily reminds me of effect types from purescript, pre 0.12. The constructor takes a datum that we defined in (0), wraps it as (1) and throws in (2) to the MkEff constructor to give it all the info it needs. ASSERTION will appear in code our hypothetical user uses.
(4)
implementation Handler AssertionEff IO where
handle res FailAssertion k = do
putStrLn "Assertion failed"
k () DI
handle res OkAssertion k = do
k () DI
An implementation of the Handler typeclass for AssertionEff (2) in which we take actions (in this case, writing a message when we hit a failed assertion) and also changing to a new state (k takes two arguments, the returned, “residual status” from scsi parlance, a value that is picked up by “<-” in monadic captures; a string for getline for example), and a Type that represents the state of the Effect system after this command is complete. In an audio system, this might indicate that the system is in a buffer full state and can’t take more samples, or that the buffer is below the low water mark and new samples are needed. That the video system is late for a deadline and that draw calls marked low priority will be dropped, that the bank represented by the other end of a websocket is close to overdraw and we can’t do more transactions. Anything the imagination can come up with. In our case, it just indicates whether the most recent assertion failed. To do this, we “call” the FailAssertion alternative of (2) to cause it’s effect to happen, which includes a postcondition of ASSERTION Failed. Since we’re expecting ASSERTION NotFailed, this is an impossible state and the program will not compile.
(5)
implementation Default (AssertionInfo NotFailed) where
default = DI
This an implementation of the Default typeclass for (AssertionInfo NotFailed), in general, it will return the start state of the effect when one isn’t present in the Eff environment to begin with. If variables or arguments were present in our effect state, we’d have to supply them concretely here.
(6) finally
assert : (x : Bool) -> (prf : (x = True)) -> Eff () [ASSERTION NotFailed] [ASSERTION (if x then NotFailed else Failed)]
assert False _ = call FailAssertion
assert True Refl = call OkAssertion
A function for each method we can use in our effect. These are normal functions that carry the actual outcome states of the effect. In my case, I gave a proof that assert False is uninhabited so we can guarantee that assert never transitions the effect to ASSERTION Failed. We leave the possibility open that some code might want to use assert in a different way, and a different method of ASSERTION might not take this proof.
So there we have a program that is well typed only if every instance of assert comes with a proof that the assertion input is True. I believe this will be a help in actually using idris for formal verification as it can be used in a really incremental way like this.
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 types. This probably isn’t strictly accurate (for example, it’s possible for these “rows” to have ids named by types as I understand it, unlike purescript), but the analogy holds pretty well when they aren’t noted by IDs since each row type matches an item of compatible type in the collection of rows.
With Effect, there are basically these states:
That’s complicated, and I’ll try to explain the various parts necessary for this to function.
The form of the effects given in the idris examples have the following general outline:
whew!!*
After that, we’ve got an EFFECT we can use. You can write a do block in the regime of your effect.
Now I’ll explain the code in more detail. First, what was the goal of all this? I’m interested in idris as a venue for software verification and using formal proof for writing code. In particular, I was curious after my previous experiments with modelling dynamic state in monads (which, while successful, also makes for very complex proofs), I could simplify what needs to be done by requiring that imperative code containing assertions also contains proof that the assertions never fire. This take distributes proof obligations, and should make proofs more modular. I had to start by discovering how effects work in idris, since I wanted the state of the assertions to be kept track of by the type system. Since reading the ‘door’ examples and hangman examples existing for idris, an effect seemed a natural way to make idris aware of my intentions.
doTryAssert : Eff () [ASSERTION NotFailed] [ASSERTION NotFailed]
doTryAssert =
do
let x = True -- Not well typed if x is False
assert x (trueEqualsTrue x)
let y = 2 /= 3 -- Not well typed for 3 /= 3
assert y (twoIsLessThanThree)
In my case, I was interested in modelling assertions in imperative code as an effect that always has an expected state of ASSERTION NotFailed. Therefore, if any assert can get False, the outcome state will possibly be ASSERTION Failed and the code won’t compile. Idris must believe that each assertion receives True at the call site via proof.
It can be invoked by the ugly but usable:
runAssertions : Eff () [ASSERTION NotFailed]
runAssertions = do
doTryAssert
main : IO ()
main = run runAssertions
Figuring out the appropriate magic to set this up took a lot of time and punching compile errors. I still don’t fully understand the interplay between Default and Eff here.
So starting with (0)
data AssertionState = NotFailed | Failed
Nothing could be simpler than a piece of data we want idris to keep track of.
On to (1)
data AssertionInfo : AssertionState -> Type where
DI : AssertionInfo s
Very usual idris code to cause each state that can be taken by AssertionState to turn into a Type we can use for Type level code.
On to (2)
data AssertionEff : Effect where
FailAssertion :
sig AssertionEff ()
(AssertionInfo NotFailed)
(AssertionInfo Failed)
OkAssertion :
sig AssertionEff ()
(AssertionInfo NotFailed)
(AssertionInfo NotFailed)
This sets out the methods of our effect, that is; what it can do and the pre and post-conditions of each method. Note that there is a 3-argument form of sig that does not take a precondition. I did not need to use it here. Using a function to give the type of a GADT label isn’t common in most code, but a bit of thinking indicates that any function yielding Type would be fine.
(3)
ASSERTION : AssertionState -> EFFECT
ASSERTION t = MkEff (AssertionInfo t) AssertionEff
This heavily reminds me of effect types from purescript, pre 0.12. The constructor takes a datum that we defined in (0), wraps it as (1) and throws in (2) to the MkEff constructor to give it all the info it needs. ASSERTION will appear in code our hypothetical user uses.
(4)
implementation Handler AssertionEff IO where
handle res FailAssertion k = do
putStrLn "Assertion failed"
k () DI
handle res OkAssertion k = do
k () DI
An implementation of the Handler typeclass for AssertionEff (2) in which we take actions (in this case, writing a message when we hit a failed assertion) and also changing to a new state (k takes two arguments, the returned, “residual status” from scsi parlance, a value that is picked up by “<-” in monadic captures; a string for getline for example), and a Type that represents the state of the Effect system after this command is complete. In an audio system, this might indicate that the system is in a buffer full state and can’t take more samples, or that the buffer is below the low water mark and new samples are needed. That the video system is late for a deadline and that draw calls marked low priority will be dropped, that the bank represented by the other end of a websocket is close to overdraw and we can’t do more transactions. Anything the imagination can come up with. In our case, it just indicates whether the most recent assertion failed. To do this, we “call” the FailAssertion alternative of (2) to cause it’s effect to happen, which includes a postcondition of ASSERTION Failed. Since we’re expecting ASSERTION NotFailed, this is an impossible state and the program will not compile.
(5)
implementation Default (AssertionInfo NotFailed) where
default = DI
This an implementation of the Default typeclass for (AssertionInfo NotFailed), in general, it will return the start state of the effect when one isn’t present in the Eff environment to begin with. If variables or arguments were present in our effect state, we’d have to supply them concretely here.
(6) finally
assert : (x : Bool) -> (prf : (x = True)) -> Eff () [ASSERTION NotFailed] [ASSERTION (if x then NotFailed else Failed)]
assert False _ = call FailAssertion
assert True Refl = call OkAssertion
A function for each method we can use in our effect. These are normal functions that carry the actual outcome states of the effect. In my case, I gave a proof that assert False is uninhabited so we can guarantee that assert never transitions the effect to ASSERTION Failed. We leave the possibility open that some code might want to use assert in a different way, and a different method of ASSERTION might not take this proof.
So there we have a program that is well typed only if every instance of assert comes with a proof that the assertion input is True. I believe this will be a help in actually using idris for formal verification as it can be used in a really incremental way like this.