Skip to content

Instantly share code, notes, and snippets.

Twan van Laarhoven twanvl

Block or report user

Report or block twanvl

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@twanvl
twanvl / gist:2938456
Created Jun 15, 2012
Applicative Concurrent computation without unnecessary threads
View gist:2938456
{-# LANGUAGE ImplicitParams #-}
import Control.Monad
import Control.Monad.Fix
import Control.Applicative
import Control.Concurrent
import Control.Concurrent.MVar
import Control.Exception
import Prelude hiding (catch)
import Data.IORef
import Data.Traversable
@twanvl
twanvl / gist:3873221
Created Oct 11, 2012
MonadTrans with explicit dictionaries
View gist:3873221
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ConstraintKinds, GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
import GHC.Exts
-- see http://www.reddit.com/r/haskell/comments/117r1p/whats_wrong_with_ghc_haskells_current_constraint/
data Dict :: Constraint -> * where
Dict :: c => Dict c
@twanvl
twanvl / gist:4944663
Created Feb 13, 2013
Ugly code to find optimal search trees
View gist:4944663
{-
http://noamlewis.wordpress.com/2013/02/12/penalty-search-problem-revisited-dynamic-programming-control-parallel-to-the-rescue/
-}
import Data.MemoCombinators
--f k = fromIntegral k
data CostTree
@twanvl
twanvl / Sorting.agda
Created May 23, 2013
Correctness and runtime of mergesort, insertion sort and selection sort.
View Sorting.agda
module Sorting where
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Nullary
@twanvl
twanvl / 2013-06-26-midpoints.agda
Last active Dec 19, 2015
Midpoints.agda: proof of equivalence for a HIT (for Cale)
View 2013-06-26-midpoints.agda
{-# OPTIONS --without-K #-}
module 2013-06-26-midpoints where
{-
This is a proof that the HIT
data S A where
[_] : A -> S A;
mid : {x y : A} -> Id x y -> Id [ x ] [ y ]
@twanvl
twanvl / 2013-10-23-lambda.agda
Created Oct 23, 2013
Formalization of untyped lambda calculus, with proof of confluence.
View 2013-10-23-lambda.agda
-- Formalization of untyped lambda calculus
module 2013-10-23-lambda where
open import Level hiding (zero;suc)
open import Function using (_∘_;id;_⟨_⟩_)
open import Data.Empty
open import Data.Star as Star using (Star;_◅_;_◅◅_;ε;_⋆)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Data.Product as P hiding (map;zip)
@twanvl
twanvl / 2013-11-13-confluence-problem.agda
Created Nov 13, 2013
Proof of the open problem in section 7 of "Pure Subtype Systems" by DeLesley S. Hutchins.
View 2013-11-13-confluence-problem.agda
module 2013-11-13-confluence-problem where
open import 2013-11-13-relations
open import Function
open import Data.Unit using (⊤;tt)
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Product as P hiding (map;zip;swap)
open import Data.Nat as Nat hiding (fold)
open import Data.Nat.Properties as NatP
@twanvl
twanvl / 2013-12-20-confluence-problem-v2.agda
Created Dec 20, 2013
New proof of confluence thing (see https://gist.github.com/twanvl/7453495), which will hopefully also extend to lambda calculus.
View 2013-12-20-confluence-problem-v2.agda
module 2013-12-20-confluence-problem-v2 where
open import 2013-12-20-relations
open import Function
open import Data.Unit using (⊤;tt)
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Product as P hiding (map;zip;swap)
open import Data.Nat as Nat hiding (fold)
open import Data.Nat.Properties as NatP
@twanvl
twanvl / 2013-11-13-relations.agda
Created Dec 21, 2013
Proof of confluence of beta reduction + D reduction (a simple form of eta for pairs), for the untyped lambda calculus. See http://lambda-the-ultimate.org/node/4835 for a discussion.
View 2013-11-13-relations.agda
module 2013-11-13-relations where
open import Level hiding (zero;suc)
open import Function
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Empty
open import Data.Product using (∃)
open import Induction.WellFounded
View leonardo.agda
-- Inspired by https://www.fpcomplete.com/user/edwardk/fibonacci/leonardo
open import Data.Nat
module Leonardo (A : Set) where
-- Tree n is a tree of size the nth Leonardo number
data Tree : ℕ → Set where
tip : A Tree 0
tip' : A Tree 1
You can’t perform that action at this time.