banacorn

module Bin where

--  `Set` is a reserved word in Agda, it's the type of all types
--  We are declaring that `Bin` is of type `Set`, `■` is of type `Bin`, and so on ...
data Bin : Set where
    ■   : Bin        -- 0
    0,_ : Bin → Bin  -- 2n
    1,_ : Bin → Bin  -- 2n+1

-- Binary number in a reversed order, for example

banacorn

批踢踢實業坊›看板 Gossiping
作者Machinator (\⊙▽⊙/)
看板Gossiping
標題[爆卦] 從近期的抗爭談些社會意識的錯誤
時間Mon Apr 14 22:09:04 2014

錯誤一：「警察是無辜的，要找就找後面下令的人。」

複製貼上故事：

banacorn

# confidence from 0% to 100%

cat data/1m | time ./dist/build/homework2-hs/homework2-hs 0.0010 0 100 +RTS -K2000m -H500m -RTS
        4.48 real         3.85 user         0.34 sys
cat data/1m | time ./dist/build/homework2-hs/homework2-hs 0.0010 0.1 100 +RTS -K2000m -H500m -RTS
        3.96 real         3.59 user         0.32 sys
cat data/1m | time ./dist/build/homework2-hs/homework2-hs 0.0010 0.2 100 +RTS -K2000m -H500m -RTS
        3.92 real         3.57 user         0.31 sys
cat data/1m | time ./dist/build/homework2-hs/homework2-hs 0.0010 0.3 100 +RTS -K2000m -H500m -RTS
        3.97 real         3.60 user         0.33 sys

banacorn

module BatBunker where

import Data.List (findIndices, delete, (\\))
import Data.Ratio 

data Cell = Empty | Wall | Bat | AlphaBat deriving (Show, Eq)
type Map = [[Cell]]
type Coord = (Int, Int)
type Vertex = (Cell, Coord)

banacorn

maximum :: Ord a => [a] -> a
maximum = foldr max (-∞)

banacorn

import Control.Monad    (forM_)
import Control.Monad.ST (runST)
import Data.IORef 
import Data.STRef

-- dirty, can't get rid of IO
sumIO :: [Int] -> IO Int
sumIO xs = do
    acc <- newIORef 0
    forM_ xs (modifyIORef acc . (+))

banacorn

Ring

Chain of class inclusions

Rings ⊃ Commutative rings ⊃ ID ⊃ UFD ⊃ PID ⊃ ED ⊃ Field

Prime

if a | bc then a | b or a | c, i.e. a can't be torn apart if a is prime

banacorn

Semantics

Lecture 1

• p. 11: For every three terms M0, M1, and M2 => For every three terms M1, M2, and M3

Type Theory & Logic

Lecture 2

banacorn

Mac OS X 的 Agda 安裝指南

詳細可以看看這裡 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX

透過 Hackage 安裝（難度 ✮✮☆☆☆）

1. 首先把 64bit 的 Haskell Platform 裝好 http://www.haskell.org/platform/

2. 把這份 script 複製到 /usr/bin 並且執行它 http://www.haskell.org/platform/ghc-clang-wrapper

banacorn

                    _oo0oo_
                   o8888888o
                   88" . "88
                   (| -_- |)
                   0\  =  /0
                  __/`---'\__
               .' \\|     |// '.