jasonreich

-- Forked from http://personal.cis.strath.ac.uk/~conor/fooling/Jigger.agda
module Jigger where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + n = n
suc m + n = suc (m + n)

jasonreich

{-
Uses the She (Stathclyde Haskell Enhancement), which you
can get from http://bit.ly/gaVM8X.
-}

{-# OPTIONS_GHC -Wall -F -pgmF she #-}
{-# LANGUAGE GADTs, KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE RankNTypes, FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}

jasonreich

{-
Uses the She (Stathclyde Haskell Enhancement), which you
can get from http://bit.ly/gaVM8X.
-}

{-# OPTIONS_GHC -Wall -F -pgmF she #-}
{-# LANGUAGE GADTs, KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE RankNTypes, FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude #-}

jasonreich

# Install the capri sandboxing tool.
cabal install capri

# Download Agda to a directory of your choice.
darcs get --lazy "http://code.haskell.org/Agda"

# Enter the directory. Make sure you `cabal clean` if you
# try this more than once.
cd Agda

jasonreich

INPUTS=...

default: progress.pdf

progress.pdf : progress.tex $(INPUTS) study.bib
	latexmk -pdf $<

%.tex : %.markdown
	pandoc -f markdown -t latex $< > $@

jasonreich

import Control.Arrow
import Control.Monad
-- Using ByteString a little superfluously but thought my parser might slow me down.
import qualified Data.ByteString.Lazy.Char8 as QS
import Data.Bits
import Data.List
import Data.Maybe
import Data.Word

-- | A bag of sweeties is a list of unsigned integers

jasonreich

Michaels solution
=================

> a 0 y = 1
> a x 0 = 1
> a x y = a (x-1) y + a x (y-1)

> result = map (\x -> a x x) [0..]

Memoised form

jasonreich

Fun with monoids
================

We'll need the monoid library.

> import Data.Monoid

Difference lists
----------------

jasonreich

import Control.Parallel.Strategies (using, parBuffer, rseq)
import Data.List (partition)

-- *** Example Haskell functions ***

-- Is a list of integers sorted?
isOrdered :: [Int] -> Bool
isOrdered (x:y:zs) = x <= y && isOrdered (y:zs)
isOrdered _        = True

jasonreich

-- Based on http://blog.sigfpe.com/2006/12/evaluating-cellular-automata-is.html
-- But uses the Gloss (http://hackage.haskell.org/package/gloss) library to draw the image.

module OneDCA where

import Data.Bits
import Data.Word
import Graphics.Gloss

-- Universes