Skip to content

Instantly share code, notes, and snippets.

Avatar
💭
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
field
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
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
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
copumpkin / Format.hs
Last active Aug 29, 2015
A simple translation of the format combinators used in The Power of Pi (http://www.staff.science.uu.nl/~swier004/Publications/ThePowerOfPi.pdf)
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
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
-- http://en.wikipedia.org/wiki/Ackermann_function#Definition_and_properties
data Nat : Set where
zero : Nat
suc : Nat Nat
{-# BUILTIN NATURAL Nat #-}
@copumpkin
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;