twanvl’s gists

twanvl / gist:2938456

Created June 15, 2012 20:02

Applicative Concurrent computation without unnecessary threads

	{-# 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 / gist:3873221

Created October 11, 2012 15:28

MonadTrans with explicit dictionaries

	{-# 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 / gist:4944663

Created February 13, 2013 13:39

Ugly code to find optimal search trees

	{-
	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 / Sorting.agda

Last active December 2, 2022 16:44

Correctness and runtime of mergesort, insertion sort and selection sort.

	module Sorting where
	-- See https://www.twanvl.nl/blog/agda/sorting

	open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
	open import Data.List hiding (merge)
	open import Data.List.Properties
	open import Data.Nat hiding (_≟_;_≤?_)
	open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans)
	open import Data.Nat.Logarithm
	open import Data.Nat.Induction

twanvl / 2013-06-26-midpoints.agda

Last active December 19, 2015 00:59

Midpoints.agda: proof of equivalence for a HIT (for Cale)

	{-# 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 / 2013-10-23-lambda.agda

Created October 23, 2013 10:07

Formalization of untyped lambda calculus, with proof of confluence.

	-- 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 / 2013-11-13-confluence-problem.agda

Created November 13, 2013 18:01

Proof of the open problem in section 7 of "Pure Subtype Systems" by DeLesley S. Hutchins.

	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 / 2013-12-20-confluence-problem-v2.agda

Created December 20, 2013 22:35

New proof of confluence thing (see https://gist.github.com/twanvl/7453495), which will hopefully also extend to lambda calculus.

	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 / 2013-11-13-relations.agda

Created December 21, 2013 23:48

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.

	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

twanvl / leonardo.agda

Created April 28, 2015 14:49

	-- 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

Twan van Laarhoven twanvl