copumpkin

module Categories.Agda.List where

open import Level
open import Categories.Category
open import Categories.Functor using (Functor; module Functor)
open import Categories.NaturalTransformation using (NaturalTransformation; module NaturalTransformation)
open import Categories.Adjunction
open import Categories.Monad
open import Categories.Agda
open import Categories.Support.PropositionalEquality

copumpkin

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)

copumpkin

{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}

data Empty

data Unit = Unit

data Equal a b where
  Refl :: Equal a a

type family F a :: *

copumpkin

-- 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

copumpkin

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 (τ ∷ Γ) τ

copumpkin

{-# 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

copumpkin

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

copumpkin

{-# 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

copumpkin

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

copumpkin

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