Skip to content

Instantly share code, notes, and snippets.

View twanvl's full-sized avatar

Twan van Laarhoven twanvl

View GitHub Profile
@twanvl
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
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)))
-- 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
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
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
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
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
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
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
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