Skip to content

Instantly share code, notes, and snippets.

View dorchard's full-sized avatar

Dominic Orchard dorchard

View GitHub Profile
@dorchard
dorchard / gist:4132742
Created November 22, 2012 20:08
Comonad for protected operations
> {-# LANGUAGE QuasiQuotes #-}
> {-# LANGUAGE EmptyDataDecls #-}
> import Control.Comonad
> import Language.Haskell.Codo
> data Input a
> data Output a
@dorchard
dorchard / gist:4df935ebad0807c47b80
Last active August 29, 2015 14:04
type level implicit parameters example (speculation)
Consider a data type representing syntax trees.
> data Expr = BinOp Expr Expr | Unop Expr
> data Stmt = Seq Stmt Stmt | Assign String Expr
Let's say I want this in a module, but I also want to be able to arbitrarily extend this AST type
in modules that import it. So, I add an extra constructor and a type parameter
to all the data type definitions:
> data Expr ext = BinOp (Expr ext) (Expr ext) | Unop (Expr ext) | Ext ext
@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
@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 / 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 / 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 / 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 / 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 / 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: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}}}