## Sunday, 30 November 2008

### Decidable Equality and Type Equality

`Require Import Eqdep_dec_defined.(** Same as Eqdep_dec but s/Qed/Defined/ **)Theorem dep_destruct :  forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type),    (forall x' (v' : T' x') (Heq : x' = x),      P (match Heq in (_ = x) return (T' x) with           | refl_equal => v'         end)) ->      P v.  intros T T' x v P I; apply (I _ v (refl_equal _)).Defined.(** Stolen from http://www.cs.harvard.edu/~adamc/cpdt/ **)Inductive type : Set :=| Nat : type| Arrow : type -> type -> type.Definition eq_type_dec' (s t : type) : s = t \/ s <> t.decide equality.Defined.Inductive equand : type -> Set :=| Zero : equand Nat| Succ : equand (Arrow Nat Nat).Definition eq_equand_dec {T} (x y : equand T) : {x = y} + {x <> y}.intro.destruct x;  intro y; apply (dep_destruct type equand _ y);    intros T y' Teq; destruct y';      discriminate ||        rewrite <- (eq_proofs_unicity eq_type_dec' (refl_equal _) Teq).left; reflexivity.left; reflexivity.Defined.`

### Calculating Journeys

`-- WARNING: contains recursive programming-- For example data, pick some imaginary flight network:data Node = Paris | London | Shanghai | NewYork | Tokyo deriving (Eq, Show)flights Paris = [London]flights London = [Paris,Shanghai,NewYork]flights Shanghai = [Tokyo,NewYork]flights NewYork = [London]flights Tokyo = [Paris,London,Shanghai]-- and a convenient data representation of the transitive closuredata Graph a = {- DeadEnd | -} a :-->: [Graph a] deriving ShowtransitiveClosure location = location :-->: map transitiveClosure (flights location){-- define the truncation of any cyclical journeysfinite visited DeadEnd = DeadEndfinite visited (location :-->: destinations) | already visited location = DeadEnd |         otherwise        = location :-->: map (finite (location : visited)) destinationsalready = flip elem-}{-- remove any 'DeadEnd's left oversimplify DeadEnd = DeadEndsimplify (location :-->: destinations) = location :-->: purge (map simplify destinations)purge = foldr cons [] where cons DeadEnd ys = ys       cons x       ys = x : ys-}-- holidays = simplify . finite [] . transitiveClosure-- but fusing the truncation and simplification into one allows the 'DeadEnd' construtor to be erased!simplifyFinite visited (location :-->: destinations) = location :-->: filter (not . already visited) (map (simplifyFinite (location : visited)) destinations)already visited (location :-->: _) = elem location visitedholidays = simplifyFinite [] . transitiveClosure-- > holidays Paris-- Paris :-->: [London :-->: [Shanghai :-->: [Tokyo :-->: [],--                                            NewYork :-->: []],--                            NewYork :-->: []]]-- > holidays London -- London :-->: [Paris :-->: [],--               Shanghai :-->: [Tokyo :-->: [Paris :-->: []],--                               NewYork :-->: []],--               NewYork :-->: []]`

## Saturday, 22 November 2008

### my thought process for breadth first numbering

