SKI Combinators

Lib.hs

module Lib
    ( Ski(..)
    , eval
    , someFunc
    ) where

import Test.QuickCheck

data Ski
 = I
 | K
 | S
 | App Ski Ski
 deriving (Show, Eq)

instance Arbitrary Ski where
  arbitrary = do
    f <- arbitrary
    x <- arbitrary
    elements [S, K, I, App f x]

eval :: Ski -> Ski
eval (App (App K x) y) = eval x
eval (App (App (App S x) y) z) = eval $ App (App x z) (App y z)
eval (App I x) = eval x
eval (App K x) = App K $ eval x
eval (App f x) = eval (App (eval f) x)
eval x = x

someFunc :: IO ()
someFunc = putStrLn "someFunc"

Spec.hs

import Lib
import Test.Hspec
import Test.QuickCheck

newtype ExprWithOnlyIAndApp = ExprWithOnlyIAndApp Ski
  deriving Show

instance Arbitrary ExprWithOnlyIAndApp where
  arbitrary = do
    ExprWithOnlyIAndApp f <- arbitrary
    ExprWithOnlyIAndApp x <- arbitrary
    ExprWithOnlyIAndApp <$> elements [I, App f x]

main :: IO ()
main = hspec $ do
  describe "eval" $ do
    it "I is irreducible" $ do
      eval I `shouldBe` I

    it "(I I) reduces to I" $ do
      eval (App I I) `shouldBe` I

    it "(I (I I)) reduces to I" $ do
      eval (App I (App I I)) `shouldBe` I

    it "((I I) I) reduces to I" $ do
      eval (App (App I I) I) `shouldBe` I

    it "arbitrarily nested applications of I only reduce to I" $
      property $ \(ExprWithOnlyIAndApp ski) -> eval ski == I

    it "K is irreducible" $ do
      eval K `shouldBe` K

    it "(K I) is irreducible" $ do
      eval (App K I) `shouldBe` App K I

    it "(K K) is irreducible" $ do
      eval (App K K) `shouldBe` App K K

    it "in (K x), we can't get rid of K but x should be reduced" $
      property $ \(ExprWithOnlyIAndApp ski) -> eval (App K ski) == App K I

    it "((K I) K) reduces to I" $ do
      eval (App (App K I) K) `shouldBe` I

    it "((K K) I) reduces to I" $ do
      eval (App (App K K) I) `shouldBe` K

    it "K K I S K reduces to S" $ do
      eval (App (App (App (App K K) I) S) K) `shouldBe` S

    it "K argument reduces" $
      property $ \(ExprWithOnlyIAndApp ski) -> eval (App (App K ski) K) == I

    it "S is irreducible" $ do
      eval S `shouldBe` S

    it "S I I I reduces to I" $ do
      eval (App (App (App S I) I) I) `shouldBe` I

    it "S K K I reduces to I" $ do
      eval (App (App (App S K) K) I) `shouldBe` I

    context "wikipedia examples" $ do
      it "SKI(KIS) reduces to I" $ do
        eval (App (App (App S K) I) (App (App K I) S)) `shouldBe` I

      it "KS(I(SKSI)) reduces to S" $ do
        eval (App (App K S) (App I  (App (App (App S K ) S ) I )) ) `shouldBe` S

      it "SKIK reduces to K" $ do
        eval (App (App (App S K) I) K) `shouldBe` K