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 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 :-->: []]

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

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}".

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

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