TAPL 练习代码 （Haskell 版）

​ 这是一个垃圾堆，以后可能会慢慢附上说明。

4.1 - An ML Implementation of Arithmetic Expressions

data Term = TmTrue 
            | TmFalse
			| TmIf Term Term Term
			| TmZero
			| TmSucc Term
			| TmPred Term
			| TmIsZero Term deriving (Show, Eq)
			
isnumericval :: Term -> Bool

isnumericval TmZero = True
isnumericval (TmSucc(t1)) = isnumericval t1
isnumericval _ = False

isval :: Term -> Bool

isval TmTrue = True
isval TmFalse = True
isval t = isnumericval t

eval1 :: Term -> Term

eval1 (TmIf TmTrue t2 t3) = t2
eval1 (TmIf TmFalse t2 t3) = t3
eval1 (TmIf t1 t2 t3) = TmIf t1' t2 t3
                           where t1' = eval1 t1
eval1 (TmSucc t1) = TmSucc(t1')
                     where t1' = eval1 t1
eval1 (TmPred TmZero) = error "No such value"
eval1 (TmPred (TmSucc t1)) = if isnumericval t1 then t1 else error "No such value"
eval1 (TmPred t1) = TmPred(t1')
                     where t1' = eval1 t1
eval1 (TmIsZero TmZero) = TmTrue
eval1 (TmIsZero (TmSucc t1)) = TmFalse
eval1 (TmIsZero _) = error "No such value"
eval1 t = t -- no rule applies

eval :: Term -> Term -- multi-stepped evaluation
eval t = if t' == t then t else eval t'
		where t' = eval1 t

arith :: Term -> Term -- expected to be big-stepped
arith (TmIf t1 t2 t3) = if b1 == TmTrue then arith t2 else arith t3
						where b1 = arith t1
arith (TmSucc t1) = TmSucc $ arith t1
arith (TmPred (TmSucc t1)) = arith t1
arith (TmIsZero t1) = if t1' == TmZero then TmTrue else TmFalse
                      where t1' = arith t1
arith _ = error "No rule applies"

5.2 Programming in the Lambda-Calculus

type Bool' a b c = a -> b -> c

tru :: Bool' a b a
tru = \t -> \f -> t

fls :: Bool' a b b
fls = \t -> \f -> f

test :: Bool' a b c -> a -> b -> c
test = \l -> \m -> (\n -> l m n)

and' = \u -> \v -> (u v fls)

or' = \u -> \v -> (u tru v)

not' = flip -- \l -> \t -> \f -> (l f t)

as_bool :: (Bool' Bool Bool Bool) -> Bool
as_bool = \u -> u True False

5.2.1 Defining Logical Functions

type Bool' a b c = a -> b -> c

tru :: Bool' a b a
tru = \t -> \f -> t

fls :: Bool' a b b
fls = \t -> \f -> f

test :: Bool' a b c -> a -> b -> c
test = \l -> \m -> (\n -> l m n)

and' = \u -> \v -> (u v fls)

or' = \u -> \v -> (u tru v)

not' = flip -- \l -> \t -> \f -> (l f t)

as_bool :: (Bool' Bool Bool Bool) -> Bool
as_bool = \u -> u True False

type Pair a b c = a -> b -> (a -> b -> c) -> c

pair :: Pair a b c
pair = \f -> \s -> \b -> b f s

fst' = \p -> p tru

snd' = \p -> p fls

5.2.2+ Numerical System

type LmNat a b c = a -> b -> c
c0 = \s -> \z -> z
-- Note that c0 is equivalent to that of `False`
c1 = \s -> \z -> s z
c2 = \s -> \z -> s $ s z

scc = \n -> \s -> \z -> s (n s z)

-- Somewhat clumsy definition
scc' = \n -> \s -> \z -> c1 s (n s z)

-- The alternative definition could be easily spotted underneath
-- in that of `prd`
plus = \x -> \y -> \s -> \z -> x s (y s z)

times = \x -> \y -> x (plus y) c0

pow = \x -> \y -> y (times x) c1

-- Natural number wrappings
data Nat = Zero | Succ Nat deriving Show

-- eval natural number
as_num :: LmNat (Nat -> Nat) Nat Nat -> Nat
as_num = \n -> n Succ Zero

-- Previous logic system
tru = \t -> \f -> t
fls = \t -> \f -> f
as_bool = \u -> u True False

iszero = \n -> n ss zz
        where zz = tru
              ss = \_ -> fls

-- Previous pair system
type Pair a b c = a -> b -> (a -> b -> c) -> c
pair :: Pair a b c
pair = \f -> \s -> \b -> b f s
fst' = \p -> p tru
snd' = \p -> p fls

-- This wouldn't work in haskell ~ because this laji could not infer infinite type
prd = \x -> fst' (x zz ss)
     where zz = pair c0 c0
           ss = \p -> pair (snd' p) (plus c1 $ fst' p)
-- Approximately (n + 1) steps of big-stepped evaluation is required to compute `prd`

-- So this would not work
sub = \x -> \y -> \s -> \z -> y prd (x s z) 

-- So do this
equal = \x -> \y -> iszero $ sub x y

5.2.8 Lambda-Styled List

nil = \c -> \n -> n

l1 = \x -> \c -> \n -> c x n

l2 = \x -> \y -> \c -> \n -> c x ( c y n ) 

cons = \h -> \t -> \c -> \n -> t c ( c h n )

-- Previous logic system
tru = \t -> \f -> t
fls = \t -> \f -> f
as_bool = \u -> u True False

isnil = \c -> c ss zz
        where zz = tru
              ss = \n -> \_ -> fls

data List a = Cons a (List a) | Nil deriving Show

head' = \c -> c head'' ()
       where head'' = \n -> \_ -> n

as_list = \l -> l Cons Nil

De Brujin’ indexes

$$
\uparrow^2 \lambda. \lambda. 1 ( 0 \ 2 ) = \lambda. \lambda. 1 ( 0 \ 4 )
$$

$$
\uparrow^2 \lambda. ( 0 \ 1 (\lambda. 0 \ 1 \ 2 ) ) = \lambda. 0 \ 3 (\lambda. 0 \ 1 \ 4)
$$

$$
Substitution: \
[b \rightarrow a] (b (\lambda x. \lambda y. b)) \
= [1 \rightarrow 0] (1 \ (\lambda . \lambda . 3)) \
= (0 (\lambda. \lambda. 2))
$$

更多代码已经迁移到私有repo中，施工中…