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
View Telescope.agda
module Telescope where
open import Function
open import Data.Unit
open import Data.Product
open import Data.Nat
open import Data.Vec
infixr 6 _∷_
@copumpkin
copumpkin / RuntimeTypes.agda
Last active Jul 24, 2018
Simulating "type providers" in Agda
View RuntimeTypes.agda
module RuntimeTypes where
open import Function
open import Data.Unit
open import Data.Bool
open import Data.Integer
open import Data.String as String
open import Data.Maybe hiding (All)
open import Data.List
open import Data.List.All
View STLC.agda
module STLC where
-- Simple substitution à la Conor, as described in http://strictlypositive.org/ren-sub.pdf
id : {A : Set} A A
id x = x
data Type : Set where
* : Type
_⇒_ : (S T : Type) Type
View keybase.md

Keybase proof

I hereby claim:

  • I am copumpkin on github.
  • I am copumpkin (https://keybase.io/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 Topology.agda
module Topology where
import Level
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Fin
open import Data.Product
open import Relation.Nullary
@copumpkin
copumpkin / Lawvere.agda
Last active Oct 26, 2017
Lawvere's theorem
View Lawvere.agda
module Lawvere where
open import Function.Equality hiding (cong)
open import Function.Surjection
open import Data.Product
open import Relation.Binary.PropositionalEquality
lawvere : {A B : Set} (f : A ↠ (A B)) (g : B B) λ x x ≡ g x
lawvere {A} {B} f g = h a , subst (λ r h a ≡ g r) (cong (λ f f a) (from-to refl)) refl
where
@copumpkin
copumpkin / WeirdIso.agda
Created Mar 10, 2014
What could this strange type be isomorphic to?
View WeirdIso.agda
module WeirdIso where
open import Coinduction
open import Data.Nat
open import Data.Stream
open import Relation.Binary.PropositionalEquality
data Weird : Set where
A : (x : Weird) Weird
B : (x : ∞ Weird) Weird
@copumpkin
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
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
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.