{{ message }}

Instantly share code, notes, and snippets.

🥺

# Ting-gan LUA banacorn

🥺
• Taipei, Taiwan
Created Nov 4, 2020
View first.ml
 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
Last active Aug 19, 2020
View FLOLAC-STLC2.agda
 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
Last active Jun 8, 2020
BuckleScript bindings for EventEmitter3 https://github.com/primus/eventemitter3
View EventEmitter3.re
 // // 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;
Last active Aug 25, 2020
View Chapter-1-6.hs
 -- 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
Last active Aug 8, 2019
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)
Last active Aug 1, 2019
Reducing expressions in CP
View cp-reduction.md

# 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.

Created Oct 1, 2018
node-gyp is problematic
View gist:0b10f5a029ae10d7cf9e81d5baed90f7
 \$ 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 []
Created Aug 2, 2018
Developing Agda with Stack
View agda-stack.md

# Build

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

# REPL

You may need to edit .ghci first:

Last active Jun 26, 2018
draft

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

# Summary of Week 4 - Caesar Cipher

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