Skip to content

Instantly share code, notes, and snippets.


Ting-gian 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 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 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 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.

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
banacorn /
Created May 29, 2018
Summary of Week 3 - Caesar Cipher

Summary of Week 4 - Caesar Cipher

  • 共有 6 位參與者
  • encode 的實作大同小異,但 decode 的方法就各異其趣
  • decoding 過程中要對於每個可能的明文去評分,而評分的方法主要分為兩種:
    • 將字母出現頻率加總,找出最高的那組
    • 建出明文的字母頻率表,並與英文字母頻率表比較「距離」,找出最小的那組
  • 有人使用字母頻率的排名,而不是頻率本身去計算,但還是解得出來!
  • 有人發現 decoding 過程其實可以寫成某種 convolution(小編終於知道以前大一修微積分是幹嘛用的了!)
  • 大家建表所選擇的資料結構有很多種(List, Array, Map),但相對於密文大小的時間複雜度應該都是一樣的