Skip to content

Instantly share code, notes, and snippets.

Avatar

Liang-Ting Chen L-TChen

View GitHub Profile
@L-TChen
L-TChen / T.agda
Last active Apr 14, 2022
Normalization by evaluation for System T with the normalization proof and the confluence proof
View T.agda
{- 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 _-→_ _-↛_
View FLOLAC-STLC-sol.agda
open import Data.Nat
open import Data.Empty
hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
hiding ([_])
infix 3 _⊢_ _=β_
infixr 7 _→̇_
View FLOLAC-STLC.lagda.md

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 Jul 27, 2020
Go to definitions in Agda mode combined with Evil mode in Emacs
View agda-input-emacs.MD

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 Mar 22, 2019
Some experiments with --prop and instance arguments
View Playground.agda
{-# 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 Feb 26, 2019
Lambda Terms which are Sized, Scoped, Indexed by (potentially) free variables
View Base.agda
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 Jan 22, 2019
An imperative implementation of Union-Find algorithm in Haskell
View Union.hs
{-# 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 Jan 18, 2019
Purely Functional Deque
View Deque.hs
{-# 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 Jan 3, 2019
The derivation of Quickselect from Quicksort, see my blog post https://xcycl.wordpress.com/2019/01/02/fromquicksorttoquickselect/
View Quickselect.hs
{-# 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 Dec 17, 2018
Pattern matching for Vector using PatternSynonyms in Haskell
View VectorPattern.hs
{-# 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