Possible logic error in hereditary substitution

[jonsterling]

@david-christiansen When you get a chance, can you look at this line? https://github.com/jonsterling/racket-grit/blob/master/logical-framework.rkt#L216

I think it might be wrong; it seems like we should be calling (inst-body body 0 new-spine) rather than (inst-body body i new-spine). This is because, I think, the scope that we got from instantiating the variable should be "closed" (in the sense of having no externally visible bound variables).

Does what I'm saying make sense, or did I get completely confused?

[jonsterling]

I'm also very worried about the secondary instantiation that is triggered here; I think that it cannot possibly be correct, since a basic invariant that must be maintained in I'm Not A Number-style syntax is that the list of new-exprs should be closed; but that invariant is not preserved here.

Thinking back, I had a bug like this in my SML ABT library way back when, and what made me think of it today is that I created the exact same bug in a new/faster implementation of ABTs yesterday.

I'm concerned that there is no clear correct implementation of this kind of hereditary substitution inside of instantiate. I think we may need to re-think how this all works...

[david-christiansen]

After hurting my brain on this for a while, I realized that we are being too clever. As long as we live in the magic Racket monad that can do anything, we might as well use pointer equality to represent binders. Here's a prototype. What do you think?

#lang racket

(module+ test
  (require rackunit))

