what happens when you write functional code without a type checker

no type checker.hs

Result:
  sigma_elim (bool_elim (\a -> (\b -> (\c -> \d -> (\e -> \f -> \g -> pair true g) c tt d) ((\c -> (\d -> d d) (\d -> c (d d))) (\c -> (\d -> \e -> tt) c tt))) a ((\b -> (\c -> (\d -> (\e -> \f -> (\g -> g) (\g -> \h -> (\i -> i) ((\i -> (\j -> \k -> \l -> (\m -> m) (\m -> \n -> (\o -> (\p -> p) (sigma_elim (bool_elim m n))) (\o -> tt))) e tt f g ((\j -> \k -> j) h)) (\i -> f ((\j -> (\k -> \l -> \m -> pair false m) j tt tt) e))))) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt)) ((\e -> \f -> \g -> f) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt)) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt))) d ((\e -> (\f -> (\g -> (\h -> \i -> (\j -> j) (\j -> \k -> (\l -> l) ((\l -> (\m -> \n -> \o -> (\p -> p) (\p -> \q -> (\r -> (\s -> s) (sigma_elim (bool_elim p q))) (\r -> tt))) h tt i j ((\m -> \n -> m) k)) (\l -> i ((\m -> (\n -> \o -> \p -> pair false p) m tt tt) h))))) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)) ((\h -> \i -> \j -> i) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt))) g ((\h -> (\i -> \j -> \k -> pair false k) h tt tt) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)))) (\g -> (\h -> \i -> (\j -> (\k -> (\l -> (\m -> m) (\m -> \n -> (\o -> (\p -> (\q -> q q) (\q -> p (q q))) o) (\o -> (\p -> (\q -> \r -> (\s -> s) (\s -> \t -> (\u -> u) ((\u -> (\v -> \w -> \x -> (\y -> y) (\y -> \z -> (\a -> (\b -> b) (sigma_elim (bool_elim y z))) (\a -> tt))) q tt r s ((\v -> \w -> v) t)) (\u -> r ((\v -> (\w -> \x -> \y -> pair false y) v tt tt) q))))) ((\q -> (\r -> r r) (\r -> q (r r))) (\q -> (\r -> \s -> tt) q tt)) k p m) (\p -> n p (o p))))) tt) ((\k -> \l -> \m -> l) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt)) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt))) i j) (\j -> (\k -> \l -> (\m -> \n -> \o -> pair true o) k tt l) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt)))) g (f g))) (e e)) (\e -> (\f -> (\g -> (\h -> \i -> (\j -> j) (\j -> \k -> (\l -> l) ((\l -> (\m -> \n -> \o -> (\p -> p) (\p -> \q -> (\r -> (\s -> s) (sigma_elim (bool_elim p q))) (\r -> tt))) h tt i j ((\m -> \n -> m) k)) (\l -> i ((\m -> (\n -> \o -> \p -> pair false p) m tt tt) h))))) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)) ((\h -> \i -> \j -> i) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt))) g ((\h -> (\i -> \j -> \k -> pair false k) h tt tt) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)))) (\g -> (\h -> \i -> (\j -> (\k -> (\l -> (\m -> m) (\m -> \n -> (\o -> (\p -> (\q -> q q) (\q -> p (q q))) o) (\o -> (\p -> (\q -> \r -> (\s -> s) (\s -> \t -> (\u -> u) ((\u -> (\v -> \w -> \x -> (\y -> y) (\y -> \z -> (\a -> (\b -> b) (sigma_elim (bool_elim y z))) (\a -> tt))) q tt r s ((\v -> \w -> v) t)) (\u -> r ((\v -> (\w -> \x -> \y -> pair false y) v tt tt) q))))) ((\q -> (\r -> r r) (\r -> q (r r))) (\q -> (\r -> \s -> tt) q tt)) k p m) (\p -> n p (o p))))) tt) ((\k -> \l -> \m -> l) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt)) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt))) i j) (\j -> (\k -> \l -> (\m -> \n -> \o -> pair true o) k tt l) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt)))) g (f g))) (e e)) ((\e -> \f -> (\g -> \h -> \i -> pair true i) e tt f) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt)) ((\e -> \f -> (\g -> \h -> \i -> pair true i) e tt f) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt)) ((\e -> (\f -> \g -> \h -> pair false h) e tt tt) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt))))))) (\d -> (\e -> (\f -> \g -> (\h -> \i -> \j -> pair true j) f tt g) ((\f -> (\g -> g g) (\g -> f (g g))) (\f -> (\g -> \h -> tt) f tt))) d (c d))) (b b)) (\b -> (\c -> (\d -> (\e -> \f -> (\g -> g) (\g -> \h -> (\i -> i) ((\i -> (\j -> \k -> \l -> (\m -> m) (\m -> \n -> (\o -> (\p -> p) (sigma_elim (bool_elim m n))) (\o -> tt))) e tt f g ((\j -> \k -> j) h)) (\i -> f ((\j -> (\k -> \l -> \m -> pair false m) j tt tt) e))))) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt)) ((\e -> \f -> \g -> f) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt)) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt))) d ((\e -> (\f -> (\g -> (\h -> \i -> (\j -> j) (\j -> \k -> (\l -> l) ((\l -> (\m -> \n -> \o -> (\p -> p) (\p -> \q -> (\r -> (\s -> s) (sigma_elim (bool_elim p q))) (\r -> tt))) h tt i j ((\m -> \n -> m) k)) (\l -> i ((\m -> (\n -> \o -> \p -> pair false p) m tt tt) h))))) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)) ((\h -> \i -> \j -> i) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt))) g ((\h -> (\i -> \j -> \k -> pair false k) h tt tt) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)))) (\g -> (\h -> \i -> (\j -> (\k -> (\l -> (\m -> m) (\m -> \n -> (\o -> (\p -> (\q -> q q) (\q -> p (q q))) o) (\o -> (\p -> (\q -> \r -> (\s -> s) (\s -> \t -> (\u -> u) ((\u -> (\v -> \w -> \x -> (\y -> y) (\y -> \z -> (\a -> (\b -> b) (sigma_elim (bool_elim y z))) (\a -> tt))) q tt r s ((\v -> \w -> v) t)) (\u -> r ((\v -> (\w -> \x -> \y -> pair false y) v tt tt) q))))) ((\q -> (\r -> r r) (\r -> q (r r))) (\q -> (\r -> \s -> tt) q tt)) k p m) (\p -> n p (o p))))) tt) ((\k -> \l -> \m -> l) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt)) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt))) i j) (\j -> (\k -> \l -> (\m -> \n -> \o -> pair true o) k tt l) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt)))) g (f g))) (e e)) (\e -> (\f -> (\g -> (\h -> \i -> (\j -> j) (\j -> \k -> (\l -> l) ((\l -> (\m -> \n -> \o -> (\p -> p) (\p -> \q -> (\r -> (\s -> s) (sigma_elim (bool_elim p q))) (\r -> tt))) h tt i j ((\m -> \n -> m) k)) (\l -> i ((\m -> (\n -> \o -> \p -> pair false p) m tt tt) h))))) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)) ((\h -> \i -> \j -> i) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt))) g ((\h -> (\i -> \j -> \k -> pair false k) h tt tt) ((\h -> (\i -> i i) (\i -> h (i i))) (\h -> (\i -> \j -> tt) h tt)))) (\g -> (\h -> \i -> (\j -> (\k -> (\l -> (\m -> m) (\m -> \n -> (\o -> (\p -> (\q -> q q) (\q -> p (q q))) o) (\o -> (\p -> (\q -> \r -> (\s -> s) (\s -> \t -> (\u -> u) ((\u -> (\v -> \w -> \x -> (\y -> y) (\y -> \z -> (\a -> (\b -> b) (sigma_elim (bool_elim y z))) (\a -> tt))) q tt r s ((\v -> \w -> v) t)) (\u -> r ((\v -> (\w -> \x -> \y -> pair false y) v tt tt) q))))) ((\q -> (\r -> r r) (\r -> q (r r))) (\q -> (\r -> \s -> tt) q tt)) k p m) (\p -> n p (o p))))) tt) ((\k -> \l -> \m -> l) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt)) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt))) i j) (\j -> (\k -> \l -> (\m -> \n -> \o -> pair true o) k tt l) ((\k -> (\l -> l l) (\l -> k (l l))) (\k -> (\l -> \m -> tt) k tt)))) g (f g))) (e e)) ((\e -> \f -> (\g -> \h -> \i -> pair true i) e tt f) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt)) ((\e -> \f -> (\g -> \h -> \i -> pair true i) e tt f) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt)) ((\e -> (\f -> \g -> \h -> pair false h) e tt tt) ((\e -> (\f -> f f) (\f -> e (f f))) (\e -> (\f -> \g -> tt) e tt))))))) (\d -> (\e -> (\f -> \g -> (\h -> \i -> \j -> pair true j) f tt g) ((\f -> (\g -> g g) (\g -> f (g g))) (\f -> (\g -> \h -> tt) f tt))) d (c d))) (b b)) a)) ((\a -> \b -> a) ((\a -> (\b -> (\c -> (\d -> \e -> (\f -> f) (\f -> \g -> (\h -> h) ((\h -> (\i -> \j -> \k -> (\l -> l) (\l -> \m -> (\n -> (\o -> o) (sigma_elim (bool_elim l m))) (\n -> tt))) d tt e f ((\i -> \j -> i) g)) (\h -> e ((\i -> (\j -> \k -> \l -> pair false l) i tt tt) d))))) ((\d -> (\e -> e e) (\e -> d (e e))) (\d -> (\e -> \f -> tt) d tt)) ((\d -> \e -> \f -> e) ((\d -> (\e -> e e) (\e -> d (e e))) (\d -> (\e -> \f -> tt) d tt)) ((\d -> (\e -> e e) (\e -> d (e e))) (\d -> (\e -> \f -> tt) d tt))) c ((\d -> (\e -> \f -> \g -> pair false g) d tt tt) ((\d -> (\e -> e e) (\e -> d (e e))) (\d -> (\e -> \f -> tt) d tt)))) (\c -> (\d -> \e -> (\f -> (\g -> (\h -> (\i -> i) (\i -> \j -> (\k -> (\l -> (\m -> m m) (\m -> l (m m))) k) (\k -> (\l -> (\m -> \n -> (\o -> o) (\o -> \p -> (\q -> q) ((\q -> (\r -> \s -> \t -> (\u -> u) (\u -> \v -> (\w -> (\x -> x) (sigma_elim (bool_elim u v))) (\w -> tt))) m tt n o ((\r -> \s -> r) p)) (\q -> n ((\r -> (\s -> \t -> \u -> pair false u) r tt tt) m))))) ((\m -> (\n -> n n) (\n -> m (n n))) (\m -> (\n -> \o -> tt) m tt)) g l i) (\l -> j l (k l))))) tt) ((\g -> \h -> \i -> h) ((\g -> (\h -> h h) (\h -> g (h h))) (\g -> (\h -> \i -> tt) g tt)) ((\g -> (\h -> h h) (\h -> g (h h))) (\g -> (\h -> \i -> tt) g tt))) e f) (\f -> (\g -> \h -> (\i -> \j -> \k -> pair true k) g tt h) ((\g -> (\h -> h h) (\h -> g (h h))) (\g -> (\h -> \i -> tt) g tt)))) c (b c))) (a a)) (\a -> (\b -> (\c -> (\d -> \e -> (\f -> f) (\f -> \g -> (\h -> h) ((\h -> (\i -> \j -> \k -> (\l -> l) (\l -> \m -> (\n -> (\o -> o) (sigma_elim (bool_elim l m))) (\n -> tt))) d tt e f ((\i -> \j -> i) g)) (\h -> e ((\i -> (\j -> \k -> \l -> pair false l) i tt tt) d))))) ((\d -> (\e -> e e) (\e -> d (e e))) (\d -> (\e -> \f -> tt) d tt)) ((\d -> \e -> \f -> e) ((\d -> (\e -> e e) (\e -> d (e e))) (\d -> (\e -> \f -> tt) d tt)) ((\d -> (\e -> e e) (\e -> d (e e))) (\d -> (\e -> \f -> tt) d tt))) c ((\d -> (\e -> \f -> \g -> pair false g) d tt tt) ((\d -> (\e -> e e) (\e -> d (e e))) (\d -> (\e -> \f -> tt) d tt)))) (\c -> (\d -> \e -> (\f -> (\g -> (\h -> (\i -> i) (\i -> \j -> (\k -> (\l -> (\m -> m m) (\m -> l (m m))) k) (\k -> (\l -> (\m -> \n -> (\o -> o) (\o -> \p -> (\q -> q) ((\q -> (\r -> \s -> \t -> (\u -> u) (\u -> \v -> (\w -> (\x -> x) (sigma_elim (bool_elim u v))) (\w -> tt))) m tt n o ((\r -> \s -> r) p)) (\q -> n ((\r -> (\s -> \t -> \u -> pair false u) r tt tt) m))))) ((\m -> (\n -> n n) (\n -> m (n n))) (\m -> (\n -> \o -> tt) m tt)) g l i) (\l -> j l (k l))))) tt) ((\g -> \h -> \i -> h) ((\g -> (\h -> h h) (\h -> g (h h))) (\g -> (\h -> \i -> tt) g tt)) ((\g -> (\h -> h h) (\h -> g (h h))) (\g -> (\h -> \i -> tt) g tt))) e f) (\f -> (\g -> \h -> (\i -> \j -> \k -> pair true k) g tt h) ((\g -> (\h -> h h) (\h -> g (h h))) (\g -> (\h -> \i -> tt) g tt)))) c (b c))) (a a)) ((\a -> \b -> (\c -> \d -> \e -> pair true e) a tt b) ((\a -> (\b -> b b) (\b -> a (b b))) (\a -> (\b -> \c -> tt) a tt)) ((\a -> \b -> (\c -> \d -> \e -> pair true e) a tt b) ((\a -> (\b -> b b) (\b -> a (b b))) (\a -> (\b -> \c -> tt) a tt)) ((\a -> (\b -> \c -> \d -> pair false d) a tt tt) ((\a -> (\b -> b b) (\b -> a (b b))) (\a -> (\b -> \c -> tt) a tt))))))))