Puffin

The Puffin Language

The day-to-day reference for writing Puffin: programs and modules, the data model, expressions, types, pattern matching, and how to run things. New to the language? Start with the tutorial (tutorial.html, Puffin for Racketeers). The standard library is catalogued in STDLIB.md, the type system in depth in TYPES.md, and the implementation in DELTA.md.

Programs

A .puf/.scm file is a sequence of top-level forms โ€” function defines, value defines, and expressions โ€” evaluated in order. The last expression's value is printed (unless it's void). The (program ...) wrapper from the course-era compiler is also accepted.

(define greeting 'hello)              ;; a top-level value
(define (shout s) (list s s s))       ;; a function
(println (shout greeting))            ;; an effect
(shout 'done)                         ;; the result: printed

Top-level defines are mutually recursive; value defines are initialized in source order (a function may mention a later global โ€” it's read at call time). Top-level definitions shadow standard-library primitives, so a program that defines its own cons runs unchanged.

Modules

A file is a module (docs/MODULES.md has the full story). (provide name ...) declares its exports โ€” no provide form means everything top-level is exported. (require "path.puf") imports another file's provided names; paths resolve relative to the requiring file.

(require "vec.puf")                     ;; unqualified: dot, norm2
(require "matrix.puf" #:as M)           ;; qualified: M.transpose
(require "util.puf" #:only (twice) #:rename ((twice do-twice)))
(provide area)
(define pi 314159)                      ;; private unless provided
(define (area r) (* pi (* r r)))

Requires must form a DAG (cycles are compile-time errors); each module's top-level effects run once, in depth-first postorder. Signature files (.pufs) optionally constrain a module's exports: (provide #:sig "ring.pufs") checks names and arities and narrows the export set to exactly the signature. Import collisions โ€” two modules providing the same name, or an import colliding with a local define or a reserved word โ€” are compile-time errors; disambiguate with #:as or #:rename. Modules work on every route โ€” the native backends, the bytecode VM, and the browser playground's file tabs โ€” and a file with no require/provide compiles exactly as before.

Values

Fixnums (61-bit), booleans #t/#f, (void), symbols 'foo, the empty list '(), pairs/lists, vectors, strings "...", hashes, sets, and procedures. Only #f is false. eq? is identity (fine for fixnums, booleans, symbols); equal? is structural over pairs, vectors, strings, and the immutable collections.

Expressions

Binding & functions:

(let ([x 1] [y 2]) body ...)          ;; parallel
(let* ([x 1] [y (+ x 1)]) body ...)   ;; sequential
(let loop ([i 0]) ... (loop (+ i 1))) ;; named let; tail calls run in O(1) stack
(letrec ([odd? ...] [even? ...]) ...) ;; mutual recursion
(define (f a b . rest) ...)           ;; variadic: rest binds a list
(lambda args ...)                     ;; all-rest lambda
(lambda (x y) body ...)               ;; or ฮป; closures are first-class
(set! x e)                            ;; mutation (locals and globals)

Bodies support internal defines, scoped letrec*-style over the whole body โ€” inner helpers can be mutually recursive:

(define (outer n)
  (define (ev? k) (if (eq? k 0) #t (od? (- k 1))))
  (define (od? k) (if (eq? k 0) #f (ev? (- k 1))))
  (list (ev? n) (od? n)))

Control:

(if g t f)
(cond [g body ...] ... [else body ...])
(when g body ...)   (unless g body ...)
(case e [(a b) body ...] [else body ...])
(begin e ...)
(while g body ...)
(and e ...) (or e ...) (not e)        ;; `or` returns its first truthy value

Arithmetic & comparison: n-ary + - *; quotient/remainder (checked division); < <= > >= (binary); eq?, equal?.

Data:

'(a 1 (b 2))                          ;; quoted data (symbols, ints, lists)
`(let ([,x ,e]) ,@body)               ;; quasiquote CONSTRUCTION, with splicing
(gensym 'tmp)                         ;; fresh interned symbols
(list 1 2 3)  (cons 1 '())  (car p) (cdr p) (pair? p) (null? p)
(vector 1 2 3) (make-vector n) (vector-ref v i) (vector-set! v i x) (vector-length v)
(hash k v ...)      an immutable hash; the default. equal?-keyed.
(hash-set h k v)    a NEW hash with the mapping added (h untouched)
(hash-remove h k)   a NEW hash without the key
(hash-ref h k) (hash-ref/default h k d) (hash-has-key? h k)
(hash-count h) (hash-keys h)            work on BOTH flavors
(set v ...) (set-add s v) (set-remove s v)   immutable sets, same story
(set-member? s v) (set-count s) (set->list s)

(make-hash) (hash-set! h k v) (hash-remove! h k)   the tolerated
(make-set) (set-add! s v) (set-remove! s v)        MUTABLE variants

"strings"   (string-append a b) (string=? a b) (string-length s)
            (symbol->string x) (string->symbol s)

Puffin is immutable by design. Pairs, strings, and symbols are immutable; hashes and sets are immutable by default โ€” hash-set returns a new hash sharing structure with the old (a persistent HAMT in the native runtime, so it's O(log n), not a copy), and immutable collections compare by value under equal?. Immutable hashes and sets key structurally (by equal?): heap values โ€” lists, vectors, ADTs, computed strings, nested collections โ€” are valid keys and elements, deduped by content, exactly like fixnums and symbols. Mutability is tolerated where you ask for it: set!, vectors (the raw mutable building block), and the make-hash/hash-set! family, which are eq?-keyed open-addressing tables โ€” identity-keyed, so heap keys in a mutable collection are distinguished by object identity, not content.

Predicates: fixnum? boolean? symbol? void? procedure? pair? null? vector? string? hash? set?.

I/O: (read) reads an integer from stdin; (read-all) the rest of stdin as a string; (println e), (display e), (newline), (displayln e); (error e) prints error: <e> and halts.

For writing compilers (see docs/BOOTSTRAP.md): value->string, (format "~a ~a" (list x y)), number->string, string->number, substring, string-byte, string<?, string-join, sort, symbol<?, apply (โ‰ค5 args), map2, set algebra (set-union/set-subtract/set-intersect/list->set), bitwise-and/ior/xor, arithmetic-shift, modulo.

Primitives are first-class-ish: naming one in value position eta-expands it, so (map car xs) works.

Types

Puffin is gradually typed (docs/TYPES.md is the full story): annotations are optional anywhere, _ is the dynamic type, and unannotated code just runs. define-type declares an algebraic datatype; a constructor with fields is an ordinary function, a nullary constructor is a value referenced bare (None, not (None)), and match destructures both.

(define-type (Option a) (None) (Some a))   ;; parameterized ADT
(define-type Expr                          ;; plain ADT
  (Num Int)
  (Add Expr Expr)
  (Mul Expr Expr))

(define (eval-expr [e : Expr]) : Int       ;; annotated formals + result
  (match e
    [(Num n) n]
    [(Add a b) (+ (eval-expr a) (eval-expr b))]
    [(Mul a b) (* (eval-expr a) (eval-expr b))]))

(: scale Int)                              ;; standalone declaration
(define scale 100)
(ann (car xs) Int)                         ;; expression ascription

Checking is bidirectional with consistency โ€” _ is compatible with everything, so typed and untyped code mix freely โ€” and declared boundaries get transient run-time casts with blame. A non-exhaustive match over an ADT warns on stderr; --strict-types (on both bin/puffin and puffincc) promotes the warning to a compile-time error.

Foreign functions

The foreign form imports typed C functions from a shared library (docs/FFI.md has the full design; the tutorial has a worked section):

(define-foreign-type Regex)              ;; an opaque handle type
(foreign "vendor/libpfregex.dylib"       ;; dlopen'd at module load
  (: regex-compile (-> Str (Nullable Regex)) #:c-name "pfregex_compile")
  (: regex-match?  (-> Regex Str Bool)       #:c-name "pfregex_is_match")
  (: regex-close   (-> Regex Void)           #:c-name "pfregex_free"
                                             #:consumes))

Each declaration is the ordinary (: name ฯ„) form; the declared type generates the marshaling, the checker types call sites with it, and every crossing is checked at run time with blame naming the import. Marshallable types: Int (plus the width spellings I8..U64), Bool, Str, Void results, declared handle types, and (Nullable ฯ„) results (C NULL becomes #f). A foreign name is an ordinary binding โ€” it provides, eta-passes, and procedure? answers #t. Library paths containing / resolve relative to the declaring module's file. The browser playground compiles FFI programs but refuses to run them at load (error: foreign library ... is not available in the browser).

Runnable examples live in examples/ โ€” ffi/hello-libc.puf (the system C library, no build step) and z3/ (the Z3 SMT solver bound as a Puffin API, with a solve-and-prove-unique Sudoku showcase); tools/test-examples.sh holds them to their goldens.

Pattern matching

(match e
  [42 ...]                     ;; literals: fixnum, boolean, string
  ['sym ...]                   ;; a symbol
  [x ...]                      ;; variable: binds
  [_ ...]                      ;; wildcard
  [(cons hd tl) ...]           ;; pairs
  [(list a b c) ...]           ;; exactly three elements
  [(vector x y) ...]           ;; vectors by length
  [(Some x) ...]               ;; ADT constructors (docs/TYPES.md)
  [(? fixnum? n) ...]          ;; predicate guard around a subpattern
  [`(add ,a ,b) ...]           ;; quasiquote: literal structure + unquote holes
  [`(lambda (,xs ...) ,body) ...]  ;; ellipsis: xs collects a sublist
  [`(program (define (,ns ,ps ...) ,bs) ...) ...]  ;; nested ellipsis: per-element lists
  [p #:when guard ...]         ;; clause guards
  )

Ellipsis in quasiquote patterns is Racket-style: the repeated pattern matches each element of a middle segment (fixed-shape patterns may follow it), and each variable under the ... collects a list of its per-element matches โ€” the idiom the Puffin compiler itself is written in.

No clause matching raises error: match-failure. Quasiquote patterns make ASTs pleasant to work with:

(define (eval-expr e)
  (match e
    [`(add ,a ,b) (+ (eval-expr a) (eval-expr b))]
    [`(mul ,a ,b) (* (eval-expr a) (eval-expr b))]
    [(? fixnum? n) n]))

Running

puffincc is the compiler. Build it once with bin/bootstrap โ€” no Racket required, just a C toolchain โ€” then:

build/puffincc prog.puf -o prog             # compile + assemble + link
build/puffincc -O 2 prog.puf -o prog        # optimization level (default -O1)
build/puffincc -t x86-64 prog.puf -o prog   # cross-target (runs under Rosetta)
build/puffincc -t bytecode prog.puf -o prog.pbc   # compile to bytecode
bin/puffin-vm prog.pbc                      # run bytecode on the native VM

With -o file.s it writes assembly instead of linking; with no -o it prints assembly to stdout. Module programs work everywhere a single file does: point the compiler at the entry file and the require DAG is resolved from disk.

The Racket driver bin/puffin fronts the optional consistency oracle in src/ and adds a REPL and an interpreter:

bin/puffin                      # REPL (,help ,env ,quit)
bin/puffin prog.puf             # compile natively + run
bin/puffin -i prog.puf          # interpret
bin/puffin -c prog.puf -o prog  # compile only

The browser playground (web/) runs the same language because it runs the same compiler: puffincc itself, compiled to bytecode, executing on a WebAssembly build of the bytecode VM. The playground's "+ file" tab turns the editor into a module DAG.

Sharp edges