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:
I hereby claim:
To claim this, I am signing this object:
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 |
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 |
{-# 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 |
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 |
{-# 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 |
module Polymorphic where | |
import Level | |
open Level using (Level; _⊔_) | |
open import Function | |
open import Data.Product hiding (map) | |
open import Data.List hiding (all) | |
data Index {A : Set} : List A → A → Set where | |
zero : ∀ {τ Γ} → Index (τ ∷ Γ) τ |
-- This is the type we're working with. | |
data List a = List (forall r. (a -> r -> r) -> r -> r) | |
-- Implement this signature. It should not be inefficient, so if you're planning | |
-- on writing something like tail (notoriously inefficient using foldr) on our | |
-- List type, think again! It should be possible to write with the same time | |
-- complexity as the original. And of course, converting to/from a conventional | |
-- list is cheating :) | |
zipWith :: (a -> b -> c) -> List a -> List b -> List c |
{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-} | |
data Empty | |
data Unit = Unit | |
data Equal a b where | |
Refl :: Equal a a | |
type family F a :: * |
module Scratch where | |
open import Level | |
open import Function | |
open import Relation.Binary.PropositionalEquality | |
import Relation.Binary.EqReasoning as EqReasoning | |
-- Legend has it that parametricity is just dinaturality | |
module Parametricity {a} {F G : Set a → Set a → Set a} | |
(mapF : ∀ {A B C D} → (A → B) → (C → D) → F B C → F A D) |