Dominic Orchard dorchard

These are a list of writing "strategies" that can be helpful when writing (e.g., to get going or to get unstuck). A meta-strategy is to jump between strategies: Feeling stuck? Then pick another strategy. Each strategy can be applied at different granularities, e.g. for an entire book or paper, or chapter or section, or just a subsection or paragraph. Different approaches may work better for you in different phases of a project.

In all cases, remember to avoid premature optimisation; re-writing and editing comes later.

Lastly, always be writing. Writing is like a muscle. Getting comfortable with writing comes with practice.

	# Run with
	#
	# python graph.py makefilename
	#
	# which generates dependencies.dot which can be compiled with graphviz
	# to a png via:
	#
	# dot -Tpng dependencies.dot -o dependencies.png
	#
	#

	from typing import TYPE_CHECKING

	flag : bool = True

	def greet(name: str) -> None:
	"""Say hello to everyone"""
	print("Hi " + name)
	return None

	greet("Manchester")

	import Data.Bits
	import Data.Word
	import Foreign ( Ptr, new, castPtr, Storable(peek, poke) )
	import System.IO.Unsafe
	import Unsafe.Coerce

	qsqrt :: Float -> Float
	qsqrt x = 1 / qRsqrt x

	qsqrt' :: Float -> Float

	\documentclass[10pt]{article}
	\usepackage{amssymb} %maths
	\usepackage{amsmath} %maths
	\usepackage[utf8]{inputenc} %useful to type directly diacritic characters
	\usepackage[margin=4cm]{geometry}

	\title{Indexed natural numbers}
	\author{Dominic Orchard}

	\begin{document}

	program example
	use naryfunc
	implicit none
	! Outputs 2 6 24
	write(,) mult(2), mult(2, 3), mult(2, 3, 4)
	end program example

	module Flexible where

	-- Exploring flexible graded monads, based on the work of Katsumata, McDermott, Uustalu and Wu
	-- https://dylanm.org/drafts/flexibly-graded-presentations.pdf

	open import Function

	_⇒_ : {E : Set} -> (E -> Set) -> (E -> Set) -> Set
	_⇒_ {E} X Y = forall (e : E) -> X e -> Y e

	-- # Examples from the paper 'Linearity and Uniqueness: An Entente Cordiale'

	-- ## Linearity (see Section 2, Key ideas)

	-- Linearity (with cake)

	data Cake = Cake
	data Happy = Happy

	eat : Cake -> Happy

	module Main where

	import System.Environment (getArgs)
	import System.Exit (exitFailure)
	import Data.List (intercalate)

	-- Scrub automata
	scrub :: String -> [String]
	scrub [] = []
	scrub ('m':'a':'i':'l':'t':'o':':':rest) =

	module Empty where

	open import Data.Empty
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary
	open import Function.Inverse

	-- Empty type has only unequal elements
	uneq : (x y : ⊥) -> x ≢ y
	uneq () y prf

Dominic Orchard dorchard

Stream of consciousness