Definition
PLAN is a combinator interpreter. It is defined by the following pseudocode:
Every PLAN vaue is either a pin x:<i>, a law x:{n a b}, an app x:(f g), a
nat x:@, or a black hole x:<>. Black holes only exist during evaluation.
(o <- x) mutates o in place, replacing it's value with x.
Run F(x) to normalize a value.
E(o:@) = o | F(o) =
E(o:<x>) = o | E(o)
E(o:(f x)) = | when o:(f x)
E(f) | F(f); F(x)
when A(f)=1 | o
o <- X(o,o) |
E(o) | N(o) = E(o); if o:@ then o else 0
o |
E(o:{n a b}) = | I(f, (e x), 0) = x
if a!=0 then o else | I(f, e, 0) = e
o <- <> | I(f, (e x), n) = I(f, e, n-1)
o <- R(0,o,b) | I(f, e, n) = f
E(o) |
| A((f x)) = A(f)-1
X((f x), e) = X(f,e) | A(<p>) = A(p)
X(<p>, e) = X(p,e) | A({n a b}) = a
X({n a b}, e) = R(a,e,b) | A(n:@) = I(1, (3 5 3), n)
X(0, (_ n a b)) = {N(n) N(a) F(b)} |
X(1, (_ p l a n x)) = P(p,l,a,n,E(x)) | R(n,e,b:@) | b≤n = I(x,e,(n-b))
X(2, (_ z p x)) = C(z,p,N(x)) | R(n,e,(0 f x)) = (R(n,e,f) R(n,e,x))
X(3, (_ x)) = N(x)+1 | R(n,e,(1 v b)) = L(n,e,v,b)
X(4, (_ x)) = <F(x)> | R(n,e,(2 x)) = x
| R(n,e,x) = x
C(z,p,n) = if n=0 then z else (p (n-1)) |
| L(n,e,v,b) =
P(p,l,a,n,(f x)) = (a f x) | x := <>
P(p,l,a,n,<x>) = (p x) | f := (e x)
P(p,l,a,n,{n a b}) = (l n a b) | x <- R(n+1,f,v)
P(p,l,a,n,x:@} = (n x) | R(n+1,f,b)A Haskell implementation is about 180 lines, with examples:
import Control.DeepSeq
import Numeric.Natural
import Data.List
data Val
= PIN !Val
| LAW !Natural !Natural !Val
| APP !Val Val
| NAT !Natural
instance NFData Val where
rnf (APP f x) = rnf f `seq` rnf x
rnf _ = ()
f % x | arity f == 1 = subst f [x]
f % x | otherwise = APP f x
arity (APP f _) = arity f - 1
arity (PIN (NAT n)) = case n of 1->3; 3->3; 4->5; _->1
arity (PIN i) = arity i
arity (LAW _ a _) = fromIntegral a :: Integer
arity (NAT n) = 0
pat p _ _ _ (PIN x) = (p % x)
pat _ l _ _ (LAW n a b) = (l % NAT n % NAT a % b)
pat _ _ a _ (APP f x) = (a % f % x)
pat _ _ _ n x@NAT{} = (n % x)
kal n e (NAT b) | b<=n = e !! fromIntegral (n-b)
kal n e (NAT 0 `APP` f `APP` x) = (kal n e f % kal n e x)
kal _ _ (NAT 2 `APP` x) = x
kal _ _ x = x
run :: Natural -> [Val] -> Val -> Val
run arity ie body = res
where (n, e, res::Val) = go arity ie body
go i acc (NAT 1 `APP` v `APP` k') = go (i+1) (kal n e v : acc) k'
go i acc x = (i, acc, kal n e x)
subst (APP f x) xs = subst f (x:xs)
subst x@(PIN l@LAW{}) xs = exec l (x:xs)
subst (PIN i) xs = subst i xs
subst x xs = exec x (x:xs)
nat (NAT n) = n
nat _ = 0
exec (LAW n a b) xs = run a (reverse xs) b
exec (NAT 0) [_,x] = PIN (force x)
exec (NAT 1) [_,n,a,b] | nat a > 0 = LAW (nat n) (nat a) (force b)
exec (NAT 2) [_,x] = NAT (nat x + 1)
exec (NAT 3) [_,z,p,x] = case nat x of 0->z; n->(p % NAT (n-1))
exec (NAT 4) [_,p,l,a,n,x] = pat p l a n x
exec f e = error $ show ("crash", (f:e))
-- Some Examples ---------------------------------------------------------------
instance Num Val where fromInteger i = NAT (fromIntegral i)
showApp (APP f x) xs = showApp f (x:xs)
showApp f xs = "(" <> intercalate " " (show <$> (f:xs)) <> ")"
instance Show Val where
show (PIN i) = concat ["<", show i, ">"]
show (LAW n a b) = concat ["{", show n, " ", show a, " ", show b, "}"]
show (APP f x) = showApp f [x]
show (NAT n) = show n
pin=(PIN 0)
law=(PIN 1)
inc=(PIN 2)
natCase=(PIN 3)
planCase=(PIN 4)
k = law % 0 % 2 % 1 -- k a _ = a
k3 = law % 0 % 4 % 1 -- k3 v _ _ _ = v
i = law % 0 % 1 % 1 -- i x = x
z1 = law % 0 % 1 % (2 % 0) -- z1 _ = 0
z3 = law % 0 % 3 % (2 % 0) -- z3 _ _ _ = 0
appHead=(planCase % 0 % 0 % k % 0)
toNat=(natCase % 0 % inc)
dec=(natCase % 0 % i)
-- helpers for building laws
a f x = (0 % f % x)
lawE n a b = (law % n % a % b)
-- length of an array
--
-- lenHelp len h t = inc (len h)
-- len x = planCase z1 z3 (\len h t -> inc (len h)) n x
lenHelp = lawE 0 3 (inc `a` (1 `a` 2))
len = lawE 0 1 (((planCase % z1 % z3) `a` (lenHelp `a` 0)) `a` z1 `a` 1)
-- getting the tag of an ADT:
--
-- head (APP h t) = h
-- head x = x
--
-- tag x = toNat (head x)
head' = lawE 0 3 (1 `a` 2) -- \head h t -> head h
headF = lawE 0 1 (planCase `a` (k `a` 1) `a` (k3 `a` 1) `a` (head' `a` 0) `a` i `a` 1)
tag = lawE 0 1 (toNat `a` (headF `a` 1))
chk :: Val -> Val -> IO ()
chk x y = do
putStrLn ("assert " <> show x <> " " <> show y)
if (x == y) then pure () else error "FAIL"
deriving instance Eq Val
main = do
-- increment, make a law, make a pin
chk 5 $ inc % 4
chk (LAW 1 2 3) $ law % 1 % 2 % 3
chk (PIN 5) $ pin % (inc % 4)
-- pattern match on nats
chk 9 $ toNat % 9
chk 0 $ toNat % (pin % 9)
-- pattern match on PLAN values
chk (1%2) (planCase % 1 % 0 % 0 % 0 % (pin%2))
chk (1%2%3%4) (planCase % 0 % 1 % 0 % 0 % (law%2%3%4))
chk (1%2%3) (planCase % 0 % 0 % 1 % 0 % (2%3))
chk (1%2) (planCase % 0 % 0 % 0 % 1 % 2)
-- basic laws
chk (LAW 0 2 0) $ law % 0 % 2 % 0 % 7 % 8
chk 7 $ law % 0 % 2 % 1 % 7 % 8
chk 8 $ law % 0 % 2 % 2 % 7 % 8
chk 3 $ law % 0 % 2 % 3 % 7 % 8
-- force a value by using it to build a law and the running it.
chk 1 (law % 0 % 1 % (2 % 1) % 0)
-- select finite part of infinite value
chk 1 (appHead % (law % 99 % 1 % (1 % (0%1%2) % 2) % 1))
-- running pins:
chk (LAW 1 2 0) $ pin % law % 1 % 2 % 0
chk (LAW 1 2 0) $ pin % (law%1) % 2 % 0
chk (PIN(LAW 1 2 0)) $ pin % (law%1%2%0) % 3 % 4
chk (PIN(LAW 1 2 0)) $ pin % (pin % (law%1%2%0)) % 3 % 4
chk 9 ( law % 0 % 1 % 1 % 9 )
chk 8 ( law % 0 % 1 % (1 % 1 % 2) % 8 )
chk 7 ( law % 0 % 1 % -- ? ($0 $1)
(1 % 3 % -- @ $2 = $3
(1 % 7 % -- @ $3 = 9
2)) -- $2
% 9)
-- more complex example
chk (1%(0%2))
(law%0%1% -- | ? ($0 $1)
(1% (0%(2%0)%3)% -- @ $2 = (0 $3)
(1% (2%2)% -- @ $3 = 2
(0%1%2)))% -- | ($1 $2)
1) -- 1
-- trivial cycles are okay if not used.
chk 7 ( (law % 0 % 1 % -- | ? ($0 $1)
(1% 7% -- @ $2 = 7
(1% 3% -- @ $3 = $3
-- $2
2))% -- 9
9))
-- length of array
chk 9 (len % (0 % 1 % 2 % 3 % 4 % 5 % 6 % 7 % 8 % 9))
-- head of closure
chk 7 (headF % (7 % 1 % 2 % 3 % 4 % 5 % 6 % 7 % 8 % 9))
chk law (headF % (law % 1 % 2))
-- tag of ADT (head cast to nat)
chk 7 (tag % (7 % 1 % 2 % 3 % 4 % 5 % 6 % 7 % 8 % 9))
chk 0 (tag % (law % 1 % 2))Last updated