(module ast racket
  (provide
   (contract-out
    (α-equiv? (->* (any/c any/c) (dict?) boolean?))
    (struct var ((name symbol?)))
    (struct SORT ())
    (struct arity ((domain (listof (cons/c var? arity?)))
                   (codomain (or/c plug? SORT?))))
    (struct bind ((vars (listof var?))
                  (scope plug?)))
    (struct plug ((var var?)
                  (spine (listof arity?))))))

  ;; This struct must not be transparent, because we want to use
  ;; pointer equality (eq?) to compare it in all contexts.
  (struct var (name)
    #:extra-constructor-name make-var
    #:methods gen:custom-write
    [(define (write-proc b port mode)
       (fprintf port "#<var:~s>" (var-name b)))])

  (struct SORT ()
    #:methods gen:custom-write
    [(define (write-proc s port mode)
       (fprintf port "SORT"))])

  ;; domain is an alist mapping bindings to expressions
  (struct arity (domain codomain)
    #:methods gen:custom-write
    [(define (write-proc a port mode)
       (fprintf port "(arity ~s ~s)"
                (for/list ([dom (arity-domain a)])
                  (list (car dom) (cdr dom)))
                (arity-codomain a)))])

  ;; vars is a list of variables. Invariant: they must be generated
  ;; fresh!
  (struct bind (vars scope)
    #:methods gen:custom-write
    [(define (write-proc b port mode)
       (if (pair? (bind-vars b))
           (fprintf port "(bind ~s ~s)" (bind-vars b) (bind-scope b))
           (write (bind-scope b) port)))])

  ;; var must be a ref, spine a list of expressions
  (struct plug (var spine)
    #:methods gen:custom-write
    [(define (write-proc p port mode)
       (if (pair? (plug-spine p))
           (begin (fprintf port "(plug ~s" (plug-var p))
                  (for ([arg (plug-spine p)])
                    (write " " port)
                    (write arg port))
                  (write ")" port))
           (write (plug-var p) port)))])

  (define (new-var [x (gensym)])
    (make-var x))

  ;; The strategy for testing alpha-equivalence is to freshen all
  ;; bindings on the way down.
  (define (α-equiv? e1 e2 [σ '()])
    (match* (e1 e2)
      [((? var?) (? var?))
       (define e3 (dict-ref σ e1 #f))
       (define e4 (dict-ref σ e2 #f))
       (or
        ;; Both bound
        (and e3 e4 (eq? e3 e4))
        ;; Both free
        (and (not e3) (not e4) (eq? e1 e2)))]
      [((SORT) (SORT)) #t]
      [((arity bs1 body1) (arity bs2 body2))
       (let/ec k
         (define σ-new
           (let loop ([args1 bs1] [args2 bs2] [σ-args σ])
             (match* (args1 args2)
               [('() '()) σ-args]
               [((cons (cons v1 t1) a1)
                 (cons (cons v2 t2) a2))
                (if (α-equiv? t1 t2 σ-args)
                    (let ([x (var 'x)])
                       (loop a1 a2 (list* (cons v1 x)
                                          (cons v2 x)
                                          σ-args)))
                    (k #f))]
               [(_ _) (k #f)])))
         (α-equiv? body1 body2 σ-new))]
      [((bind xs body1) (bind ys body2))
       (let/ec k
         (define σ-new
           (let loop ([vs1 xs]
                      [vs2 ys])
             (match* (vs1 vs2)
               [('() '()) σ]
               [((cons v1 more1)
                 (cons v2 more2))
                (define x (var 'x))
                (list* (cons v1 x)
                       (cons v2 x)
                       (loop more1 more2))]
               [(_ _) (k #f)])))
         (α-equiv? body1 body2 σ-new))]
      [((plug var1 spine1)
        (plug var2 spine2))
       (and (α-equiv? var1 var2 σ)
            (let loop ([xs spine1]
                       [ys spine2])
              (match* (xs ys)
                [('() '()) #t]
                [((cons e1 es1)
                  (cons e2 es2))
                 (and (α-equiv? e1 e2 σ)
                      (loop es1 es2))]
                [(_ _) #f])))]
      [(_ _) #f]))

  ;; Intersperse two lists of the same length
  (define (intersperse l1 l2)
    (match* (l1 l2)
      [('() '()) '()]
      [((cons x xs) (cons y ys))
       (cons x (cons y (intersperse xs ys)))]
      [(_ _)
       (raise-arguments-error 'intersperse
                              "Lengths of lists are not the same"
                              "first list" l1
                              "second list" l2)]))

  ;; Simultaneous hereditary substitution - σ is a dict mapping from
  ;; bindings to expressions.
  (define (subst σ e)
    (match e
      [(? var? x)
       (dict-ref σ x e)]
      [(arity dom cod)
       (arity (for/list ([b (in-list dom)])
                (cons (car b) (subst σ (cdr b))))
              (subst σ cod))]
      [(bind vars sc)
       (bind vars (subst σ sc))]
      [(plug var spine)
       (define new-spine
         (for/list ([arg spine])
           (subst σ arg)))
       (define var-val
         (dict-ref σ var #f))
       (match var-val
         [(bind vars sc)
          (apply dict-set* σ (intersperse vars new-spine))]
         (plug var new-spine))]
      [(SORT) e])))

(module lf-syntax racket
  (require (prefix-in ast: (submod ".." ast)))
  (require (for-syntax syntax/parse))
  (provide bind arity SORT plug)

  (define (as-base-classifier e)
    (match e
      [(? ast:var?)
       (as-base-classifier (ast:plug e '()))]
      [(ast:SORT)
       e]
      [(ast:plug _ _)
       e]))

  (define (as-arity e)
    (if (ast:arity? e)
        e
        (ast:arity '() (as-base-classifier e))))

  (define (as-plug e)
    (if (ast:plug? e)
        e
        (ast:plug e '())))

  (define (lf-syntax? e)
    (or (ast:var? e)
        (ast:SORT? e)
        (ast:arity? e)
        (ast:bind? e)
        (ast:plug? e)))

  (define (loose-α-equiv? e1 e2)
    (if (and (lf-syntax? e1) (lf-syntax? e2))
        (let ([x (as-arity e1)]
              [y (as-arity e2)])
          (ast:α-equiv? x y))
        (equal? e1 e2)))

  (match-equality-test loose-α-equiv?)

  (define-match-expander arity
    (lambda (stx)
      (syntax-parse stx
        [(_ ((x:id ty:expr) ...) body:expr)
         (syntax/loc stx
           (? ast:arity?
              (and (app ast:arity-domain (list (cons x ty) ...))
                   (app ast:arity-codomain body))))]))
    (lambda (stx)
      (syntax-parse stx
        [(_ ((x:id ty:expr) ...) body:expr)
         (syntax/loc stx
           (let ([x (ast:var 'x)] ...)
             (ast:arity (list (cons x (as-arity ty)) ...)
                        (as-base-classifier body))))])))

  (define-match-expander SORT
    (lambda (stx)
      (syntax-parse stx
        [s:id (syntax/loc stx (ast:SORT))]))
    (lambda (stx)
      (syntax-parse stx
        [s:id (syntax/loc stx (ast:SORT))])))

  (define (as-bind e)
    (if (ast:bind? e)
        e
        (ast:bind '() (as-base-classifier e))))

  (define-match-expander bind
    (lambda (stx)
      (syntax-parse stx
        [(_ (x:id ...) body)
         (syntax/loc stx
           (? ast:bind?
              (and (app ast:bind-vars (list x ...))
                   (app ast:bind-scope body))))]))
    (lambda (stx)
      (syntax-parse stx
        [(_ (x:id ...) body)
         (syntax/loc stx
           (let ([x (ast:var 'x)] ...)
             (ast:bind (list x ...) (as-plug body))))])))

  (define-match-expander plug
    (lambda (stx)
      (syntax-parse stx
        [(_ x)
         (syntax/loc stx
           (ast:plug x '()))]
        [(_ x arg ...)
         (syntax/loc stx
           (? ast:plug?
              (and (app ast:plug-var x)
                   (app ast:plug-spine (list arg ...)))))]))
    (lambda (stx)
      (syntax-parse stx
        [(_ x arg ...)
         (syntax/loc stx
           (ast:plug x (list (as-bind arg) ...)))]
        [(_ e)
         (syntax/loc stx
           (as-plug e))]))))

(require 'lf-syntax)

(module+ test
  (require (prefix-in ast: (submod ".." ast)))
  (define-values (b1 b2 b3)
    (values (ast:var 'x) (ast:var 'y) (ast:var 'z)))

  (define-simple-check (check-α-equiv? e1 e2)
    (ast:α-equiv? e1 e2 '()))

  (check-α-equiv? (bind (x) x) (bind (y) y))

  (check-α-equiv? (bind (x) x)
                  (let ([y (ast:var 'y)])
                    (ast:bind (list y) (ast:plug y '()))))

  (check-α-equiv?
   (arity ((z SORT)) z)
   (let ([x (ast:var 'y)])
     (ast:arity (list (cons x (ast:arity '() (ast:SORT))))
                (ast:plug x '()))))

  (check-not-false
   (match (bind (x y) x)
     [(bind (y z) y) y]
     [_ #f])
   "Check that binders are matched right")

  (check-false
   (match (bind (x y) x)
     [(bind (y z) z) z]
     [_ #f])
   "Check that binders are matched right")
  )

[jonsterling]

I feel like this is a lot simpler! Nice job.

[david-christiansen]

I've made some progress on this representation.

In this version, variables are straight-up pointers to their binding site, rather than copies of fresh names that are held at binding sites. This means that Racket's equal? is alpha equivalence.

There's also a (probably buggy) start on the type checker and signature mechanism.

#lang racket

(module+ test
  (require rackunit))

(module ast racket
  (require racket/fixnum)
  (provide
   (contract-out
    [can-bind? (-> any/c boolean?)]
    [binder-arity (-> can-bind? exact-nonnegative-integer?)]

    [lf? (-> any/c boolean?)]

    [var? (-> any/c boolean?)]
    [var (->i ([binder can-bind?]
               [index (binder) (and/c exact-nonnegative-integer?
                                      (</c (binder-arity binder)))])
              [_ var?])]
    [var-binder (-> var? can-bind?)]
    [var-index (->i ([v var?])
                    [_ (v) (and/c exact-nonnegative-integer?
                                  (</c (binder-arity (var-binder v))))])]

    (struct SORT ())

    [arity? (-> any/c boolean?)]
    [arity (->i ([Ψ telescope?]
                 [body (Ψ) (dynamic->*
                            #:mandatory-domain-contracts (build-list (length (telescope->list Ψ))
                                                                     (lambda (_) var?))
                            #:range-contracts (list (or/c plug? SORT?)))])
                [_ arity?])]
    [arity-domain (-> arity? telescope?)]
    [arity-codomain (-> arity? (or/c plug? SORT?))]

    [empty-tele (-> telescope?)]
    [empty-tele? (-> any/c boolean?)]

    [cons-tele (-> symbol? arity? (-> var? telescope?)
                   telescope?)]
    [cons-tele? (-> any/c boolean?)]
    [cons-tele-name (-> cons-tele? symbol?)]
    [cons-tele-type (-> cons-tele? arity?)]
    [cons-tele-telescope (-> cons-tele? telescope?)]

    [telescope? (-> any/c boolean?)]
    [telescope->list (-> telescope? (listof telescope?))]
    [telescope->alist (-> telescope? (listof (cons/c symbol? arity?)))]

    [bind? (-> any/c boolean?)]
    [bind (->i ([arg-names (listof symbol?)]
                [scope (arg-names) (dynamic->*
                                    #:mandatory-domain-contracts (build-list (length arg-names) (lambda (_) var?))
                                    #:range-contracts (list plug?))])
               [_ bind?])]
    [bind-vars (-> bind? (listof symbol?))]
    [bind-scope (-> bind? plug?)]

    [plug? (-> any/c boolean?)]
    [plug-var (-> plug? var?)]
    [plug-spine (-> plug? (listof bind?))]
    [plug (->* (var?) ()
               #:rest (listof bind?)
               plug?)]))

  (define (can-bind? b)
    (or (bind? b) (cons-tele? b)))

  (define (binder-arity b)
    (cond [(cons-tele? b) 1]
          [(bind? b) (length (bind-vars b))]))

  (define (var-name binder index)
    (cond [(cons-tele? binder)
           (cons-tele-name binder)]
          [(bind? binder)
           (list-ref (bind-vars binder) index)]
          [else (error 'bad-binder)]))

  ;; Variables are a pair of a pointer to their binding site and a
  ;; natural number stating which bound variable they are
  (struct var (binder index)
    #:extra-constructor-name make-var
    #:transparent
    #:methods gen:custom-write
    [(define (write-proc v port mode)
       (fprintf port "#<var:~s>" (var-name (var-binder v) (var-index v))))])

  (struct SORT ()
    #:transparent
    #:methods gen:custom-write
    [(define (write-proc s port mode)
       (fprintf port "SORT"))])

  (define (telescope->alist tele)
    (cond [(empty-tele? tele) '()]
          [(cons-tele? tele)
           (cons (cons (cons-tele-name tele) (cons-tele-type tele))
                 (telescope->alist (cons-tele-telescope tele)))]))

  (define (telescope->list x)
    (if (empty-tele? x)
        '()
        (cons x (telescope->list (cons-tele-telescope x)))))

  (define (telescope? x)
    (or (empty-tele? x) (cons-tele? x)))

  (struct empty-tele () #:transparent
    #:methods gen:custom-write
    [(define (write-proc s port mode)
       (fprintf port "#tele<~a>" (telescope->alist s)))])

  (struct cons-tele (name type [telescope-internal #:mutable])
    #:constructor-name make-cons-tele
    #:omit-define-syntaxes
    #:methods gen:custom-write
    [(define (write-proc s port mode)
       (fprintf port "#tele<~a>" (telescope->alist s)))]
    #:methods gen:equal+hash
    [(define (equal-proc cons-tele-1 cons-tele-2 rec-equal?)
       ;; Ignore the name hint
       (and (rec-equal? (cons-tele-type cons-tele-1)
                        (cons-tele-type cons-tele-2))
            (rec-equal? (cons-tele-telescope cons-tele-1)
                        (cons-tele-telescope cons-tele-2))))
     (define (hash-proc tele rec-hash)
       (fxxor (rec-hash (cons-tele-type tele))
              (rec-hash (cons-tele-telescope tele))))
     (define (hash2-proc tele rec-hash)
       (fxxor (rec-hash (cons-tele-type tele))
              (rec-hash (cons-tele-telescope tele))))])

  (define (cons-tele name type sc)
    (define Ψ (make-cons-tele name type #f))
    (define sc-val (sc (var Ψ 0)))
    (set-cons-tele-telescope-internal! Ψ sc-val)
    Ψ)

  (define (cons-tele-telescope tele)
    (cons-tele-telescope-internal tele))

  ;; domain is a telescope that binds variables also visible in the codomain
  (struct arity (domain [codomain-internal #:mutable])
    #:methods gen:custom-write
    [(define (write-proc a port mode)
       (fprintf port "(arity ~s ~s)"
                (for/list ([dom (telescope->alist (arity-domain a))])
                  (list (car dom) (cdr dom)))
                (arity-codomain a)))]
    #:methods gen:equal+hash
    [(define (equal-proc arity1 arity2 rec-equal?)
       ;; Ignore the bound names
       (and (rec-equal? (arity-domain arity1)
                        (arity-domain arity2))
            (rec-equal? (arity-codomain arity1)
                        (arity-codomain arity2))))
     (define (hash-proc ar rec-hash)
       (fxxor (rec-hash (map cdr (arity-domain ar)))
              (rec-hash (arity-codomain ar))))
     (define (hash2-proc ar rec-hash)
       (fxxor (rec-hash (map cdr (arity-domain ar)))
              (rec-hash (arity-codomain ar))))])

  (define (arity-codomain ar)
    (define sc (arity-codomain-internal ar))
    (if (procedure? sc)
        (let* ([vars (for/list ([b (telescope->list (arity-domain ar))])
                       (var b 0))]
               [sc-val (apply sc vars)])
          (set-arity-codomain-internal! ar sc-val)
          sc-val)
        sc))

  ;; vars is a list of variable names, scope is an LF term or a
  ;; function from the binder to an LF term. The first time the
  ;; function is called, the result is memoized.
  (struct bind (vars [scope-internal #:mutable])
    #:omit-define-syntaxes
    #:constructor-name make-bind
    #:methods gen:custom-write
    [(define (write-proc b port mode)
       (if (pair? (bind-vars b))
           (fprintf port "(bind ~s ~s)" (bind-vars b) (bind-scope b))
           (write (bind-scope b) port)))]
    #:methods gen:equal+hash
    [(define (equal-proc b1 b2 rec-equal?)
       (rec-equal? (bind-scope b1) (bind-scope b2)))
     (define (hash-proc b rec-hash)
       (rec-hash b))
     (define (hash2-proc b rec-hash)
       (rec-hash b))])

  (define (bind vars sc)
    (define b (make-bind vars #f))
    (define sc-val
      (apply sc (for/list ([i (in-range (length vars))])
                  (var b i))))
    (set-bind-scope-internal! b sc-val)
    b)

  (define (bind-scope b)
    (bind-scope-internal b))

  ;; var must be a ref, spine a list of expressions
  (struct plug (var spine)
    #:transparent
    #:omit-define-syntaxes
    #:constructor-name make-plug
    #:methods gen:custom-write
    [(define (write-proc p port mode)
       (if (pair? (plug-spine p))
           (begin (fprintf port "(plug ~s" (plug-var p))
                  (for ([arg (plug-spine p)])
                    (display " " port)
                    (display arg port))
                  (display ")" port))
           (write (plug-var p) port)))])

  (define (plug x . σ)
    (make-plug x σ))

  (define (intersperse l1 l2)
    (match* (l1 l2)
      [('() '()) '()]
      [((cons x xs) (cons y ys))
       (cons x (cons y (intersperse xs ys)))]
      [(_ _)
       (raise-arguments-error 'intersperse
                              "Lengths of lists are not the same"
                              "first list" l1
                              "second list" l2)]))

  (define (lf? e)
    (or (SORT? e) (arity? e) (plug? e) (var? e) (bind? e))))

(module substitution racket
  (require (submod ".." ast))
  (provide
   (contract-out
    [subst (-> lf? (listof lf?) telescope?
               lf?)]
    [rename-to-telescope (-> lf? (listof var?) telescope?
                             lf?)]))

  (define (rename-to-telescope expr xs Ψ)
    (define ρ
      (for/hash ([x xs]
                 [b (telescope->list Ψ)])
        (values x (var b 0))))
    (do-subst ρ expr))

  (define (subst expr σ Ψ)
    (define ρ
      (for/hash ([b (telescope->list Ψ)]
                 [val σ])
        (values (var b 0) val)))

    (do-subst ρ expr))

  (define (do-subst ρ e)
    (match e
      [(? var? x)
       (define val (hash-ref ρ x #f))
       (if val val x)]
      [(? arity?
          (app arity-domain dom)
          (app arity-codomain cod))
       (arity (do-subst ρ dom)
              (do-subst ρ cod))]
      [(? bind?
          b
          (app bind-vars vars)
          (app bind-scope sc))
       (bind vars
             (lambda xs
               ;; Extend the environment with a renaming from the
               ;; old bound vars to the new
               (define ρ*
                 (let loop ([old-ρ ρ]
                            [new-vars xs]
                            [i 0])
                   (if (pair? new-vars)
                       (loop (hash-set old-ρ (var b i) (car new-vars))
                             (cdr new-vars)
                             (add1 i))
                       old-ρ)))
               (do-subst ρ* sc)))]
      [(? plug?
          (app plug-var var)
          (app plug-spine spine))
       (define new-spine
         (for/list ([arg spine])
           (do-subst ρ arg)))
       (define var-val
         (hash-ref ρ var #f))
       (match var-val
         [(? bind? b)
          (define var-count (length (bind-vars b)))
          (do-subst
           (let loop ([old-ρ ρ]
                      [i 0]
                      [sp new-spine])
             (if (pair? sp)
                 (loop (hash-set old-ρ (var b i) (car sp))
                       (add1 i)
                       (cdr sp))
                 old-ρ))
           (bind-scope b))]
         [_ (apply plug var new-spine)])]
      [(SORT) e])))

(module lf-syntax racket
  (require (prefix-in ast: (submod ".." ast)))
  (require (for-syntax syntax/parse racket/list))
  (provide bind arity SORT plug as-arity)

  (struct exn:fail:lf-syntax exn:fail (val)
    #:extra-constructor-name make-exn:fail:lf-syntax)

  (define (raise-bad-lf-syntax v)
    (raise (make-exn:fail:lf-syntax (format "Bad LF syntax: ~a" v)
                                    (current-continuation-marks)
                                    v)))

  (define (as-base-classifier e)
    (match e
      [(? ast:var?)
       (as-base-classifier (ast:plug e))]
      [(ast:SORT)
       e]
      [(? ast:plug?)
       e]
      [v (raise-bad-lf-syntax v)]))

  (define (as-arity e)
    (if (ast:arity? e)
        e
        (ast:arity (ast:empty-tele)
                   (lambda () (as-base-classifier e)))))

  (define (as-plug e)
    (if (ast:plug? e)
        e
        (ast:plug e)))

  (define (lf-syntax? e)
    (or (ast:var? e)
        (ast:SORT? e)
        (ast:arity? e)
        (ast:bind? e)
        (ast:plug? e)))

  (define (loose-equal? e1 e2)
    (if (and (lf-syntax? e1) (lf-syntax? e2))
        (let ([x (as-arity e1)]
              [y (as-arity e2)])
          (equal? x y))
        (equal? e1 e2)))

  (match-equality-test loose-equal?)

  (define (open-arity ar)
    (define Γ (ast:arity-domain ar))
    (define vars (for/list ([x/t (ast:telescope->alist Γ)]
                            [i (in-naturals)])
                   (ast:var x/t i)))
    (define types (for/list ([x/t (ast:arity-domain ar)])
                   (cdr x/t)))
    (define scope (ast:arity-codomain ar))
    (values vars types scope))

  (define (open-cons-tele t)
    (values
     (ast:var t 0)
     (ast:cons-tele-type t)
     (ast:cons-tele-telescope t)))

  (define-match-expander telescope
    (λ (stx)
      (syntax-parse stx
        [(_) (syntax/loc stx (? ast:empty-tele?))]
        [(_ (x0:id ty0) (x:id ty) ...)
         (syntax/loc stx
           (? ast:cons-tele?
              (and (app open-cons-tele
                        x0
                        ty0
                        (telescope (x:id ty) ...)))))]))
    (λ (stx)
     (syntax-parse stx
       [(_) (syntax/loc stx
              (ast:empty-tele))]
       [(_ (x0:id ty0) (x:id ty) ...)
        (syntax/loc stx
          (ast:cons-tele 'x0 (as-arity ty0) (λ (x0) (telescope (x ty) ...))))])))

  (define-match-expander arity
    (lambda (stx)
      (syntax-parse stx
        [(_ ((x:id ty:expr) ...) body:expr)
         (syntax/loc stx
           (? ast:arity?
              (app open-arity
                   (list x ...)
                   (list ty ...)
                   body)))]))
    (lambda (stx)
      (syntax-parse stx
        [(_ ((x:id ty:expr) ...) body:expr)
         (syntax/loc stx
           (ast:arity (telescope (x ty) ...)
                      (lambda (x ...)
                        (as-base-classifier body))))])))

  (define-match-expander SORT
    (lambda (stx)
      (syntax-parse stx
        [s:id (syntax/loc stx (ast:SORT))]))
    (lambda (stx)
      (syntax-parse stx
        [s:id (syntax/loc stx (ast:SORT))])))

  (define (as-bind e)
    (if (ast:bind? e)
        e
        (ast:bind '() (lambda () (as-base-classifier e)))))

  (define (open-bind b)
    (define vars (for/list ([x (ast:bind-vars b)]
                            [i (in-naturals)])
                   (ast:var b i)))
    (define sc (ast:bind-scope b))
    (values vars sc))

  (define-match-expander bind
    (lambda (stx)
      (syntax-parse stx
        [(_ (x:id ...) body)
         (syntax/loc stx
           (? ast:bind?
              (app open-bind
                   (list x ...)
                   body)))]))
    (lambda (stx)
      (syntax-parse stx
        [(_ (x:id ...) body)
         (syntax/loc stx
           (ast:bind (list 'x ...)
                     (λ (x ...)
                       (as-plug body))))])))

  (define-match-expander plug
    (lambda (stx)
      (syntax-parse stx
        [(_ x)
         (syntax/loc stx
           (ast:plug x))]
        [(_ x arg ...)
         (syntax/loc stx
           (? ast:plug?
              (and (app ast:plug-var x)
                   (app ast:plug-spine (list arg ...)))))]))
    (lambda (stx)
      (syntax-parse stx
        [(_ x arg ...)
         (syntax/loc stx
           (ast:plug x (as-bind arg) ...))]
        [(_ e)
         (syntax/loc stx
           (as-plug e))]))))

(module check racket
  (require (submod ".." ast) (submod ".." substitution))

  (provide
   (contract-out
    [typing-context? (-> any/c boolean?)]
    [empty-ctx typing-context?]
    [extend-context (-> typing-context? telescope? typing-context?)]
    [context->list (-> typing-context? (listof telescope?))]
    [well-formed-classifier (-> typing-context? lf? void?)]))

  (struct typing-context (telescopes)
    #:methods gen:custom-write
    [(define (write-proc Γ port mode)
       (fprintf port "~a" (apply append
                                 (map telescope->alist
                                      (typing-context-telescopes Γ)))))])

  (define empty-ctx (typing-context '()))

  (define/contract (extend-context Γ Ψ)
    (-> typing-context? telescope? typing-context?)
    (typing-context (cons Ψ (typing-context-telescopes Γ))))

  (define (context->list Γ)
    (apply append (map telescope->list (typing-context-telescopes Γ))))

  (define (lookup x Γ)
    (let outer ([teles (typing-context-telescopes Γ)])
      (if (pair? teles)
          (let inner ([Ψ (car teles)])
            (if (cons-tele? Ψ)
                (if (eq? (var-binder x) Ψ)
                    (cons-tele-type Ψ)
                    (inner (cons-tele-telescope Ψ)))
                (outer (cdr teles))))
          (raise-bad-var x))))

  (define (raise-type-mismatch expected found)
    (error (format "Expected: ~a but found ~a" expected found)))

  (define (raise-bad-var x)
    (error (format "Unknown variable: ~a" x)))

  (define (raise-not-arity t)
    (error (format "Not an arity: ~a" t)))

  (define (raise-not-bind N)
    (error (format "Not a binder: ~a" N)))

  (define (raise-spine-underflow Ψ)
    (error (format "Not enough variables in substitution. Leftovers: ~a" Ψ)))

  (define (raise-spine-overflow σ)
    (error (format "Too many variables in substitution. Leftovers: ~a" σ)))

  (define (is-arity t)
    (if (arity? t)
        (values (arity-domain t) (arity-codomain t))
        (raise-not-arity t)))

  ;; Check the judgment Γ ⊢ Ψ ctx. Returns (void) on success, throws
  ;; an exception on failure.
  (define (telescope-ok Γ Ψ)
    (cond
      [(empty-tele? Ψ) (void)]
      [(cons-tele? Ψ)
       (begin (telescope-ok Γ (cons-tele-telescope Ψ))
              (well-formed-classifier (extend-context Γ Ψ) (cons-tele-type Ψ)))]))

  ;; Check the judgment Γ ⊢ V ⇐ ok, (void) on success or exception on failure
  (define (well-formed-classifier Γ V)
    (define Ψ (arity-domain V))
    (define cod (arity-codomain V))
    (begin (telescope-ok Γ Ψ)
           (if (or (SORT? cod)
                   (SORT? (synth (extend-context Γ Ψ) cod)))
               (void)
               (raise-not-arity V))))

  ;; The judgment Γ ⊢ σ ⇐ Ψ. (void) on success, exn on failure.
  (define (check-spine Γ σ Ψ)
    (match σ
      ['()
       (if (empty-tele? Ψ)
           (void)
           (raise-spine-underflow Ψ))]
      [(cons M σ-rest)
       (if (cons-tele? Ψ)
           (let ([x (var Ψ 0)]
                 [V (cons-tele-type Ψ)])
             (check-type Γ M (subst V σ-rest Ψ)))
           (raise-spine-overflow σ))]))

  ;; The judgment Γ ⊢ N ⇐ V
  (define (check-type Γ N V)
    (if (bind? N)
        (if (arity? V)
            (let* ([Ψ (arity-domain V)]
                   [ty (synth (extend-context Γ Ψ)
                              (rename-to-telescope (for/list ([i (in-range (length (bind-vars N)))])
                                                     (var N i))
                                                   (bind-scope N)
                                                   Ψ))])
              (if (equal? ty (arity-codomain V))
                  (void)
                  (raise-type-mismatch (arity-codomain V) ty)))
            (raise-not-arity V))
        (raise-not-bind N)))

  ;; The judgment Γ ⊢ R ⇒ v (where v is output-moded).
  (define (synth Γ R)
    (define-values (Ψ v) (is-arity (lookup (plug-var R) Γ)))
    (check-spine Γ (plug-spine R) Ψ)
    (subst v (plug-spine R) Ψ)))

(module signatures racket
  (require
   (submod ".." ast)
   (prefix-in syn: (submod ".." lf-syntax))
   (submod ".." check)
   (for-syntax syntax/parse))

  (provide extend-signature define-sig)

  ;; We re-use typing contexts as signatures to keep things easy.

  (define-syntax (extend-signature stx)
    (syntax-parse stx
      [(_ Γ ())
       (syntax/loc stx
         Γ)]
      [(_ Γ ([x0:id ty0:expr]
             [x:id ty:expr]
             ...))
       (syntax/loc stx
         (let ([t (syn:as-arity ty0)])
           (well-formed-classifier Γ t)
           (define Ψ (cons-tele 'x0 t (lambda (x0) (empty-tele))))
           (define x0 (var Ψ 0))
           (extend-signature (extend-context Γ Ψ)
                             ([x ty] ...))))]))

  (define-syntax (define-sig stx)
    (syntax-parse stx
      [(_ Σ:id #:extend Γ ([x:id ([y:id yt] ...) t] ...))
       (with-syntax ([(z ...) (reverse (syntax->list #'(x ...)))])
         #'(begin
             (define Σ
               (extend-signature Γ ([x (syn:arity ([y yt] ...) t)] ...)))
             (match-define (list-rest z ... xs)
               (map (lambda (Ψ) (var Ψ 0))
                    (context->list Σ)))))]
      [(_ Σ:id ([x:id ([y:id yt] ...) t] ...))
       #'(define-sig Σ #:extend empty-ctx ([x ([y yt] ...) t] ...))]))

  )

(module+ test
  (require (prefix-in ast: (submod ".." ast)))
  (require (submod ".." lf-syntax))
  (require (submod ".." check))
  (require (submod ".." signatures))

  (define-simple-check (check-void? x)
    (void? x))

  (check-equal? (bind (x) x) (bind (y) y))

  (check-equal? (bind (x) x)
                (ast:bind '(y) (lambda (y) (ast:plug y))))

  (check-equal?
   (arity ((z SORT)) z)
   (ast:arity (ast:cons-tele 'x (ast:arity (ast:empty-tele) (lambda () (ast:SORT))) (lambda (_) (ast:empty-tele)))
              (lambda (x)
                (ast:plug x))))

  (check-not-false
   (match (bind (x y) x)
     [(bind (y z) y) y]
     [_ #f])
   "Check that binders are matched right")

  (check-false
   (match (bind (x y) x)
     [(bind (y z) z) z]
     [_ #f])
   "Check that binders are matched right")

  (check-void?
   (well-formed-classifier empty-ctx (arity () SORT)))

  (check-void?
   (well-formed-classifier empty-ctx (arity ([x SORT]) SORT)))

  (check-void?
   (well-formed-classifier empty-ctx (arity ([x SORT]) x)))

  (define-sig sig1
    ([Nat () SORT]
     [zero () Nat]
     [succ ([n (arity () Nat)]) Nat]))

  (define-sig sig2 #:extend sig1
    ([Expr () SORT]
     [lam ([body (arity ([x Expr]) Expr)])
          Expr]
     [ap ([rator Expr]
          [rand Expr])
         Expr]
     [nat ([n Nat]) Expr]
     [Type () SORT]
     [ℕ () Type]
     [→ ([dom Type] [rng Type]) Type]))

  )

[jonsterling]

@david-christiansen hey, this looks really cool, super nice! It looks way better than what we have.

Sorry I haven't been very responsive lately, I got swamped.

[david-christiansen]

Business happens.

I'm currently redoing all the LF stuff based on that model. The major interface changes along the way are:

1. Instead of having a signature define a bunch of helper macros, signatures are now objects with both compile-time and run-time bindings. The compile-time structure is used for syntax, and the run-time structure is used for things like type checking and variable references.

2. Like Redex, there is a single macro called term for getting LF syntax. term allows escaping back to Racket syntax, and it is parameterized with the signature to be used. This allows things like having two signatures that have overlapping names. I plan on adding a #:lint option to term as well to get it to typecheck the resulting LF term.

Hopefully this will make the whole thing easier to use, at the cost of a little complexity in the term macro.

[jonsterling]

@david-christiansen All this sounds very interesting, and much better-designed. nice!