Skip to content

Instantly share code, notes, and snippets.

View ashley-woodard's full-sized avatar

Ashley Woodard ashley-woodard

View GitHub Profile
@ashley-woodard
ashley-woodard / web-servers.md
Created January 19, 2020 08:55 — forked from willurd/web-servers.md
Big list of http static server one-liners

Each of these commands will run an ad hoc http static server in your current (or specified) directory, available at http://localhost:8000. Use this power wisely.

Discussion on reddit.

Python 2.x

$ python -m SimpleHTTPServer 8000
@ashley-woodard
ashley-woodard / myappindicator_v5.py
Created June 27, 2019 16:14 — forked from candidtim/myappindicator_v5.py
Ubuntu AppIndicator to show Chuck Norris jokes
# This code is an example for a tutorial on Ubuntu Unity/Gnome AppIndicators:
# http://candidtim.github.io/appindicator/2014/09/13/ubuntu-appindicator-step-by-step.html
import os
import signal
import json
from urllib2 import Request, urlopen, URLError
from gi.repository import Gtk as gtk

Keybase proof

I hereby claim:

  • I am ashley-woodard on github.
  • I am ashley_woodard (https://keybase.io/ashley_woodard) on keybase.
  • I have a public key ASB3VunOu_DpPBtESa6CaOzwWRQkZQ1SvXoWpfqNPyzEYAo

To claim this, I am signing this object:

module ULC where
import Data.Set as S
import Data.Map.Lazy as M
--untyped lambda calculus - variables are numbers now as it's easier for renaming
data Term
= Var Int
| Abs Int Term
| App Term Term
@ashley-woodard
ashley-woodard / SystemT.hs
Created May 22, 2018 04:13 — forked from lukeg101/SystemT.hs
haskell implementation of Godel's System T (typed Lambda calculus with Nats as a base type)
module SystemT where
import Data.Map as M
import Data.Set as S
data T
= TNat
| TArr T T
deriving (Eq, Ord)
@ashley-woodard
ashley-woodard / ABT.hs
Created May 22, 2018 04:12 — forked from jozefg/ABT.hs
A tiny tottering implementation of abstract binding trees
{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleContexts, LambdaCase #-}
-- | A humane representation of binding.
module ABT ( FreeVar (..)
, Operator (..)
, ABT
, View (..)
, view
, fold
@ashley-woodard
ashley-woodard / PatCompile.hs
Created May 22, 2018 04:07 — forked from jozefg/PatCompile.hs
Wadler's classic pattern matching algorithm implemented for a core language with Bound.
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module PatCompile where
import Bound
import Bound.Var
import Bound.Scope
import Control.Monad (ap)
@ashley-woodard
ashley-woodard / BoundPi.hs
Created May 22, 2018 04:03 — forked from jozefg/BoundPi.hs
Bound my type checker for λΠ
{-# LANGUAGE LambdaCase, DeriveFunctor #-}
module LambdaPi where
import Bound
import Control.Applicative
import Control.Monad
import Control.Monad.Gen
import Control.Monad.Reader
import qualified Data.Map as M
import Data.Maybe
import Prelude.Extras
--Roughly based on https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Core.hs by Gabriel Gonzalez et al.
data Expr = Star | Box | Var Int | Lam Int Expr Expr | Pi Int Expr Expr | App Expr Expr deriving (Show, Eq)
subst v e (Var v') | v == v' = e
subst v e (Lam v' ta b ) | v == v' = Lam v' (subst v e ta) b
subst v e (Lam v' ta b ) = Lam v' (subst v e ta) (subst v e b )
subst v e (Pi v' ta tb) | v == v' = Pi v' (subst v e ta) tb
subst v e (Pi v' ta tb) = Pi v' (subst v e ta) (subst v e tb)
subst v e (App f a ) = App (subst v e f ) (subst v e a )
@ashley-woodard
ashley-woodard / pp-comonad.hs
Created October 28, 2017 01:30 — forked from jtobin/pp-comonad.hs
Probabilistic programming using comonads.
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
import Control.Comonad
import Control.Comonad.Cofree
import Control.Monad
import Control.Monad.ST