Skip to content

Instantly share code, notes, and snippets.

Mostly unresponsive these days

Daniel Peebles copumpkin

Mostly unresponsive these days
View GitHub Profile
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} [] ≡ []
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
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
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 / Resource.hs
Last active Aug 29, 2015
Can you break my shitty linear resource monad transformer? Looking for people to find ways that it's unsafe.
View Resource.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RebindableSyntax #-}
module Resource where
View FingerStar.agda
module FingerStar where
open import Level using (_⊔_)
open import Algebra
open import Data.Empty
open import Data.Product hiding (map)
open import Data.Nat hiding (compare; _⊔_)
open import Data.Nat.Properties
open import Data.Vec renaming (map to mapVec) hiding ([_])
View Ack.agda
module Ack where
data Nat : Set where
zero : Nat
suc : Nat Nat
copumpkin / Instances.hs
Created Jul 17, 2015
Map parametrized by "named Ord instances"
View Instances.hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
module Instances where
data Map o k v = Map
{ mapOrder :: k -> k -> Ordering
, mapImpl :: () -- You'd stick your actual map implementation as another field here and hide the constructor
data ForgottenMap k v = forall o. ForgottenMap (Map o k v)
View gist:93840
#include <iostream>
void f(int &imachangeu) {
imachangeu = 7;
int main() {
int x = 5;
std::cout << x << std::endl;