FTC Design

Planned features

• High-level ASCII lambda syntax to define a pure function
  • Ident: ^[a-z][a-zA-Z0-9_]*$, which applies to both functions, types, and type constructors
  • Keywords start with uppercase.
  • Recursion is not allowed.
  • Multi-line definition is the same as let binding, which in turn is a syntax sugar for lambda abstraction-application. e.g. f = expr1; g = expr2 compiles to g = (\f. expr2) expr1 if expr2 has a reference to f.

succ = \n f x. f (n f x)
pred = \n f x. n (\g h. h (g f)) (\u. x) (\u. u)
fix = \f. (\x. f (x x)) (\x. f (x x))
true = \x y. x
false = \x y. y
iszero = \n. n (\x. false) true
mult = \m n f. m (n f)
facfix = \f n. (iszero n) (\f x. f x) (mult n (f (pred n)))
fac = fix facfix

• Syntax sugar for Church/Scott numerals and lists
  • 123 for Church numeral (type nat), $123 for Scott numeral (type natS)
  • [a, b, c] for Church list (type list T), $[a, b, c] for Scott list (type listS T; $[ is a single token)
  • "xyz" == [ord('x'), ord('y'), ord('z')], which has type list nat
• Custom type declarations for Scott encoding
  • The language itself is untyped; types are only used for I/O in test cases, and an error will be generated at runtime if the output cannot be interpreted as having the given type

Type natS = zeroS | succS natS
-- which generates
zeroS = \c1 c2. c1
succS = \n. \c1 c2. c2 n
-- and formatting will be done by
-- `fmt_natS = \f. f print_zeroS print_succS`
-- where a call of `print_zeroS` will print `"zeroS"` and `print_succS n` will print `"succS(" + fmt_natS n + ")"`

• Optimizing lambda-to-SKI compiler
  • Can be ported from AndersK's one and another one from the creator of Crazy L
  • Also Church literals may use AndersK's results hardcoded (running at runtime is infeasible)
• Test cases support
  • Test fn [args...] As ty should run fn on args and format the result using type declaration ty
• Compiler, post formatter, source importer for BLC, BCL, SKI, Unlambda, Iota, Jot, Godel-LC
  • Import* "filepath" As fnname would do, where * is one of BLC, BCL, SKI, Unlambda, Iota, Jot, GodelLC

Open questions

• How to justify the byte count of Godel-LC (or other langs, for that matter)?
  • A way to reference an external file would be enough. That way I can claim "the size of this file is the size of the function".
  • Such a statement would look like ImportGodel "filepath" as name
• Good way to compile code like this:

f1 = expr1
f2 = f1_smth2
f3 = f1_smth3
f4 = f2_f3_smth
-- naive:
f4 = (\f1. (\f2. (\f3. f2_f3_smth ) f1_smth3 ) f1_smth2 ) expr1
-- is this better?
f4 = (\f1. (\f2. \f3. f2_f3_smth) f1_smth2 f1_smth3) expr1
-- it has equal term size, but lower de Bruijn indices overall
-- which is slightly better for BLC coding... but probably not worth the effort;
-- human can (and should) hand-optimize various aspects anyway

NBE-based normalizer

• Supplied by reddit user Noughtmare
• Claims to rely on the laziness of NBEEnv

data ULC = Var !Int | Lam ULC | App ULC ULC
  deriving (Show, Eq, Generic)
data NBEVal = VFree !Int | VVar !Int | VApp !NBEVal !NBEVal | VLam !NBEClosure
  deriving Show
data NBEClosure = Closure !NBEEnv !ULC deriving Show
data NBEEnv = EEmpty | ECons NBEVal NBEEnv deriving Show
semanticNBE e = quote 1 (eval EEmpty e) where
  ($$) :: NBEClosure -> NBEVal -> NBEVal
  ($$) (Closure env t) u = eval (ECons u env) t
  elookup :: Int -> NBEEnv -> NBEVal
  elookup i EEmpty = VFree i
  elookup 1 (ECons x _) = x
  elookup n (ECons _ xs) = elookup (n-1) xs
  eval :: NBEEnv -> ULC -> NBEVal
  eval env = \case
    Var i -> elookup i env
    Lam t -> VLam (Closure env t)
    App t u -> case (eval env t, eval env u) of
      (VLam t, u) -> t $$ u
      (t, u) -> VApp t u
  quote :: Int -> NBEVal -> ULC
  quote l = \case
    VFree i -> Var i
    VVar i -> Var (l - i)
    VLam t -> Lam (quote (l + 1) (t $$ VVar l))
    VApp t u -> App (quote l t) (quote l u)