Skip to content

Refactor typecheck.rkt #71

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
May 10, 2018
Merged

Refactor typecheck.rkt #71

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
37f6245
Refactor class/instance specific logic out of typecheck.rkt
iitalics May 9, 2018
22b4332
Hide implementation details of type contexts
iitalics May 10, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions hackett-lib/hackett/private/base.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,12 @@

(for-syntax hackett/private/infix
hackett/private/typecheck
hackett/private/typeclass
hackett/private/util/list
hackett/private/util/stx))

(provide (for-syntax (all-from-out hackett/private/typecheck)
(all-from-out hackett/private/typeclass)
τs⇔/λ! τ⇔/λ! τ⇔! τ⇐/λ! τ⇐! τ⇒/λ! τ⇒! τ⇒app! τs⇒!)
(rename-out [#%top @%top])
@%module-begin @%datum @%app
Expand Down Expand Up @@ -239,9 +241,7 @@
#:literal-sets [type-literals]
[(#%type:wobbly-var x^)
#:with [x1^ x2^] (generate-temporaries #'[x^ x^])
(modify-type-context
#{snoc % (ctx:solution #'x^ (template
(?->* (#%type:wobbly-var x1^) (#%type:wobbly-var x2^))))})
(type-inst-l! #'x^ (template (?->* (#%type:wobbly-var x1^) (#%type:wobbly-var x2^))))
(values (quasisyntax/loc src
(lazy- (#%app- (force- #,e_fn) #,(τ⇐! e_arg #'(#%type:wobbly-var x1^)))))
#'(#%type:wobbly-var x2^))]
Expand Down
1 change: 1 addition & 0 deletions hackett-lib/hackett/private/class.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
syntax/parse/define

(for-syntax hackett/private/infix
hackett/private/typeclass
hackett/private/util/stx)
(except-in hackett/private/base @%app)
(only-in (unmangle-types-in #:no-introduce (only-types-in hackett/private/kernel))
Expand Down
291 changes: 13 additions & 278 deletions hackett-lib/hackett/private/typecheck.rkt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,30 +1,26 @@
#lang curly-fn racket/base

; This module contains the core implementation of the Hackett typechecker, as well as the core type
; representations. The Hackett typechecker operates using a mutable typechecker context implemented
; as a Racket parameter, which contains information about solutions for existing solver variables.
; This module contains the core implementation of the Hackett typechecker. The Hackett typechecker
; operates using a mutable typechecker context implemented as a Racket parameter, which contains
; information about solutions for existing solver variables.
;
; The core typechecker implements typing subsumption rules and the constraint solver for resolving
; typeclass instances. Other functionality is deferred to the implementation site of Hackett forms.
; The functions that perform the actual process of type inference (via recursive expansion) are
; defined in hackett/private/base, and they provide the primary interface to the various typechecker
; functions in this module.
; The core typechecker implements typing subsumption rules and variable instantiation. Other
; functionality is deferred to the implementation site of Hackett forms. The functions that perform
; the actual process of type inference (via recursive expansion) are defined in hackett/private/base,
; and they provide the primary interface to the various typechecker functions in this module.

(require (for-template racket/base
syntax/id-table
hackett/private/type-language)
(for-syntax racket/base
syntax/transformer)
data/gvector

racket/contract
racket/format
racket/function
racket/list
racket/match
racket/string
racket/syntax
racket/stxparam-exptime
syntax/id-table
syntax/parse
syntax/parse/class/local-value
syntax/parse/define
Expand All @@ -35,29 +31,13 @@
hackett/private/util/list
hackett/private/util/stx)

(provide (contract-out [struct ctx:solution ([x^ identifier?] [t type?])]
[struct class:info ([vars (listof identifier?)]
[method-table immutable-free-id-table?]
[default-methods immutable-free-id-table?]
[superclasses (listof constr?)]
[deriving-transformer (or/c (-> syntax? syntax?) #f)])]
[struct class:instance ([class class:info?]
[vars (listof identifier?)]
[subgoals (listof constr?)]
[ts (listof (and/c type? type-mono?))]
[dict-expr syntax?])])
type? type=? constr? type-mono? type-vars^ type->string
(provide type? type=? constr? type-mono? type-vars^ type->string
generalize inst insts type<:/full! type<:/elaborate! type<:! type-inst-l! type-inst-r!
ctx-elem? ctx? ctx-elem=? ctx-member? ctx-remove
ctx-find-solution current-ctx-solution apply-subst apply-current-subst
apply-subst apply-current-subst
current-type-context modify-type-context
register-global-class-instance! constr->instances lookup-instance!
reduce-context type-reduce-context
attach-type attach-expected get-type get-expected apply-current-subst-in-tooltips
make-typed-var-transformer

(for-template (all-from-out hackett/private/type-language)
local-class-instances @%superclasses-key))
(for-template (all-from-out hackett/private/type-language)))

;; ---------------------------------------------------------------------------------------------------
;; type operations
Expand Down Expand Up @@ -173,11 +153,9 @@

(define/contract (ctx-find-solution ctx x^)
(-> ctx? identifier? (or/c type? #f))
(and~> (findf #{and (ctx:solution? %) (free-identifier=? x^ (ctx:solution-x^ %))} ctx)
(and~> (findf #{and (ctx:solution? %)
(free-identifier=? x^ (ctx:solution-x^ %))} ctx)
ctx:solution-t))
(define/contract (current-ctx-solution x^)
(-> identifier? (or/c type? #f))
(ctx-find-solution (current-type-context) x^))

(define/contract (apply-subst ctx t)
(-> ctx? type? type?)
Expand Down Expand Up @@ -226,48 +204,6 @@
(-> (-> ctx? ctx?) void?)
(current-type-context (f (current-type-context))))

;; ---------------------------------------------------------------------------------------------------
;; instance contexts

(struct class:info (vars method-table default-methods superclasses deriving-transformer) #:transparent
#:property prop:procedure
(λ (info stx)
((make-variable-like-transformer
#`(#%type:con #,(syntax-parse stx
[id:id #'id]
[(id:id . _) #'id])))
stx)))
(struct class:instance (class vars subgoals ts dict-expr) #:transparent)

(define-syntax-class (class-id #:require-deriving-transformer? [require-deriving-transformer? #f])
#:description "class id"
#:attributes [local-value]
[pattern
{~var || (local-value class:info? #:failure-message "identifier was not bound to a class")}
#:fail-unless (or (not require-deriving-transformer?)
(class:info-deriving-transformer (attribute local-value)))
"class is not derivable"])

(define global-class-instances (make-gvector))
(define/contract (register-global-class-instance! instance)
(-> class:instance? void?)
(gvector-add! global-class-instances instance))

(module local-instances-stxparam racket/base
(require (for-syntax racket/base) racket/stxparam)
(provide local-class-instances)
(define-syntax-parameter local-class-instances '()))
(require (for-template 'local-instances-stxparam))

(define/contract (current-class-instances)
(-> (listof class:instance?))
(append (syntax-parameter-value #'local-class-instances)
(gvector->list global-class-instances)))

(define (current-instances-of-class class)
(-> class:info? (listof class:instance?))
(filter #{eq? class (class:instance-class %)} (current-class-instances)))

;; ---------------------------------------------------------------------------------------------------
;; subsumption, instantiation, and elaboration

Expand Down Expand Up @@ -394,207 +330,6 @@
[_ (error 'type-inst-r! (format "internal error: failed to instantiate ~a to a supertype of ~a"
(type->string #`(#%type:wobbly-var #,x^)) (type->string t)))]))

; Performs one-way unification to see if a type matches another one. Unlike general unification,
; one-way matching is asymmetric: it only solves wobbly variables in the first type argument, never in
; the second. If unifying the two types would require unification in the second type, matching fails.
; Also, matching is more restricted than unification: it never instantiates quantifiers in other type,
; nor does it permit qualified types. If a quantifier or qualified type is encountered, matching
; fails.
(define/contract (types-match?! a b)
(-> type? type? boolean?)
(syntax-parse (list (apply-current-subst a) (apply-current-subst b))
#:context 'match-types!
#:literal-sets [type-literals]
[[(#%type:rigid-var x^) (#%type:rigid-var y^)]
#:when (free-identifier=? #'x^ #'y^)
#t]
[[(#%type:wobbly-var x^) t]
#:when (type-mono? #'t)
(modify-type-context #{snoc % (ctx:solution #'x^ #'t)})
#t]
[[(#%type:con a) (#%type:con b)]
#:when (free-identifier=? #'a #'b)
#t]
[[(#%type:app a b) (#%type:app c d)]
(and (types-match?! #'a #'c) (types-match?! #'b #'d))]
[[_ _]
#f]))

;; ---------------------------------------------------------------------------------------------------

(module superclasses-key racket/base
(require (for-syntax racket/base))
(provide @%superclasses-key)
(define-syntax (@%superclasses-key stx)
(raise-syntax-error #f "cannot be used as an expression" stx)))
(require (for-template 'superclasses-key))

(define/contract constr->class:info+ts
(-> constr? (values class:info? (listof type?)))
(syntax-parser
#:context 'constr->class:info
#:literal-sets [type-literals]
[(~#%type:app* (#%type:con class-id:class-id) ts ...)
(values (attribute class-id.local-value) (attribute ts))]))

; Given a constraint, calculate the instances it brings in scope, including instances that can be
; derived via superclasses. For example, the constraint (Monad m) brings in three instances, one for
; Monad and two for Functor and Applicative.
(define/contract (constr->instances constr dict-expr)
(-> constr? syntax? (listof class:instance?))
(let-values ([(class-info ts) (constr->class:info+ts constr)])
(let* ([ts* (map apply-current-subst ts)]
[instance (class:instance class-info '() '() ts* dict-expr)]
; instantiate the superclass constraints, so for (Monad Unit), we get (Applicative Unit)
; instead of (Applicative m)
[insts-dict (map cons (class:info-vars class-info) ts*)]
[super-constrs (map #{insts % insts-dict} (class:info-superclasses class-info))]
[superclass-dict-expr #`(free-id-table-ref #,dict-expr #'@%superclasses-key)]
[super-instances (for/list ([(super-constr i) (in-indexed (in-list super-constrs))])
(constr->instances
super-constr
#`(vector-ref #,superclass-dict-expr '#,i)))])
(cons instance (append* super-instances)))))

; Attempts to unify a type with an instance head with a type for the purposes of picking a typeclass.
; If the match succeeds, it returns a list of instantiated subgoals for the instance, otherwise it
; returns #f.
(define/contract (unify-instance-head ts vars subgoals head)
(-> (listof type?) (listof identifier?) (listof constr?) (listof (and/c type? type-mono?))
(or/c (listof constr?) #f))
(let* ([vars^ (generate-temporaries vars)]
[var-subst (map #{cons %1 #`(#%type:wobbly-var #,%2)} vars vars^)]
[head-inst (map #{insts % var-subst} head)]
[subgoals-inst (map #{insts % var-subst} subgoals)])
(and (andmap types-match?! head-inst ts)
subgoals-inst)))

(define/contract (lookup-instance!
constr
#:src src
#:failure-thunk [failure-thunk
(λ ()
(raise-syntax-error
'typechecker
(~a "could not deduce "
(type->string (apply-current-subst constr)))
src))])
(->* [constr? #:src syntax?]
[#:failure-thunk (-> any)]
any) ; (values class:instance? (listof constr?))
(define-values [class ts] (constr->class:info+ts constr))
(define ts* (map apply-current-subst ts))
(define instance+subgoals
(for/or ([instance (in-list (current-instances-of-class class))])
(let ([old-type-context (current-type-context)])
(let ([constrs (unify-instance-head ts*
(class:instance-vars instance)
(class:instance-subgoals instance)
(class:instance-ts instance))])
(if constrs (list instance constrs)
(begin (current-type-context old-type-context) #f))))))
(if instance+subgoals
(apply values instance+subgoals)
(failure-thunk)))

;; ---------------------------------------------------------------------------------------------------
;; context reduction

; Context reduction is the process of simplifying contexts by pruning unnecessary constraints.
; Removing these constraints reduces the number of dictionaries that need to be passed, which is
; especially important in macro-enabled Hackett, since users might write macros that expand to
; constraints with redundant or otherwise unnecessary information. To avoid placing an unreasonable
; burden on macro authors to intelligently prune these contexts themselves, Hackett guarantees it will
; perform a certain amount of context reduction automatically.
;
; Implementing context reduction is a problem with a large design space, but fortunately, the various
; choices and their tradeoffs have been covered extensively in the paper “Type classes: an exploration
; of the design space”, available here:
;
; https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/multi.pdf
;
; Hackett implements context reduction based on the following rules:
;
; 1. Duplication constraint elimination. For example, the type:
;
; (forall [a] (Eq a) (Eq a) => ....)
;
; ...can be simplified to this type:
;
; (forall [a] (Eq a) => ....)
;
; 2. Superclass subsumption. Since subclass dictionaries include dictionaries for their
; superclasses, superclass constraints can be eliminated in favor of equivalent subclass ones.
; For example, the type:
;
; (forall [f] (Functor f) (Applicative f) => ....)
;
; ...can be simplified to this type:
;
; (forall [f] (Applicative f) => ....)
;
; 3. Discharging tautological constraints. A tautological constraint is a constraint that can be
; immediately resolved via an in-scope instance declaration. For example, the constraint
; (Eq Integer) always holds, so there is never any reason to include it in a context.
;
; This is complicated slightly by the fact that instances can also have contexts, so for a
; constraint to be tautological, all constraints in the chosen instance context must also be
; tautological. For example, given an instance:
;
; (instance (forall [a] (Eq a) => (Foo (Tuple a b))) ....)
;
; ...the constraint (Foo (Tuple Integer t)) is tautological regardless of t, since (Eq Integer)
; is tautological.

(define/contract (constr-tautological? constr #:extra-constrs [extra-constrs '()])
(->* [constr?] [#:extra-constrs (listof constr?)] boolean?)
(or (ormap #{type=? constr %} extra-constrs)
(match/values (lookup-instance! constr #:src #'here #:failure-thunk (λ () (values #f #f)))
[[#f _] #f]
[[_ subgoals] (andmap constr-tautological? subgoals)])))

(define/contract (superclasses-entail? constr-a constr-b)
(-> constr? constr? boolean?)
(match-let-values ([(class ts) (constr->class:info+ts constr-a)])
(let* ([inst-dict (map cons (class:info-vars class) ts)]
[supers (map #{insts % inst-dict} (class:info-superclasses class))])
(or (ormap #{types-match?! % constr-b} supers)
(ormap #{superclasses-entail? % constr-b} supers)))))

(define/contract (constrs-entail? constrs constr)
(-> (listof constr?) constr? boolean?)
(and (or (member constr constrs type=?)
(ormap #{superclasses-entail? % constr} constrs))
#t))

(define/contract (reduce-context constrs
#:extra-tautological-constrs [extra-tautological-constrs '()])
(->* [(listof constr?)] [#:extra-tautological-constrs (listof constr?)] (listof constr?))
(let loop ([constrs constrs]
[constrs* '()])
(match constrs
[(cons constr remaining-constrs)
(loop remaining-constrs
(let ([reduced-context (append remaining-constrs constrs*)])
(if (or (constr-tautological?
constr
#:extra-constrs (append reduced-context extra-tautological-constrs))
(constrs-entail? reduced-context constr))
constrs*
(cons constr constrs*))))]
[_
(reverse constrs*)])))

(define/contract type-reduce-context
(-> type? type?)
(syntax-parser
#:context 'type-reduce-context
[(~#%type:forall* [x ...] {~and t_qual (~#%type:qual* [constr ...] t)})
#:with [constr* ...] (reduce-context (attribute constr))
(quasisyntax/loc/props this-syntax
(?#%type:forall* [x ...] #,(syntax/loc/props #'t_qual
(?#%type:qual* [constr* ...] t))))]))

;; -------------------------------------------------------------------------------------------------

; To support type tooltips, we attach 'mouse-over-tooltips properties to syntax objects whenever we
Expand Down
Loading