+ ANSWER using right-fold lists:
+
+ ; are xs strictly longer than ys?
+ let longer? = \xs ys. neg (leq? (length xs) (length ys)) in
+
+ ; uncons xs f ~~> f (head xs) (tail xs)
+ let uncons = \xs f. f (head xs) (tail xs) in
+
+ let check = \x p. p (\bool ys. uncons ys (\y ys. pair (and (num_equal? x y) bool) ys)) in
+ let finish = \bool ys. (empty? ys) bool false in
+ let list_equal? = \xs ys. (longer? xs ys) false (xs check (pair true (rev ys)) finish) in
+
+ let get_fringe = Y (\get_fringe. \t.
+ ; this uses a similar pattern to previous problem
+ (singleton? t)
+ t
+ ; else if t is a tree, it contains two or more subtrees
+ (append
+ (get_fringe (head t))
+ ; don't recurse if (tail t) is a singleton
+ ((singleton? (tail t))
+ (get_fringe (second t))
+ ; else it's ok to recurse
+ (get_fringe (tail t))))) in
+
+ Here is some test data:
+
+ let leaf1 = singleton 1 in
+ let leaf2 = singleton 2 in
+ let leaf3 = singleton 3 in
+ let t12 = doubleton leaf1 leaf2 in
+ let t23 = doubleton leaf2 leaf3 in
+ let alpha = cons leaf1 t23 in
+ let beta = doubleton t12 leaf3 in
+ let gamma = doubleton leaf1 t23 in
+ list_equal? (get_fringe gamma) (get_fringe alpha)
+
+ And here are some cleverer implementations of some of the functions used above:
+
+ let box = \a. \v. v a in
+ let singleton? = \xs. xs (\x b. box (b (K true))) (K false) not in
+
+ ; this function works by first converting [x1,x2,x3] into (true,(true,(true,(K false))))
+ ; then each element of ys unpacks that stack by applying its fst to its snd and itself
+ ; so long as we've not gotten to the end, this will have the result of selecting the snd each time
+ ; when we get to the end of the stack, ((K false) fst) ((K false) snd) (K false) ~~> K false
+ ; after ys are done iterating, we apply the result to fst, which will give us either true or ((K false) fst) ~~> false
+ let longer? = \xs ys. ys (\y p. (p fst) (p snd) p) (xs (\x. pair true) (K false)) fst in
+
+ let shift = \x t. t (\a b c. triple (cons x a) a (pair x))) in
+ let uncons = \xs. xs shift (triple empty empty (K err_head)) (\a b c. c b) in
+ ...