-- Evaluate a single step.
eval1 :: Expr -> Maybe Expr
eval1 expr = case expr of
Succ t -> Succ <$> (eval1 t)
Pred Zero -> Just Zero
Pred (Succ t) | isNum t -> Just t
Pred t -> Pred <$> (eval1 t)
IsZero Zero -> Just Tr
IsZero (Succ t) | isNum t -> Just Fl
IsZero t -> IsZero <$> (eval1 t)
If Tr c _ -> Just c
If Fl _ a -> Just a
If t c a -> (\t' -> If t' c a) <$> eval1 t
_ -> Nothing
I dont think this typechecks
https://github.com/sdiehl/write-you-a-haskell/blob/master/004_type_systems.md#small-step-semantics