Skip to content

Instantly share code, notes, and snippets.

Avatar

Ting-gan LUA banacorn

View GitHub Profile
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
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 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.

@banacorn
banacorn / TSP.md
Last active Oct 30, 2018
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 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:

View monad-interchange.md

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