Skip to content

Instantly share code, notes, and snippets.

View L-TChen's full-sized avatar

Liang-Ting Chen L-TChen

87 followers · 143 following
View GitHub Profile
@L-TChen
L-TChen / T.agda
Last active April 14, 2022 06:09
Normalization by evaluation for System T with the normalization proof and the confluence proof
{- Coquand, T., & Dybjer, P. (1997). Intuitionistic model constructions and normalization proofs.
Mathematical Structures in Computer Science, 7(1). https://doi.org/10.1017/S0960129596002150 -}
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂; ∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
infix 3 _-→_ _-↛_
@L-TChen
L-TChen / FLOLAC-STLC-sol.agda
Created August 19, 2020 08:46
open import Data.Nat
open import Data.Empty
hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
hiding ([_])
infix 3 _⊢_ _=β_
infixr 7 _→̇_
@L-TChen
L-TChen / FLOLAC-STLC.lagda.md
Last active August 20, 2020 15:42

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
@L-TChen
L-TChen / agda-input-emacs.MD
Created July 27, 2020 11:47
Go to definitions in Agda mode combined with Evil mode in Emacs

Evil mode overwrites the mouse-2 event which is used by Agda to go to the definition of clicked identifier. To restore the desired behavioru, just add the following line after enabling Evil (require 'evil)

(define-key evil-normal-state-map [mouse-2] 'agda2-goto-definition-mouse)
@L-TChen
L-TChen / Playground.agda
Last active March 22, 2019 20:15
Some experiments with --prop and instance arguments
{-# OPTIONS --safe --prop --overlapping-instances #-}
module Playground where
open import Data.Nat
open import Data.List
open import Data.Bool
open import Data.Empty
open import Data.Unit
@L-TChen
L-TChen / Base.agda
Created February 26, 2019 14:43
Lambda Terms which are Sized, Scoped, Indexed by (potentially) free variables
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
module Term.Base (Atom : Set)(_≟A_ : Decidable {A = Atom} (_≡_)) where
open import Relation.Nullary public
open import Data.Nat renaming (_≟_ to _≟ℕ_)
open import Data.Fin renaming (_≟_ to _≟F_) hiding (_+_; compare)
open import Data.Product hiding (map)
open import Data.List
@L-TChen
L-TChen / Union.hs
Last active January 22, 2019 22:48
An imperative implementation of Union-Find algorithm in Haskell
{-# LANGUAGE BangPatterns #-}
module Union where
import Data.Ix
import Data.Array
import Data.Array.ST
import Control.Monad
import Control.Monad.ST
@L-TChen
L-TChen / Deque.hs
Last active January 18, 2019 19:14
Purely Functional Deque
{-# LANGUAGE ViewPatterns, PatternSynonyms #-}
module Deque where
import Text.Read
import Data.Bifunctor
import Prelude hiding (length, init, tail, last, head)
import qualified Prelude as P
data Deque a =
@L-TChen
L-TChen / Quickselect.hs
Last active January 3, 2019 09:09
The derivation of Quickselect from Quicksort, see my blog post https://xcycl.wordpress.com/2019/01/02/fromquicksorttoquickselect/
{-# LANGUAGE TypeApplications #-}
import Test.QuickCheck
import Data.List (sort)
selectOrigin k = (!! k) . sort
select :: (Ord a) => Int -> [a] -> a
select k (x:xs) = case compare k n of
LT -> select k ys
EQ -> x
@L-TChen
L-TChen / VectorPattern.hs
Last active June 30, 2023 13:42
Pattern matching for Vector using PatternSynonyms in Haskell
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}
import Data.Vector as V
pattern Empty :: Vector a
pattern Empty <- (V.null -> True) where Empty = V.empty
uncons :: Vector a -> Maybe (a, Vector a)
uncons Empty = Nothing