Skip to content

Instantly share code, notes, and snippets.


Ting-gan LUA banacorn

View GitHub Profile
let first p xs =
let length = Array.length xs in
(* mutable aray index *)
let i = ref 0 in
(* there are no loop breaks in OCaml anyway *)
let break = ref false in
while not (!break) && !i < length do
if p (xs.(!i)) then break := true else i := (!i) + 1
View Chapter-1-6.hs
-- This exercise covers the first 6 chapters of "Learn You a Haskell for Great Good!"
-- Chapter 1 -
-- Chapter 2 -
-- Chapter 3 -
-- Chapter 4 -
-- Chapter 5 -
-- Chapter 6 -
-- Download this file and then type ":l Chapter-1-6.hs" in GHCi to load this exercise
View FLOLAC-STLC2.agda
Intrinsically-typed de Bruijn representation of simply typed lambda calculus
open import Data.Nat
open import Data.Empty
hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
// Types
type t;
type eventName = string;
type listener('a) = 'a => unit;
type listener2('a, 'b) = ('a, 'b) => unit;
type listener3('a, 'b, 'c) = ('a, 'b, 'c) => unit;
View WAT.agda
{-# OPTIONS --without-K #-}
module A where
infixl 4 _≡_
data _≡_ {A : Set} (x : A) : A Set where
refl : x ≡ x
J : (A : Set) (C : (x y : A) x ≡ y Set)
((x : A) C x x refl)
banacorn /
Last active Aug 1, 2019
Reducing expressions in CP

Reducing expressions in CP


CP is a process calculus presented by Philip Wadler in his paper "Propositions as sessions" (, as an attempt to bridge π-calculus with Linear logic.

Process calculus (like CP) provides a mean of modelling and describing the interactions and communications between a bunch of independent processes. The interaction between these processes are often described with some reduction rules.

banacorn /
Last active Oct 30, 2018

Goal: show that TSP is NP-complete

  • TSP is NP
  • TSP is NP-Hard


  • Algorithm: given a tour, sum the weights, and see if it exceeds the bound
  • The verifier runs in polynomial time
View gist:0b10f5a029ae10d7cf9e81d5baed90f7
$ apm rebuild
Rebuilding modules ✗
gyp info it worked if it ends with ok
gyp verb cli [ '/Applications/',
gyp verb cli '/Applications/',
gyp verb cli 'rebuild' ]
gyp info using node-gyp@3.4.0
gyp info using node@8.9.3 | darwin | x64
gyp verb command rebuild []
gyp verb command clean []
banacorn /
Created Aug 2, 2018
Developing Agda with Stack


stack build --stack-yaml stack-8.4.3.yaml


You may need to edit .ghci first:


A monad is also a applicative functor, that seems pretty obvious, right?

Let's formalize this idea a bit:

This is record that houses the laws of applicative functors.

record IsApplicative {ℓ} (F : Set Set ℓ)
                 (pure : {A : Set ℓ}  A  F A)
                 (_⊛_ : {A B : Set ℓ}  (F (A  B))  F A  F B)
                 : Set (suc ℓ) where