yangzhixuan

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

postulate
  funext : ∀ {a b} {A : Set a} {B : A → Set b} → {f g : (x : A) → B x}
         → ((x : A) → f x ≡ g x) → f ≡ g

  uip : ∀ {a} {A : Set a} {x y : A} → {p q : x ≡ y} → p ≡ q

yangzhixuan

\documentclass{article}

\usepackage{amsmath}

%include polycode.fmt

\newenvironment{autohscode}%
  {\relax\ifmmode\expandafter\pmboxed\else\expandafter\plainhscode\fi}%
  {\relax\ifmmode\expandafter\endpmboxed\else\expandafter\endplainhscode\fi}

yangzhixuan

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE GADTs #-}

data Free f a where
  V :: a -> Free f a
  O :: f (Free f a) -> Free f a

fold :: Functor f => (a -> c) -> (f c -> c) -> Free f a -> c
fold k alg (V a) = k a
fold k alg (O o) = alg (fmap (fold k alg) o)

yangzhixuan

{-# LANGUAGE DataKinds, ImpredicativeTypes #-}

-- Clocked guarded corecursion in the style of Atkey and McBride
-- https://bentnib.org/productive.pdf

-------- Library code -----------
data Clock

newtype Later (k :: Clock) (a :: *) = L a

yangzhixuan

import Control.Monad (foldM)
import Prelude hiding (sum)
import Control.Monad.Random (MonadRandom(getRandom))

type Pos = Int

data TArray = E | N TArray        -- Left subtree
                     Int          -- Data payload (not position!)
                     Int          -- Priority
                     Int          -- Size of the tree

yangzhixuan

% ----------------------------------------------------------------------
% Some useful commands when doing highlighting of Agda code in LaTeX.
% ----------------------------------------------------------------------

\ProvidesPackage{agda}

\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
                calc, environ, xparse, xkeyval, amsmath}

% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation

yangzhixuan

#lang racket

(require "reflection.rkt")

; unit : x -> [x]
(define unit (lambda (x) (cons x '())))

; bind : [x] -> (x -> [y]) -> [y]
(define bind (lambda (m f) (apply append (map f m))))

yangzhixuan

{-# LANGUAGE KindSignatures, GADTs, TypeOperators, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds, DeriveFunctor #-}

import Prelude hiding (Functor)
import qualified Prelude (Functor)

-- This file explores doing category theory in Haskell by implementing 
-- Ralf Hinze et al.'s adjoint folds [1]: 
--

yangzhixuan

{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ScopedTypeVariables, KindSignatures #-}

module FastApp where

import Prelude hiding (head, tail)
import Control.Applicative

-- Chris Okasaki invented many cool and efficient functional data structures
-- in his book Purely Functional Data Structures.
-- Among them, one is catenable lists supporting amortised O(1)-time |(++)|,

yangzhixuan

{-# LANGUAGE RankNTypes #-}

-- Church-Scott encoding combines the Church encoding and Scott encoding of datatypes
-- See: http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf
-- Although the encoding in the paper seems not to support (++) efficiently, it can be fixed as follows. 

import Prelude hiding ((++), head, tail)

newtype CSList a = CSList { run :: forall x . x -> CSList a -> (a -> CSList a -> x -> x) -> x}