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
View Leonardo.hs
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
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 / 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-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
@twanvl
twanvl / machinesbench.hs
Created Jun 7, 2016
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
View machinesbench.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
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.