Proposed BFPG lightning talk. 25 slides, 5 minutes, 12 seconds per slide. No problem!
September 2014
Motivation: we want to write something as clear as this, but this is O(n^2).
Require Import List. | |
Import ListNotations. | |
Set Implicit Arguments. | |
Fixpoint reverse (X: Type) (xs: list X): list X := | |
match xs with | |
| [] => [] | |
| x :: xs' => reverse xs' ++ [x] | |
end. |
Lemma list_narrow_ind: | |
forall | |
(X: Type) | |
(P: list X -> Prop) | |
(H: P []) | |
(J: forall x, P [x]) | |
(K: forall x ys z, P ys -> P (x :: ys ++ [z])) | |
(l: list X), | |
P l. | |
Proof. |
Lemma list_len_odd_even_ind: | |
forall | |
(X: Type) | |
(P: list X -> Prop) | |
(H: forall xs, length xs = 0 -> P xs) | |
(J: forall xs, length xs = 1 -> P xs) | |
(K: forall xs n, length xs = n -> P xs -> forall ys, length ys = S (S n) -> P ys) | |
(l: list X), | |
P l. | |
Proof. |
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2, | |
split l = (l1, l2) -> | |
combine l1 l2 = l. | |
Proof. | |
induction l as [|[x y] ps]; | |
try (simpl; destruct (split ps)); | |
inversion 1; | |
try (simpl; apply f_equal; apply IHps); | |
reflexivity. | |
Qed. |
Fixpoint split | |
{X Y : Type} (l : list (X*Y)) | |
: (list X) * (list Y) := | |
match l with | |
| nil => (nil, nil) | |
| (x,y) :: t => | |
let (r,s) := split t in | |
(x :: r, y :: s) | |
end. |
{-# LANGUAGE RankNTypes #-} | |
import Control.Lens.Lens (Lens,lens) | |
type Quotient s t a = forall b. Lens s t a b | |
quotient :: (s -> a) -> (s -> t) -> Quotient s t a | |
quotient sa st = lens sa (const . st) |
{-# LANGUAGE DeriveFoldable #-} | |
{-# LANGUAGE DeriveFunctor #-} | |
{-# LANGUAGE DeriveTraversable #-} | |
{-# LANGUAGE ImpredicativeTypes #-} | |
{-# LANGUAGE Rank2Types #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE TypeOperators #-} | |
-- Richard Bird, Thinking Functionally with Haskell. | |
-- Chapter 2, Exercise E: |
{-# LANGUAGE Rank2Types #-} | |
type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t) | |
type Ref s t a b = s -> Rep a b t | |
data Rep a b t = Rep a (b -> t) | |
instance Functor (Rep a b) where | |
fmap f (Rep a g) = Rep a (f . g) |
import Criterion.Main (Benchmark, bench, bgroup, defaultMain, env, whnf) | |
import Data.Foldable (Foldable(..),toList) | |
import Data.Maybe (Maybe(..)) | |
import Data.Monoid (Monoid(..), (<>)) | |
import Data.Set (Set,fromList) | |
import Prelude (Eq(..),Ord(..),Show(..),Int,(.),($),($!),Num(..),const,take,iterate,map,return,IO) | |
last :: Foldable t => t a -> Maybe a | |
last = foldl (const Just) Nothing |