Skip to content

Instantly share code, notes, and snippets.

View themattchan's full-sized avatar

themattchan

120 followers · 136 following
View GitHub Profile
@themattchan
themattchan / cps1.lhs
Last active May 20, 2019 04:08
https://parametri.city/blog/2019-05-19-cps-and-embeddings.html
@Iceland_jack: https://twitter.com/Iceland_jack/status/1130243968820830208
< begin :: ([a] -> res) -> res
< begin k = k []
< push :: [a] -> a -> ([a] -> res) -> res
< push as a k = k (a : as)
< add :: Num a => [a] -> ([a] -> res) -> res
< add (a:b:rest) k = k (b+a:rest)
@themattchan
themattchan / cursor.md
Created November 18, 2018 05:24
nixos: fix cursor size

Fix cursor size in nixos/linux

  1. Set your XCURSOR_SIZE to 32 (or desired size) in either your /etc/nixos/configuration.nix
environment.variables.XCURSOR_SIZE = "32";

or ~/.Xresources:

@themattchan
themattchan / fibo.hs
Last active March 31, 2018 21:40
{-# LANGUAGE DeriveFunctor #-}
import Control.Arrow ((&&&))
import Data.Bifunctor
-- Recursion Schemes for Dynamic Programming
-- Kabanov and Vene, Mathematics for Program Construction 2006
-- Basic stuff
newtype Mu f = In { out :: f (Mu f) }
@themattchan
themattchan / liquidlens.hs
Last active March 20, 2018 16:23
{-# LANGUAGE ExistentialQuantification, RankNTypes #-}
module Main where
{-@ LIQUID "--higherorder" @-}
import Language.Haskell.Liquid.ProofCombinators
import Data.Functor.Const
import Data.Functor.Identity
type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t)
@themattchan
themattchan / vector.hs
Last active October 30, 2017 04:14
{-# LANGUAGE
DataKinds
, TypeApplications
, TypeFamilies
, TypeOperators
, TypeInType
, KindSignatures
, ExistentialQuantification
, InstanceSigs
, ScopedTypeVariables
@themattchan
themattchan / Game.v
Created July 25, 2017 03:14 — forked from arthuraa/Game.v
Basic combinatorial game theory
Require Import Coq.Lists.List.
Open Scope bool_scope.
(* This is a direct definition of CGTs, using just one inductive type
instead of a pair of mutually-inductive types *)
Inductive game := Game {
left_moves : list game;
right_moves : list game
@themattchan
themattchan / Box.after.hs
Last active March 10, 2017 02:55
CSE 130 discussion week 6
{-# LANGUAGE FlexibleInstances #-}
-- | Fun with typeclasses
module Box where
import Prelude hiding (Functor(..), Applicative(..), Monad(..), Monoid(..), (.))
infixr 6 <>
--------------------------------------------------------------------------------
-- * Parametricity and typeclasses
-- see https://www.schoolofhaskell.com/school/starting-with-haskell/introduction-to-haskell/5-type-classes
@themattchan
themattchan / linux style gnu indent
Last active May 21, 2016 07:53
gnuindent -kr -l80 -ut -i8 -ts8 -sob *.c *.h
# cribbed from scripts/Lindent from kernel
gnuindent -npro -kr -i8 -ts8 -sob -l80 -ss -ncs -cp1
@themattchan
themattchan / diagram.hs
Created April 24, 2016 01:44
#! /usr/bin/runhaskell
{-# LANGUAGE FlexibleContexts #-}
module Lib where
import Diagrams.Prelude
import Diagrams.Backend.PGF.CmdLine
pipeline :: Diagram PGF
pipeline = foldr1 (|||) labelledBlocks
where
@themattchan
themattchan / keybase.md
Created March 4, 2016 05:02

Keybase proof

I hereby claim:

  • I am themattchan on github.
  • I am mattchan (https://keybase.io/mattchan) on keybase.
  • I have a public key whose fingerprint is 43B9 F9E7 C56E D3BF 1063 7CFC 013F 7CA0 4EBC 8427

To claim this, I am signing this object: