Programming lab: Natural Numbers Encoding

Introduction

We can encoding different data types in the untyped λ-calculus (Booleans, order pairs, natural numbers, list among others). An encoding of the natural numbers is the Church encoding based on the Church numerals. The aim of this programming assignment is to know an alternative encoding for the natural numbers.

Assignment (80%)

• The data type Expr representing the λ-terms and the betaEq function are defined in Lennart Augustsson's blog Simpler, Easier! You can use the source code of this blog, given the correspondents credit, of course!

• (70%) To implement the functions

        import Numeric.Natural ( Natural )
        import Test.QuickCheck ( (==>), Property, quickCheck )
  
        eN    :: Natural -> Expr
        ePred :: Expr
        eAdd  :: Expr
        eMult :: Expr
      

  where using an encoding different to the Church encoding, the function eN n returns the λ-term associated with the natural number n, and the functions ePred, eAdd and eMult are the λ-terms correspond to the operations of predecessor, addition and multiplication, respectively.

  The lab will be tested with the tests function

        predW :: Expr -> Expr
        addW, multW :: Expr -> Expr -> Expr
  
        propPred :: Natural -> Property
        propPred n = n > 0 ==> betaEq (predW $ eN n) (eN $ n - 1)
  
        propAdd :: Natural -> Natural -> Bool
        propAdd m n = betaEq (addW (eN m) (eN n)) (eN $ m + n)
  
        propMult :: Natural -> Natural -> Bool
        propMult m n = betaEq (multW (eN m) (eN n)) (eN $ m * n)
  
        tests :: IO ()
        tests = do
          quickCheck propPred
          quickCheck propAdd
          quickCheck propMult
      

  The tests function which use the QuickCheck library (install the library from Hackage and see the paper).

  For running the tests function, you must define the functions predW, addW and multW. These functions are wrappers for the functions ePred, eAdd and eMult, respectively.

• (10%)

  • Your lab will be tested using the -Wall, -Wmissing-local-signatures and -Wmissing-signatures options.
  • Annotate (in English) your source code using Haddock. Documentation should explain your solution for the assignment.
  • Improve your implementation with HLint.

Clean code (10%)

Before submitting your code, which includes your README, clean it up:

• Does not have long lines (at most 80 columns).
• Has an uniformly indentation (we recommended two characters).
• Has a consistent layout.
• Has type signatures for everything (included where-clauses and let-definitions).
• Has good comments.
• Has no junk (unused code, commented code, unnecessary code).
• Has no overly complicated function definitions.
• Does not contain any repetitive code.
• Has no tabs.
• Has no unnecessary spaces at the end of a line, or empty lines at the end of a file. (See: Fixing trailing whitespace issues with Emacs ).
• Has spell-checked comments.

Submission (10%)

Submission is electronic. Send an email to asr(at)eafit(dot)edu(dot)co and attach a compressed file (.zip or .tar.gz) with your solution.

Your submission has to include the following:

• NatEncoding.hs, a Haskell module file with your solution for the assignment.
• README (or README.md), a file containing at least the following information.
  • The name of your program.
  • Your name(s).
  • A general description of your program.
  • Information on how to use your program.
  • GHC or Haskell platform version used
• Do not include any other files.

Notes

• The programming lab may either be solved on your own, or jointly with one other student taking the course.
• You are to use the Haskell Platform ≥ 8.0.1 or GHC[i] ≥ 8.0.1.

Foundations of Functional Programming Languages