Skip to content

Instantly share code, notes, and snippets.

Avatar
💭
Mostly unresponsive these days

Daniel Peebles copumpkin

💭
Mostly unresponsive these days
View GitHub Profile
@copumpkin
copumpkin / Types.agda
Last active Mar 5, 2021
Types form a commutative semiring!
View Types.agda
module Types where
open import Level
open import Function
open import Algebra
open import Data.Empty
open import Data.Unit
open import Data.Sum as Sum
open import Data.Product as Prod
open import Relation.Binary
View FinVector-cons.agda
module FinVector-cons (T : Set) where
data Nat : Set where
zero : Nat
suc : Nat Nat
data Fin : Nat Set where
zero : {n} Fin (suc n)
suc : {n} Fin n Fin (suc n)
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 / Prime.agda
Last active May 17, 2020
There are infinite primes
View Prime.agda
module Prime where
open import Coinduction
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility
open import Data.Fin hiding (pred; _+_; _<_; _≤_; compare)
open import Data.Fin.Props hiding (_≟_)
View Primes.agda
module Primes where
open import Level using (_⊔_)
open import Coinduction
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility
View gist:166118
{-# LANGUAGE ExistentialQuantification, TypeOperators #-}
module Fold where
import Control.Applicative
import Control.Functor.Contra
import Data.Array.Vector
import qualified Data.Foldable as Foldable
data Fold b c = forall a. Fold (a -> b -> a) a (a -> c)
@copumpkin
copumpkin / gist:149443
Created Jul 18, 2009
Lots of iPhone protocols. Consider this BSD-licensed. I'd also appreciate if you made changes through the gist interface so I can see what you've done, but no pressure :)
View gist:149443
# Very alpha still, but getting there...
# Yeah, I like it this way
require 'pp'
require 'set'
require 'zlib'
require 'base64'
require 'socket'
require 'openssl'
require 'stringio'
@copumpkin
copumpkin / Grothendieck.agda
Last active Nov 2, 2019
Grothendieck group
View Grothendieck.agda
module Grothendieck where
open import Level using (_⊔_)
open import Function
open import Algebra
open import Algebra.Structures
open import Data.Product
import Relation.Binary.EqReasoning as EqReasoning
View SelectiveSigma.hs
{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds, PolyKinds, TypeOperators, ScopedTypeVariables #-}
-- Lots of ways you can phrase this, but this works for me
-- For folks who haven't seen it before, this is "the essence of the sum type" and sigma stands for sum.
-- You see it far more often in dependent types than elsewhere because it becomes a lot more pleasant to
-- work with there, but it's doable in other contexts too. Think of the first parameter to the data
-- constructor as a generalized "tag" as we talk about in "tagged union", and the second parameter is the
-- "payload". It turns out that you can represent any simple sum type you could write in Haskell this way
-- by using a finite and enumerable `f`, but things can get more unusual when `f` isn't either. In such
-- cases, it's often easier to think of this as the essence of existential types.
@copumpkin
copumpkin / Unify.agda
Last active Jul 6, 2019
Structurally recursive unification à la McBride
View Unify.agda
module Unify where
-- Translated from http://strictlypositive.org/unify.ps.gz
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)