`data Tree a = Leaf a | Branch a (Tree a) (Tree a) deriving Showi 0 = Leaf 0i n = Branch 0 (i (n-1)) (i (n-1))identity (Leaf i) = Leaf iidentity (Branch i left right) = Branch i (identity left) (identity right)depth current (Leaf _) = Leaf currentdepth current (Branch _ left right) = Branch current (depth (current + 1) left) (depth (current + 1) right)depth' current (Leaf i) = Leaf idepth' current (Branch i left right) = Branch i left' right' where left' = depth' (current + 1) left       right' = depth' (current + 1) rightdepth'' current target (Leaf i) = Leaf (if current == target then i+1 else i)depth'' current target (Branch i left right) = Branch (if current == target then i+1 else i) left' right' where left' = depth'' (current + 1) target left       right' = depth'' (current + 1) target rightdepth''' current target delta (Leaf i) = Leaf (if current == target then i+delta else i) `with` (if current == target then delta+1 else delta)depth''' current target delta (Branch i left right) = Branch (if current == target then i+delta else i) left' right' `with` delta'' where (left',delta') = depth''' (current + 1) target (if current == target then delta+1 else delta) left       (right',delta'') = depth''' (current + 1) target delta' rightwith = (,)unfold step current = case step current of Nothing -> current ; Just next -> unfold step nextbreadth tree = case unfold step (0,0,tree) of (_,_,tree) -> tree where step (depth, delta, tree) = case depth''' 0 depth delta tree of         (tree, delta') -> if delta == delta' then Nothing else Just (depth + 1, delta', tree)-- > breadth (i 3)-- Branch 0 (Branch 1 (Branch 3 (Leaf 7)--                              (Leaf 8))--                    (Branch 4 (Leaf 9)--                              (Leaf 10)))--          (Branch 2 (Branch 5 (Leaf 11)--                              (Leaf 12))--                    (Branch 6 (Leaf 13)--                              (Leaf 14)))`

## Thursday, 20 November 2008

### Type Error

