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.
Sunday 30 November 2008
Decidable Equality and Type Equality
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 closure
data Graph a = {- DeadEnd | -} a :-->: [Graph a] deriving Show
transitiveClosure location = location :-->: map transitiveClosure (flights location)
{-- define the truncation of any cyclical journeys
finite visited DeadEnd = DeadEnd
finite visited (location :-->: destinations)
| already visited location = DeadEnd
| otherwise = location :-->: map (finite (location : visited)) destinations
already = flip elem
-}
{-- remove any 'DeadEnd's left over
simplify DeadEnd = DeadEnd
simplify (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 visited
holidays = 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 Show
i 0 = Leaf 0
i n = Branch 0 (i (n-1)) (i (n-1))
identity (Leaf i) = Leaf i
identity (Branch i left right) = Branch i (identity left) (identity right)
depth current (Leaf _) = Leaf current
depth current (Branch _ left right) = Branch current (depth (current + 1) left) (depth (current + 1) right)
depth' current (Leaf i) = Leaf i
depth' current (Branch i left right) = Branch i left' right'
where left' = depth' (current + 1) left
right' = depth' (current + 1) right
depth'' 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 right
depth''' 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' right
with = (,)
unfold step current = case step current of Nothing -> current ; Just next -> unfold step next
breadth 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 environment
ty : type
m : term ty
eq_term_dec :
forall (m' : {m' : term ty | size m' < size m}) (n : term ty),
{`m' = n} + {`m' <> n}
n : term ty
eq_term_dec0 :
forall (ty : type) (m n : term ty),
{[m : (term ty)]= [n : (term ty)]} + {m =/= n}
ty0 : type
m0 : term ty0
n0 : term ty0
uTy : type
vTy : type
u : term (uTy --> vTy)
v : term uTy
uTy' : type
vTy' : type
u' : 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_var
u0 : term (uTy --> vTy)
v0 : term uTy
u'0 : term (uTy --> vTy)
v'0 : term uTy
filtered_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
Variadic via GADT
data Pill a where
Stop :: Pill Integer
O :: Pill (Pill a -> a)
collect :: Integer -> Pill a -> a
collect i Stop = i
collect 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
Sunday 9 November 2008
Somewhat Pointfree Haskell Huffman Tree
{-# LANGUAGE NoMonomorphismRestriction #-}
import Prelude hiding (Either(..))
import Data.List
import Data.Maybe
import Data.Ord
import Control.Monad.Reader
lookdown :: (Eq b) => [(a, b)] -> b -> Maybe a
lookdown 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) Branch
depthFirstTraversal = foldHuff return (++)
-- foldHuff (!) (*) t =
-- (return T) ++
-- (return F) ++
-- (return T)
-- = [T,F,T]
member e = foldHuff (== e) (||)
data Direction = Left | Right deriving Show
type 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 . sort
joinTrees ((p1,t1) : (p2,t2) : freqs) = joinTrees (insertBy (comparing fst) (p1 + p2,Branch t1 t2) freqs)
joinTrees [(_,tree)] = tree
huffmanTree = joinTrees . frequencies
codeTable = depthFirstTraversal . label . huffmanTree
encode 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 path
traverse (Branch l r) (Right:path) = traverse r path
traverse _ [] = Nothing
huffmanDecode = 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 string
savings 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
Subscribe to:
Posts (Atom)