We’ve just finished covering the B language.
Now we’re going to look at the N language, which deals with natural numbers.
The code for N is available here.
This is going to be a relative short tour, since you’ve seen most of this before. The important points are that we’ll be dealing with inductively defined values, and we’ll be looking briefly at the difference between strict and lazy evaluation.
The natural numbers are defined as:
The terms of N are as follows:
We are including here, which represents the predecessor of . Since we don’t have negative numbers, we define .
We can easily create a
Term type in Haskell:
data Term = TmZero | TmSucc Term | TmPred Term
We’ve already mentioned that the natural numbers are either zero or the successor of a natural number. These will be the form of the values of N.
For the zero case, we have:
valueTmZero :: Term -> Maybe Term valueTmZero TmZero = Just TmZero valueTmZero _ = Nothing
For the successor case, we have:
valueTmSucc :: (Term -> Maybe Term) -> Term -> Maybe Term valueTmSucc val (TmSucc tm) = TmSucc <$> val tm valueTmSucc _ _ = Nothing
We have four small-step rules: two of them are reduction rules, and two of them are congruence rules.
The reduction rules define the predecessor function.
pred O we have:
ePredZero :: Term -> Maybe Term ePredZero (TmPred TmZero) = Just TmZero ePredZero _ = Nothing
pred (S n) we have:
ePredSucc :: Term -> Maybe Term ePredSucc (TmPred (TmSucc tm)) = value tm ePredSucc _ = Nothing
The two congruence rules deal are used to keep things moving on when
pred are wrapped around something other than a value.
The rule for
which corresponds to:
eSucc :: (Term -> Maybe Term) -> Term -> Maybe Term eSucc step (TmSucc tm) = do tm' <- step tm return $ TmSucc tm' eSucc _ _ = Nothing
and the rule for
which corresponds to:
ePred :: (Term -> Maybe Term) -> Term -> Maybe Term ePred step (TmPred tm) = do tm' <- step tm return $ TmPred tm' ePred _ _ = Nothing
The rules we have seen so far are for strict evaluation.
The usual distinction between strict and non-strict is related to whether evaluation continues inside of function abstraction or not.
We haven’t covered functions yet, but we now have something similar. Recall that constructors in Haskell are functions, and that natural numbers would be represented by:
data Nat = O | S Nat
so we have a function
S :: Nat -> Nat
With strict evaluation we evaluate the arguments to
S - using
E-Succ - when we come across
S n as the top-level term.
With lazy evaluation we don’t evaluate the argument to
S in either of those cases. The rule
E-PredSucc can still move things forward when we have a
S inside of one of our terms, but the outer ’S’s are left alone.
This means that for lazy evaluation we completely delete the
E-Succ rule above and rely on the other rules to peek inside of the
We also need to update the
V-Succ rule so that it doesn’t look inside of the
S constructor, and so we have:
valueTmSucc :: Term -> Maybe Term valueTmSucc (TmSucc tm) = Just (TmSucc tm) valueTmSucc _ = Nothing
For now we’ll stick to strict evaluation, but we’ll come back to lazy evaluation later in the series.
From this point, we just need to write the code for
QuickCheck support, parsing and printing for N and we’re done.
And that’s all we need to do. If we copy the tests and the REPL across from the B project into the N project, they’ll still work.
That’s partly due to using the same interface, but also partly due to the form and robustness of the PLT theorems that we’re using for our properties.
We are going to look at more uni-typed language before we add some new concepts into the mix.
QuickCheck, parsing and printing for N.
QuickCheck, parsing and pretty-printing.