Skip to content

Instantly share code, notes, and snippets.

DaveCTurner / gist:37258febb57ddaef99b0
Created Jan 5, 2015
The 'ClearBefore' monoid, adding the ability to clear a log generated by a Writer.
View gist:37258febb57ddaef99b0
-- ClearBefore.hs
module ClearBefore where
import Data.Monoid
data ClearBefore a = ClearBefore Bool a
instance Monoid a => Monoid (ClearBefore a) where
mempty = ClearBefore False mempty
DaveCTurner / Main.hs
Created Feb 10, 2015
Haskell checkout kata
View Main.hs
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
module Main (main) where
import Control.Applicative
import Control.Monad
import Control.Monad.RWS
import Control.Monad.Trans.Either
DaveCTurner / Main.hs
Created Feb 11, 2015
Haskell checkout kata II
View Main.hs
{- a simpler implementation -}
module Main (main) where
import Test.Hspec
import Test.Hspec.QuickCheck
import Data.List
import qualified Data.Map as M
main :: IO ()
View gist:f977123b4498c4c64569
import Network.Socket
import System.Log.Logger
import System.Log.Handler.Syslog
openUDP = generalOpen
$ openlog_remote AF_INET "" 514
openDevLog = generalOpen
$ openlog_local "/dev/log"
View RandomPartition.hs
{-# LANGUAGE TupleSections #-}
import System.Random
import Control.Monad
import Data.List
import Text.Printf
main :: IO ()
main = do
let target = 4.7
DaveCTurner / gist:0614baa193da5880c99d
Created Aug 7, 2015
Using curl to add a PR to an issue
View gist:0614baa193da5880c99d
curl \
-XPOST --data-binary '{"issue":57,"head":"DaveCTurner:issue-57","base":"master"}' \
-H"Content-type: application/json" -u DaveCTurner -H"X-GitHub-OTP: nnnnnn" # asks for password
DaveCTurner / RailwayPeriod.hs
Last active Aug 29, 2015
Railway period calculations
View RailwayPeriod.hs
railwayPeriodStart :: Integer -> Integer -> Day
railwayPeriodStart yr pd
| pd == 1 = fromGregorian (yr - 1) 4 1
| otherwise = addDays (28 * pd) (dayZero yr)
railwayPeriodEnd :: Integer -> Integer -> Day
railwayPeriodEnd yr pd = addDays (-1) $ railwayPeriodStart yr' (pd' + 1)
where (yr', pd') = divMod (yr * 13 + pd) 13

Keybase proof

I hereby claim:

  • I am davecturner on github.
  • I am dcturner ( on keybase.
  • I have a public key ASAZdCj2ryspkWzhpFttsuadl4bwlg4fgKtJ_oaaHRjzowo

To claim this, I am signing this object:


Linearisability vs Sequential Consistency

Linearisability is a really rather strong property on a distributed system. There is a good discussion in [1] with some much more precise definitions on which I'm going to base this article.

The setup is a distributed system with some client processes which can perform operations (think: RPCs) on some remote data objects (think: a single-value register). The operations, being remote, take some nonzero amount of time between the client invoking the operation and being notified of its

DaveCTurner / Clock.thy
Created Feb 18, 2018
Safety, liveness and refinement of simple TLA+ clock specifications in Isabelle/HOL
View Clock.thy
theory Clock
imports "HOL-TLA.TLA"
lemma imp_imp_leadsto:
fixes F G :: stpred
fixes S :: temporal
assumes "⊢ F ⟶ G"
shows "⊢ S ⟶ (F ↝ G)"
apply (auto simp add: Valid_def)