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 extract.py
#!/usr/bin/env python
from os import listdir
from os.path import isfile, join
import re
import json
from bs4 import BeautifulSoup
"""
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 / 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 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 #-}
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 ([_])
@copumpkin
copumpkin / Relations.agda
Created Jul 9, 2014
Relations form a semiring!
View Relations.agda
-- See also https://gist.github.com/copumpkin/2636229
module Relations where
open import Level
open import Function
open import Algebra
open import Data.Empty
open import Data.Sum as Sum
open import Data.Product as Prod
open import Relation.Binary
@copumpkin
copumpkin / classifiers
Created May 3, 2014
Chinese classifiers and the words they classify, built from CC-CEDICT and Max Bolingbroke's cjk Haskell package
View classifiers
[箇 个 [ge4] /variant of 個|个[ge4]/,個 个 [ge4] /individual/this/that/size/classifier for people or objects in general/]
鼻子 鼻子 [bi2 zi5] /nose/CL:個|个[ge4],隻|只[zhi1]/
鼓舞 鼓舞 [gu3 wu3] /heartening (news)/boost (morale)/CL:個|个[ge4]/
黨員 党员 [dang3 yuan2] /political party member/CL:名[ming2],位[wei4],個|个[ge4]/
黨 党 [dang3] /party/association/club/society/CL:個|个[ge4]/
黑板 黑板 [hei1 ban3] /blackboard/CL:塊|块[kuai4],個|个[ge4]/
黃鱔 黄鳝 [huang2 shan4] /swamp eel/finless eel/CL:個|个[ge4],條|条[tiao2]/
鬼 鬼 [gui3] /ghost/sly/crafty/CL:個|个[ge4]/
高麗菜 高丽菜 [gao1 li4 cai4] /cabbage/CL:顆|颗[ke1],個|个[ge4]/
高度 高度 [gao1 du4] /height/altitude/elevation/high degree/highly/CL:個|个[ge4]/
@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
@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
@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
You can’t perform that action at this time.