Skip to content

Instantly share code, notes, and snippets.

Avatar
🥺

Ting-gian LUA banacorn

🥺
View GitHub Profile
@banacorn
banacorn / windows.md
Last active November 3, 2021 04:55
FLOLAC'16 / Windows 安裝指南
View windows.md

有哪些東西要安裝?

Windows 64-bit 一鍵安裝包:http://www.cs.uiowa.edu/~astump/agda/備用連結(比較快)) 本安裝檔包含 GHC 7.8、Agda 2.4 以及 Emacs

  1. Haskell
  • ghcghci ,GHC 提供的 Haskell 編譯器與交互式直譯器
  • 建議版本為 **GHC 7.8 (較舊版本例如 **7.6 也可以接受,而更新的版本 prelude 所提供的函數型別會與教學使用的有些落差)
  1. Agda
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
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
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
@banacorn
banacorn / EventEmitter3.re
Last active June 8, 2020 07:29
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;
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
banacorn / cp-reduction.md
Last active August 1, 2019 04:06
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.

@banacorn
banacorn / TSP.md
Last active October 30, 2018 00:24
HC to TSP
View TSP.md

Goal: show that TSP is NP-complete

  • TSP is NP
  • TSP is NP-Hard

TSP is NP

  • 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/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
View agda-stack.md

Build

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

REPL

You may need to edit .ghci first: