twanvl’s gists

twanvl / machinesbench.hs

Created June 7, 2016 21:01

Machines benchmark modified to include vector stream fusion. Addapted from https://gist.github.com/michaelt/f19bef01423b17f29ffd, which is in turn based on https://github.com/ekmett/machines/blob/master/benchmarks/Benchmarks.hs

	{-#LANGUAGE NoMonomorphismRestriction #-}
	module Main (main) where

	import Control.Monad (void)
	import Control.Monad.Identity
	import Criterion.Main
	import qualified Data.Conduit as C
	import qualified Data.Conduit.Combinators as CC
	import qualified Data.Conduit.List as C
	import qualified Data.Machine as M

twanvl / Leonardo.hs

Created April 28, 2015 16:11

	data Spine a
	= NS (NS a a (a,a,a))
	\| AS (AS a a a)
	deriving (Show)

	-- non-adjacent spine: list of increasing size trees, with no two trees of adjacent index
	data NS a b c
	= Nil
	\| NMore (NS a c (a,b,c))
	\| NCons b (NS a (a,b,c) (a,c,(a,b,c)))

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

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

Twan van Laarhoven twanvl