Skip to content

Instantly share code, notes, and snippets.

Mostly unresponsive these days

Daniel Peebles copumpkin

Mostly unresponsive these days
Block or report user

Report or block copumpkin

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
copumpkin / Format.hs
Last active Aug 29, 2015
A simple translation of the format combinators used in The Power of Pi (
View Format.hs
{-# LANGUAGE EmptyDataDecls, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-}
module Format where
import Prelude hiding (read)
import Data.Either
import Data.Binary.Get
import Data.Binary.Builder
import Data.Monoid
import Data.Foldable
import Control.Applicative
copumpkin / Prickler.hs
Last active Aug 29, 2015
Reasonably painless bidirectional serialization of sums of products
View Prickler.hs
{-# LANGUAGE TemplateHaskell, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-}
module Prickler where
Main goals:
# Minimal indirection, so I didn't want big n-tuples of stuff getting curried into constructors or shit like that
# Magical constructor/eliminator pairing, so I don't have to write ugly unsafe pattern matches or constructor -> Int mappings (unlike the alt combinator in the pickler paper)
# Minimize the amount of metadata traversal that happens during serialization (not 100% there yet)
# Not be ugly to use

Keybase proof

I hereby claim:

  • I am copumpkin on github.
  • I am copumpkin ( on keybase.
  • I have a public key whose fingerprint is C275 212F 15F2 9AB8 FB97 E5F5 1AF9 2946 9280 FBD6

To claim this, I am signing this object:

View Cont.agda
module Categories.Agda.Cont where
open import Categories.Category
open import Categories.Agda
open import Categories.Functor
open import Categories.Monad
open import Categories.Adjunction
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _≣_)
copumpkin / Mat.agda
Last active Aug 29, 2015
"Simple" matrix math for Agda
View Mat.agda
module Mat where
open import Function
open import Data.Empty
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin; zero; suc; toℕ)
open import Data.Fin.Props using ()
open import Data.Product
open import Relation.Nullary
open import Relation.Binary
View Reverse.agda
module Reverse where
open import Data.List as List hiding (reverse)
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality
record ReverseLike (reverse : {A : Set} List A List A) : Set₁ where
constructor rl
reverse0 : {A} reverse {A} [] ≡ []
copumpkin / UnboxableSums.hs
Last active Dec 24, 2015
Unboxable sigmas à la (unimplemented) Kmett, based on "unzipping" with a rank datastructure (currently super shitty). Please excuse the crap quality of the code, but I was just banging out ideas.
View UnboxableSums.hs
{-# LANGUAGE TypeFamilies, GADTs, ConstraintKinds, RankNTypes, TypeOperators, ScopedTypeVariables, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses #-}
module UnboxableSums where
import Prelude hiding (lookup)
import Data.Word
import Data.Bits
import Data.Maybe
import Data.Function
import Data.Constraint
import qualified Data.Vector as V
copumpkin / Unify.agda
Last active Jul 6, 2019
Structurally recursive unification à la McBride
View Unify.agda
module Unify where
-- Translated from
open import Data.Empty
import Data.Maybe as Maybe
open Maybe hiding (map)
open import Data.Nat
open import Data.Fin
open import Data.Product hiding (map)
copumpkin / Collatz.agda
Last active Dec 23, 2015
Here's Collatz, as promised. Hole left as exercise for the reader.
View Collatz.agda
module Collatz where
open import Coinduction
open import Data.Nat hiding (_+_; _*_)
open import Data.Fin hiding (_+_; fromℕ; toℕ)
open import Data.Bin hiding (suc)
open import Data.Maybe
open import Data.Product
open import Data.List as List
open import Data.Colist
copumpkin / Mutable.hs
Last active Dec 23, 2015
Mutable buffered Iteratee-like things. Goal is to let me reuse the input "chunks" but to prevent users from hanging onto them and seeing data they shouldn't see. Does it work? You can leak the MVector reference in an existential but then you can't do anything with it, right?
View Mutable.hs
{-# LANGUAGE RankNTypes, BangPatterns #-}
module Mutable where
import Control.Monad
import Control.Monad.ST
import Data.STRef
import Data.Vector.Mutable (MVector)
import qualified Data.Vector.Mutable as MV
-- A read-only view into an MVector or similar
You can’t perform that action at this time.