CODEWITHSUNDEEP
haskelllambdafunctional-programmingfactorial
Aria Pahlavan
Aria Pahlavan

Reputation: 1408

Functional Programming à la 1940s: Minimalistic Implementation of Factorial

I have watched the amazing talk by John Hughes titled Why Functional Programming Matters a couple of times and only recently decided to actually try implementing the "minimalist" version of booleans, integers, and of course factorial, as shown in the video.

I implemented true, false, ifte, zero, one, two, iszero, decr and finally fact here as follow:

-- boolean
true x y = x
false x y = y
ifte bool t e = bool t e

-- positive integers
three f x = f $ f $ f x
two f x = f $ f x
one f x = f x
zero f x = x 

-- add and multiplication
add m n f x = m f $ n f x
mul m n f x = m (n f) x 

-- is zero check
iszero n =  n (\_ -> false) true

-- decrement
decr n = 
  n (\m f x -> f (m f zero))
    zero
    (\x->x)
    zero


-- factorial
fact n =
  ifte (iszero n)
    one
    (mul n (fact (decr n)))

Problem

I tested every function, and they all compile and work perfectly, except for decr and fact.

Even though John Hughes promises at 6:37 that his implementation of decr works, it fails to compile with the following error:

error: Variable not in scope: incr

I am not certain how incr should be implemented in (\m f x -> f (m incr zero)).

Now if I define them as incr = (+1) and change the definition of decr to the following, then decr compiles and works fine, but fact still causes compilation failure. 

decr n = 
  n (\m f x -> f (m incr x))
    zero
    (\x->x)
    zero'

Is there a bug in the lambda (\m f x -> f (m incr zero)) used in the definition of decr, or should incr be defined differently?

Update

When I define incr as incr n = (\f x -> f (n f x)), decr n works fine, but fact n fails to compile. Here's the readable portion of the error message:

factorial.hs:30:1: error: • Occurs check: cannot construct the infinite type:

...

| fact n =
| ^^^^^^^^...

...

factorial.hs:33:6: error: • Occurs check: cannot construct the infinite type:

...

• In the third argument of ‘ifte’, namely ‘(mul n (fact (decr n)))’
  In the expression: ifte (iszero n) one (mul n (fact (decr n)))
  In an equation for ‘fact’:
      fact n = ifte (iszero n) one (mul n (fact (decr n)))

...

| (mul n (fact (decr n)))
| ^^^^^^^^^^^^^^^^^^^^^

Note: the complete error message is several pages long.

Upvotes: 1

Views: 233

Answers (2)

leftaroundabout
leftaroundabout

Reputation: 120711

First, let's try to explicitly type everything. Naïvely, all this stuff is parameterised on some type that the Church functions deal with:

type Logical a = a -> a -> a
type Nat a = (a->a) -> a->a

-- boolean
true, false :: Logical a
true x y = x
false x y = y

ifte :: Logical a -> a -> a -> a
ifte = id

incr :: Nat a -> Nat a
incr n f = f . n f

-- integer “literals”
zero, one, two, three :: Nat a
three = incr two
two   = incr one
one   = incr zero
zero _ = id

-- addition and multiplication
add, mul :: Nat a -> Nat a -> Nat a
add m n f = m f . n f
mul m n f = m $ n f

-- zero check
isZero :: Nat a -> Logical a
isZero n = n (const false) true

...ok, here we run into the first problem:

• Couldn't match expected type ‘Logical a’ with actual type ‘a’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      isZero :: forall a. Nat a -> Logical a
    at /tmp/wtmpf-file7834.hs:25:1-28
• In the expression: n (const false) true

The issue is that we try to use the Nat-church-numbers as a function not on the underlying a type that the result Logical is supposed to work with, but on those logicals themselves. I.e. it's actually

isZero :: Nat (Logical a) -> Logical a

It gets worse for decr – this doesn't work:

decr :: Nat a -> Nat a
decr n = n (\m f x -> f (m incr x))
           zero
           id
           zero

because you're trying to use the number for both a logical purpose as in isZero, which requires injecting another Nat layer, but also for just passing on/incrementing. In traditional Hindley-Milner, you'd need to decide on one of these, so it's not possible to make it typecheck.

In modern Haskell, you can make it typecheck, by making the argument polymorphic:

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}
decr :: (∀ α . Nat α) -> Nat a

To avoid carrying around the quantifier, we might make another synonym:

type ANat = ∀ α . Nat α

then it's just

decr :: ANat -> Nat a

And that technique works for the factorial as well:

fact :: ANat -> Nat a
fact n = ifte (isZero n)
      one
      (mul n $ fact (decr n))

Upvotes: 1

Mulan
Mulan

Reputation: 135187

It looks like you're really close

I can show you how to do this using Church's encodings in JavaScript, but not in Haskell, because I don't know how to make some simple combinators type-check in Haskell (U below)

Because JavaScript is strictly evaluated, predicate branches must be wrapped in a lambda

Go ahead and run the snippet – we calculate 8!

const True = a => b =>
  a ()
  
const False = a => b =>
  b ()
  
const IsZero = n =>
  n (x => False) (True)

const Succ = n =>
  f => x => f (n (f) (x))
  
const Pred = n =>
  f => x => n (g => h => h (g (f))) (u => x) (u => u)

const Mult = m => n =>
  f => m (n (f))
  
const Add = m => n =>
  m (Succ) (n)

const one = f => x =>
  f (x)
  
const two =
  Add (one) (one)
  
const four =
  Add (two) (two)
  
const eight =
  Add (four) (four)

const U = f => f (f)

const Fact = U (f => acc => n =>
  IsZero (n)
    (z => acc) // thunks used for predicate branches
    (z => U (f) (Mult (acc) (n)) (Pred (n)))) (one)
    
const result = 
  Fact (eight)
  
// convert church numeral result to a JavaScript number
console.log ('8! =', result (x => x + 1) (0))
// 8! = 40320

If you cheat a little, you can achieve faux laziness by using JavaScript's ?: ternary operator – I'm only showing this so you can see Fact in a more readable form; the above implementation uses only lambdas

const IsZero = n =>
  // cheat by returning JavaScript's true/false booleans
  n (x => false) (true)

const Succ = n =>
  f => x => f (n (f) (x))
  
const Pred = n =>
  f => x => n (g => h => h (g (f))) (u => x) (u => u)

const Mult = m => n =>
  f => m (n (f))
  
const Add = m => n =>
  m (Succ) (n)

const one = f => x =>
  f (x)
  
const two =
  Add (one) (one)
  
const four =
  Add (two) (two)
  
const eight =
  Add (four) (four)

const U = f => f (f)

const Fact = U (f => acc => n =>
  IsZero (n)
    ? acc // now we're sorta cheating using JavaScript's ternary here
    : U (f) (Mult (acc) (n)) (Pred (n))) (one)

const result = 
  Fact (eight)
  
console.log ('8! =', result (x => x + 1) (0))
// 8! = 40320

Upvotes: 3

Related Questions