Skip to content

Instantly share code, notes, and snippets.

View dorchard's full-sized avatar

Dominic Orchard dorchard

292 followers · 42 following
View GitHub Profile
@dorchard
dorchard / Makefile.template
Created February 14, 2018 10:19
A script that generates a simple makefile (with no dependency tracking) for latex / bibtex that I use all the time.
default: quick
quick:
pdflatex paper.tex
full:
pdflatex paper.tex
bibtex paper
pdflatex paper.tex
pdflatex paper.tex
@dorchard
dorchard / CBNLambdaEff.hs
Last active November 15, 2018 20:40
A Haskell implementation of the categorical semantics for the effectful CBN lambda calculus
{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls #-}
{-
A Haskell-based implementation of the monadic semantics for the
simply-typed Call-By-Name computational lambda calculus, following
Moggi's 'Computational lambda-calculus and monads' (1989) (technical report version)
but for the typed calculus (rather than untyped as in this paper).
Category theory seminar, Programming Languages and Systems group,
@dorchard
dorchard / gist:2ef456b5c9bccd5bbe3c0c2c646d233a
Last active August 16, 2017 22:39
Auto highlighting with lhs2TeX
% Highlight comments in darkgreen
\definecolor{darkgreen}{rgb}{0,0.5,0}
\newcommand{\commenthighlight}{\color{darkgreen}\quad-{}- }
\let\onelinecomment=\commenthighlight
% Highlight constructors in darkblue
\definecolor{darkblue}{rgb}{0,0,0.5}
\renewcommand{\Conid}[1]{\textcolor{darkblue}{\textit{#1}}}
@dorchard
dorchard / Category.agda
Last active August 17, 2017 14:13
Definition of a category as an Agda record: level polymorphic in the objects and arrows
module Category where
open import Level
open import Relation.Binary.PropositionalEquality
open Level
record Category {lobj : Level} {larr : Level} : Set (suc (lobj ⊔ larr)) where
field obj : Set lobj
arr : (src : obj) -> (trg : obj) -> Set larr
@dorchard
dorchard / gist:8d726882bb3cdbb5bd44e8ffc14e0ff4
Created August 10, 2016 09:58
type families for extra information on pretty printer
class Pretty t where
type ExtraInfo t
pprint :: FortranVersion -> t -> ExtraInfo t -> Doc
instance Pretty (Expression a) where
type ExtraInfo (Expression a) = ()
pprint v e () = ...
instance Pretty (Block a) where
type ExtraInfo (Block a) = Int -- indent level
@dorchard
dorchard / CatToMon.agda
Last active September 2, 2016 10:37
Proofs for inducing monoids from categories
module CatToMon where
open import Data.Product
open import Data.Sum
open import Data.Unit
open import Data.Empty
open import Level
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Relation.Binary
@dorchard
dorchard / cloudsession.hs
Created April 29, 2015 13:37
Prototype of type-enforced linear behaviour for Cloud Haskell
{-
Proof of concept for adding linearity constraints on the communication-patterns
of Cloud Haskell.
Uses the 'effect-monad' package for embedding effect systems in Haskell types:
cabal install effect-monad
-}
@dorchard
dorchard / jam-evening
Created October 15, 2014 23:07
Evening jam with Sonic Pi
define :sequence do |xs,tp|
xs.each do |ys|
in_thread do
if (ys[0] == :zawa || ys[0] == :tb303 || ys[0] == :pulse || ys[0] == :s) then
synth = ys[0]
zs = ys[1..-1]
else
synth = :tri
zs = ys
end
@dorchard
dorchard / gist:7ed17c66677a64d069ff
Last active August 30, 2016 05:53
My QuickCheck instance for Data.Matrix (square matrices)
instance (Arbitrary a) => Arbitrary (Matrix a) where
-- NB: for square matrices
arbitrary = sized (\n -> do xs <- vectorOf (n*n) arbitrary
return $ matrix n n (\(i, j) -> xs !! ((i-1)*n + (j-1))))
@dorchard
dorchard / gist:abd86980909e7e910c79
Created July 24, 2014 12:58
Profiling builds with GHC, useful sites
* https://www.haskell.org/ghc/docs/7.8.2/html/users_guide/prof-compiler-options.html
GHC profiling options
* http://lambdor.net/?p=258
Describes how to install profile libraries
* http://www.haskell.org/pipermail/haskell-cafe/2009-April/060482.html