Skip to content

Instantly share code, notes, and snippets.

View banacorn's full-sized avatar
🥺

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
done;
!i
Intrinsically-typed de Bruijn representation of simply typed lambda calculus
============================================================================
\begin{code}
open import Data.Nat
open import Data.Empty
hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
@banacorn
banacorn / EventEmitter3.re
Last active June 8, 2020 07:29
BuckleScript bindings for EventEmitter3 https://github.com/primus/eventemitter3
//
// 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;
-- This exercise covers the first 6 chapters of "Learn You a Haskell for Great Good!"
-- Chapter 1 - http://learnyouahaskell.com/introduction
-- Chapter 2 - http://learnyouahaskell.com/starting-out
-- Chapter 3 - http://learnyouahaskell.com/types-and-typeclasses
-- Chapter 4 - http://learnyouahaskell.com/syntax-in-functions
-- Chapter 5 - http://learnyouahaskell.com/recursion
-- Chapter 6 - http://learnyouahaskell.com/higher-order-functions
-- Download this file and then type ":l Chapter-1-6.hs" in GHCi to load this exercise
{-# 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
banacorn / cp-reduction.md
Last active August 1, 2019 04:06
Reducing expressions in CP

Reducing expressions in CP

Background

CP is a process calculus presented by Philip Wadler in his paper "Propositions as sessions" (https://dl.acm.org/citation.cfm?id=2364568), 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.

$ apm rebuild
Rebuilding modules ✗
gyp info it worked if it ends with ok
gyp verb cli [ '/Applications/Atom.app/Contents/Resources/app/apm/bin/node',
gyp verb cli '/Applications/Atom.app/Contents/Resources/app/apm/node_modules/.bin/node-gyp',
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
banacorn / agda-stack.md
Created August 2, 2018 07:19
Developing Agda with Stack

Build

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

REPL

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
banacorn / summary-week-4.md
Created May 29, 2018 08:32
Summary of Week 3 - Caesar Cipher

Summary of Week 4 - Caesar Cipher

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