Find tree height using folde function in Haskell

The assignment says it should treat T and F as height 1. It goes on that Not x should evaluate to height x + 1. And and Or has the height of its tallest subtree + 1.

You can write this pretty directly with explicit recursion:

height T = 1
height F = 1
height (Not x) = height x + 1
height (And x y) = max (height x) (height y) + 1
height (Or  x y) = max (height x) (height y) + 1

Now, how do you write this with folde? The key thing about recursive folding is that folde gives each of your functions the result of folding all the subtrees. When you folde on And l r, it folds both subtrees first, and then passes those results into the argument to folde. So, instead of you manually calling height x, folde is going to calculate that for you and pass it as an argument, so your own work ends up something like \x y -> max x y + 1. Essentially, split height into 5 definitions, one per constructor, and instead of destructuring and recursing down subtrees, take the heights of the subtrees as arguments:

heightT = 1 -- height T = 1
heightF = 1 -- height F = 1
heightN x = x + 1 -- height (Not x) = height x + 1
heightA l r = max l r + 1 -- height (And l r) = max (height l) (height r) + 1
heightO l r = max l r + 1 -- height (Or  l r) = max (height l) (height r) + 1

Feed them to folde, and simplify

height = folde 1 1  -- T F
               ao   -- And
               ao   -- Or
               (+1) -- Not
         where ao x y = max x y + 1

data ExpF a = T | F | Not a | And a a | Or a a
              deriving (Functor, Foldable, Traversable)

This looks like your Exp, except instead of recursion it's got a type parameter and a bunch of holes for values of that type. Now, take a look at the types of expressions under ExpF:

T :: forall a. ExpF a
Not F :: forall a. ExpF (ExpF a)
And F (Not T) :: forall a. ExpF (ExpF (ExpF a))

If you set a = ExpF (ExpF (ExpF (ExpF (ExpF ...)))) (on to infinity) in each of the above, you find that they can all be made to have the same type:

T             :: ExpF (ExpF (ExpF ...))
Not F         :: ExpF (ExpF (ExpF ...))
And F (Not T) :: ExpF (ExpF (ExpF ...))

Infinity is fun! We can encode this infinitely recursive type with Fix

newtype Fix f = Fix { unFix :: f (Fix f) }
-- Compare
-- Type  level: Fix f = f (Fix f)
-- Value level: fix f = f (fix f)
-- Fix ExpF = ExpF (ExpF (ExpF ...))
-- fix (1:) =    1:(   1:(  1: ...))
-- Recover original Exp
type Exp = Fix ExpF
-- Sprinkle Fix everywhere to make it work
Fix T :: Exp
Fix $ And (Fix T) (Fix $ Not $ Fix F) :: Exp
-- can also use pattern synonyms
pattern T' = Fix T
pattern F' = Fix F
pattern Not' t = Fix (Not t)
pattern And' l r = Fix (And l r)
pattern Or' l r = Fix (Or l r)
T' :: Exp
And' T' (Not' F') :: Exp

And now here's the nice part: one definition of fold to rule them all:

fold :: Functor f => (f a -> a) -> Fix f -> a
fold alg (Fix ffix) = alg $ fold alg <$> ffix
-- ffix :: f (Fix f)
-- fold alg :: Fix f -> a
-- fold alg <$> ffix :: f a
-- ^ Hey, remember when I said folds fold the subtrees first?
-- Here you can see it very literally

Here's a monomorphic height

height = fold $ \case -- LambdaCase extension: \case ... ~=> \fresh -> case fresh of ...
  T -> 1
  F -> 1
  Not x -> x + 1
  And x y -> max x y + 1
  Or  x y -> max x y + 1

And now a very polymorphic height (in your case it's off by one; oh well).

height = fold $ option 0 (+1) . fmap getMax . foldMap (Option . Just . Max)
height $ Fix T -- 0
height $ Fix $ And (Fix T) (Fix $ Not $ Fix F) -- 2

See the recursion-schemes package to learn these dark arts. It also makes this work for base types like [] with a type family, and removes the need to Fix everything with said trickery + some TH.