`Error:In environmentty : typem : term tyeq_term_dec :forall (m' : {m' : term ty | size m' < size m}) (n : term ty),{`m' = n} + {`m' <> n}n : term tyeq_term_dec0 :forall (ty : type) (m n : term ty),{[m : (term ty)]= [n : (term ty)]} + {m =/= n}ty0 : typem0 : term ty0n0 : term ty0uTy : typevTy : typeu : term (uTy --> vTy)v : term uTyuTy' : typevTy' : typeu' : term (uTy' --> vTy')v' : term uTy'vTyEq : vTy = vTy'filtered_var := eq_type_dec uTy uTy' : {uTy = uTy'} + {uTy <> uTy'}uTyEq : uTy = uTy'Heq_anonymous : in_left = filtered_varu0 : term (uTy --> vTy)v0 : term uTyu'0 : term (uTy --> vTy)v'0 : term uTyfiltered_var0 := eq_term_dec0 (uTy --> vTy) u0 u'0 :{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}filtered_var1 := eq_term_dec0 uTy v0 v'0 :{[v0 : (term uTy)]= [v'0 : (term uTy)]} + {v0 =/= v'0}branch_0 :=fun (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])  (wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)])  (Heq_anonymous0 : in_left = filtered_var0)  (Heq_anonymous1 : in_left = filtered_var1) => in_left :forall  (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])  (wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),in_left = filtered_var0 ->in_left = filtered_var1 ->{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +{app u0 v0 =/= app u'0 v'0}branch_1 :=fun  (wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +               {u0 =/= u'0})  (wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +                {u'0 =/= filtered_var0})  (H : forall         (wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0                       : (term (uTy --> vTy))])         (wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),       ~ (in_left = wildcard' /\ in_left = wildcard'0))  (Heq_anonymous0 : wildcard' = filtered_var0)  (Heq_anonymous1 : wildcard'0 = filtered_var1) => in_right :forall  (wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +               {u0 =/= u'0})  (wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +                {u'0 =/= filtered_var0}),(forall   (wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])   (wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]), ~ (in_left = wildcard' /\ in_left = wildcard'0)) ->wildcard' = filtered_var0 ->wildcard'0 = filtered_var1 ->{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +{app u0 v0 =/= app u'0 v'0}Anonymous : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]wildcard' := in_left :{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}Anonymous0 : u'0 =/= wildcard'wildcard'0 := in_right :{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}The term "wildcard'0" has type "{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}" while it is expected to have type "{[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +  {u'0 =/= filtered_var0}".`

## Saturday, 15 November 2008

`data Pill a where Stop :: Pill Integer O :: Pill (Pill a -> a)collect :: Integer -> Pill a -> acollect i Stop = icollect i O = collect (i+1)start = collect 0-- > start Stop-- 0-- > start O Stop-- 1-- > start O O Stop-- 2-- > start O O O Stop-- 3-- > start O O O O Stop-- 4-- > start O O O O O Stop-- 5`
`{-# LANGUAGE NoMonomorphismRestriction #-}import Prelude hiding (Either(..))import Data.Listimport Data.Maybeimport Data.Ordimport Control.Monad.Readerlookdown :: (Eq b) => [(a, b)] -> b -> Maybe alookdown pairs i = lookup i (map swap pairs)onFst f (x,y) = (f x, y)swap (x,y) = (y,x)f & g = \x -> (f x, g x)infix 4 &-------data Huff a = Leaf a | Branch (Huff a) (Huff a) deriving Show-- -- Example tree:-- let t =--   (Branch (Leaf T)--           (Branch (Leaf F)--                   (Leaf T)))foldHuff leaf branch = φ where φ (Leaf o) = leaf o       φ (Branch left right) = branch (φ left) (φ right)-- foldHuff (!) (*) t =--   (* (! T)--      (* (! F)--         (! T)))instance Functor Huff where fmap f = foldHuff (Leaf . f) BranchdepthFirstTraversal = foldHuff return (++)-- foldHuff (!) (*) t =--   (return T) ++--       (return F) ++--       (return T)-- = [T,F,T]member e = foldHuff (== e) (||)data Direction = Left | Right deriving Showtype Path = [Direction]branch join left right = \φleft φright -> join (left φleft) (right φright)label = foldHuff (Leaf . (,) []) -- you are here                 (branch Branch (fmap (onFst (Left:))) -- first on your left                                (fmap (onFst (Right:))))type Freq a = (Integer, Huff a)frequencies = map (length & Leaf . head) . sortBy (comparing length) . group . sortjoinTrees ((p1,t1) : (p2,t2) : freqs) = joinTrees (insertBy (comparing fst) (p1 + p2,Branch t1 t2) freqs)joinTrees [(_,tree)] = treehuffmanTree = joinTrees . frequenciescodeTable = depthFirstTraversal . label . huffmanTreeencode codeTable = catMaybes . map (lookdown codeTable)huffmanCode = concat . join (encode . codeTable)traverse (Leaf o) path = Just (o, path)traverse (Branch l r) (Left:path) = traverse l pathtraverse (Branch l r) (Right:path) = traverse r pathtraverse _ [] = NothinghuffmanDecode = unfoldr . traverse-- forall text, length text > 1 ->correct text = huffmanDecode (huffmanTree text) (huffmanCode text) == text-- checking how many bits saved on an 8 bit encoded stringsavings text = length text * 8 - length (huffmanCode text)-- > huffmanTree "quick brown fox jumped over the lazy dog"-- Branch (Branch (Branch (Branch (Branch (Leaf 'i') (Leaf 'j')) (Branch (Leaf 'g') (Leaf 'h'))) (Branch (Branch (Leaf 'm') (Leaf 'n')) (Branch (Leaf 'k') (Leaf 'l')))) (Branch (Branch (Leaf 'd') (Leaf 'r')) (Branch (Branch (Leaf 'c') (Leaf 'f')) (Branch (Leaf 'a') (Leaf 'b'))))) (Branch (Branch (Leaf 'o') (Branch (Leaf 'u') (Leaf 'e'))) (Branch (Leaf ' ') (Branch (Branch (Branch (Leaf 't') (Leaf 'v')) (Branch (Leaf 'p') (Leaf 'q'))) (Branch (Branch (Leaf 'y') (Leaf 'z')) (Branch (Leaf 'w') (Leaf 'x'))))))-- > correct "quick brown fox jumped over the lazy dog"-- True-- > savings  "quick brown fox jumped over the lazy dog"-- 143`