Skip to content

Commit 27a895c

Browse files
YarinHeffesstylewarning
YarinHeffes
authored and
stylewarning
committed
add in-line documentation for functional dependencies
1 parent 1a8d33d commit 27a895c

9 files changed

Lines changed: 303 additions & 92 deletions

File tree

‎src/typechecker/context-reduction.lisp‎

Lines changed: 89 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -263,64 +263,113 @@ Returns (VALUES deferred-preds retained-preds defaultable-preds)"
263263
;;; "transitive `closure'" of the known types.
264264

265265
(defun fundep-entail (env expr-preds preds known-tyvars)
266-
(loop :with _expr-preds
267-
:= (alexandria:mappend (alexandria:curry #'by-super env) expr-preds)
268-
:with subs := nil
269-
:for pred :in preds
270-
:for new-subs := (fundep-entail% env _expr-preds pred known-tyvars)
271-
:do (setf subs (compose-substitution-lists subs new-subs))
272-
:finally (return subs)))
266+
"Produce a list of type substitutions that reduce the generality of
267+
PREDS with respect to EXPR-PREDS based on functional dependencies.
268+
269+
For example, consider the following,
270+
271+
```
272+
(define-class (C :a :b (:a -> :b)))
273+
(define-class (C :a :b => D :a :b)
274+
(m :a))
275+
276+
(declare f (D :a :b => Unit -> :a))
277+
(define (f) m)
278+
```
279+
280+
For the example above, EXPR-PREDS includes only D #T1 #T2 and PREDS
281+
includes only D #T1 #T3, and KNOWN-TYVARS includes only #T1. In the
282+
absence of functional dependencies, the second type variable in the
283+
predicate for class D is ambiguous, i.e., it cannot be determined.
284+
But, functional dependencies allow us to determine that #T2 and #T3
285+
must in fact be the same type, so FUNDEP-ENTAIL will return the
286+
substitution #T3 +-> #T2. Note that in the absence of functional
287+
dependencies, the class definition for D itself would not have passed
288+
through the typechecker, because the method M does not contain all of
289+
the type variables of the class D.
290+
"
291+
(flet ((expand (context)
292+
(alexandria:mappend (alexandria:curry #'by-super env) context)))
293+
(loop :with expr-preds := (expand expr-preds)
294+
:with preds := (expand preds)
295+
:with subs := nil
296+
:for pred :in preds
297+
:for new-subs := (fundep-entail% env expr-preds pred known-tyvars)
298+
:do (setf subs (compose-substitution-lists subs new-subs))
299+
:finally (return subs))))
273300

274301
(defun fundep-entail% (env expr-preds pred known-tyvars)
302+
"A helper function for FUNDEP-ENTAIL to be applied iteratively, binding
303+
PRED to each element in a list of predicates. Note that we do not
304+
consider superclass functional dependencies here. That is because the
305+
predicates were expanded into their superclasses prior to the
306+
applications of this function such that any relevant superclass
307+
functional dependencies will be considered directly when the
308+
respective superclass predicate is passed to this function."
275309
(let ((class (lookup-class env (ty-predicate-class pred))))
310+
276311
(unless (ty-class-fundeps class)
277312
(return-from fundep-entail% nil))
278313

279-
(let* ((unknown-indices nil)
280-
281-
(known-indices
314+
(let* ((partitioned-indices
282315
(loop :for ty :in (ty-predicate-types pred)
316+
:for tyvars := (type-variables ty)
283317
:for i :from 0
284-
:if (intersection (type-variables ty) known-tyvars :test #'eq)
285-
:collect i
318+
:if (consp (intersection tyvars known-tyvars :test #'ty=))
319+
:collect i :into known-indices
286320
:else
287-
:do (push i unknown-indices)))
321+
:collect i :into unknown-indices
322+
:finally (return (cons known-indices unknown-indices))))
323+
324+
(known-indices (car partitioned-indices))
325+
(unknown-indices (cdr partitioned-indices))
288326

289-
(unknown-indices (reverse unknown-indices))
290-
291-
(known-class-vars (util:project-indices known-indices (ty-class-class-variables class)))
327+
(class-vars (ty-class-class-variables class))
292328

329+
(known-class-vars
330+
(util:project-indices known-indices class-vars))
293331
(unknown-class-vars
294-
(util:project-indices unknown-indices (ty-class-class-variables class)))
332+
(util:project-indices unknown-indices class-vars))
295333

334+
;; We expand the list of known variables by computing the
335+
;; closure of the known class variables over the class's
336+
;; functional dependencies. See the docstring for CLOSURE
337+
;; for more details.
296338
(closure (closure known-class-vars (ty-class-fundeps class))))
297339

298-
(unless (subsetp unknown-class-vars closure)
340+
;; If the unknown class variables are not a subset of the
341+
;; closure of the known class variables, then the predicate is
342+
;; not fully determined by the known class variables and the
343+
;; class functional dependencies. In this case, we ignore any
344+
;; substitutions that can be made, since they would only be
345+
;; relevant in the case that we allow ambiguous methods to be
346+
;; determined by the functional dependencies of another type
347+
;; class.
348+
(unless (subsetp unknown-class-vars closure :test #'eq)
299349
(return-from fundep-entail% nil))
300350

301-
(loop :for expr-pred :in expr-preds
351+
(loop :for expr-pred
352+
;; We only consider expression predicates for the same
353+
;; class as that of PRED.
354+
:in (remove (ty-predicate-class pred) expr-preds :key #'ty-predicate-class
355+
:test (complement #'eq))
302356

303-
:for expr-pred-indices
304-
:= (loop :for ty :in (ty-predicate-types pred)
357+
:for expr-pred-known-indices
358+
:= (loop :for ty :in (ty-predicate-types expr-pred)
359+
:for tyvars := (type-variables ty)
305360
:for i :from 0
306-
:when (intersection (type-variables ty) known-tyvars :test #'eq)
361+
:when (consp (intersection tyvars known-tyvars :test #'ty=))
307362
:collect i)
308363

309-
:when (and (eq (ty-predicate-class pred) (ty-predicate-class expr-pred))
310-
(equalp known-indices expr-pred-indices))
311-
312-
:do
313-
(return-from
314-
fundep-entail%
315-
(loop :for ty :in (util:project-indices
316-
unknown-indices
317-
(ty-predicate-types expr-pred))
318-
319-
:for ty_ :in (util:project-indices
320-
unknown-indices
321-
(ty-predicate-types pred))
322-
323-
:when (and (tyvar-p ty) (tyvar-p ty_))
324-
:collect (make-substitution :from ty_ :to ty))))
325-
326-
nil)))
364+
:when (every #'= known-indices expr-pred-known-indices)
365+
;; Create and return substitutions for the unknown - but now
366+
;; determined by functional dependencies - types.
367+
:do (flet ((project (pred)
368+
(let ((types (ty-predicate-types pred)))
369+
(util:project-indices unknown-indices types))))
370+
(loop :for from-ty :in (project pred)
371+
:for to-ty :in (project expr-pred)
372+
:append (match from-ty to-ty) :into new-subs
373+
:finally (return-from fundep-entail% new-subs)))
374+
375+
:finally (return nil)))))

‎src/typechecker/define-class.lisp‎

Lines changed: 25 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -400,15 +400,31 @@
400400
known-method-tyvars)))
401401

402402
;; Ensure that methods are not ambiguous
403-
:unless (or (subsetp var-names
404-
(tc:closure method-tyvar-names fundeps)
405-
:test #'eq)
406-
(subsetp (mapcar (alexandria:curry #'tc:apply-ksubstitution ksubs) vars)
407-
(tc:generic-closure
408-
known-method-tyvars
409-
(tc:collect-fundeps (partial-type-env-env env) preds)
410-
:test #'tc:ty=)
411-
:test #'tc:ty=))
403+
:unless (or
404+
;; First, we check if the class variables are fully determined
405+
;; by the functional dependencies which are immediately provided
406+
;; in this class definition, such as in the following example.
407+
;; (define-class (C :a :b (:a -> :b))
408+
;; (m (Unit -> :a)) ; :B is determined by :A.
409+
;; )
410+
(subsetp var-names
411+
(tc:closure method-tyvar-names fundeps)
412+
:test #'eq)
413+
;; Otherwise, we collect functional dependencies by recursing into
414+
;; the superclass predicates and computing a generic closure on the
415+
;; types themselves using TC:TY=. This allows for examples like the
416+
;; following.
417+
;; (define-class (C :a :b (:a -> :b)))
418+
;; (define-class (D :a :b)
419+
;; (m (Unit -> :a)) ; :B is determined by the functional dependency
420+
;; ; provided in the class definition of C.
421+
;; )
422+
(subsetp (mapcar (alexandria:curry #'tc:apply-ksubstitution ksubs) vars)
423+
(tc:generic-closure
424+
known-method-tyvars
425+
(tc:collect-fundep-vars (partial-type-env-env env) preds)
426+
:test #'tc:ty=)
427+
:test #'tc:ty=))
412428
:do (tc-error "Ambiguous method"
413429
(tc-note method
414430
"the method is ambiguous"))

‎src/typechecker/define-instance.lisp‎

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -141,16 +141,33 @@
141141
((tc:lookup-function env instance-codegen-sym :no-error t)
142142
(setf env (tc:unset-function env instance-codegen-sym))))
143143

144-
(when (tc:ty-class-fundeps class)
144+
(when (consp (tc:ty-class-fundeps class))
145145
(handler-case
146146
(setf env (tc:update-instance-fundeps env pred context))
147147
(tc:fundep-ambiguity (e)
148+
;; In this case, a instance definition is ambiguous
149+
;; because a dependent type is too general.
150+
;; For example,
151+
;; (define-class (C :a :b (:a -> :b)))
152+
;; (define-instance (C :c :d))
153+
;; Here, the dependent type (:d) contains a type variable
154+
;; that is not in the determinant type (:c), but the
155+
;; underlying principle of functional dependencies requires
156+
;; that if we know the determinant type, then we should also
157+
;; know the dependent type, as we would in the following case,
158+
;; (define-instance (C :c (List :c))
148159
(tc-error "Instance fundep ambiguity"
149160
(tc-location (parser:toplevel-define-instance-head-location instance)
150161
(let ((*print-escape* nil))
151162
(with-output-to-string (s)
152163
(print-object e s))))))
153164
(tc:fundep-conflict (e)
165+
;; In thid case, an instance simply conflicts with another on
166+
;; the basis of functional dependencies.
167+
;; For example,
168+
;; (define-class (C :a :b (:a -> :b)))
169+
;; (define-instance (C T U))
170+
;; (define-instance (C T V)) ; Conflicts with the previous above.
154171
(tc-error "Instance fundep conflict"
155172
(tc-location (parser:toplevel-define-instance-head-location instance)
156173
(let ((*print-escape* nil))

‎src/typechecker/define.lisp‎

Lines changed: 33 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
;;;;
1+
;;;
22
;;;; Type inference for toplevel definitions and expressions. The
33
;;;; implementation is based on the paper "Typing Haskell in Haskell"
44
;;;; by Jones.
@@ -1978,7 +1978,14 @@ Returns (VALUES INFERRED-TYPE NODE SUBSTITUTIONS)")
19781978
(tc-note (first accessors)
19791979
"accessor is ambiguous")))
19801980

1981-
;; Generate additional substitutions from fundeps
1981+
;; Generate additional substitutions from fundeps.
1982+
;; The purpose of this block is primarily to effect
1983+
;; the inheritance of functional dependencies.
1984+
;; For example, if we have
1985+
;; (define-class (C :a :b (:a -> :b)))
1986+
;; (define-class (C :a :b => D :a :b))
1987+
;; and a list of predicates ((D #T1 #T2) (C #T1 #T3)), then
1988+
;; the following lines will ensure that #T2 and #T3 are unified.
19821989
(setf fresh-preds (tc:apply-substitution subs fresh-preds))
19831990
(setf subs (nth-value 1 (tc:solve-fundeps (tc-env-env env) fresh-preds subs)))
19841991
(setf preds (tc:apply-substitution subs preds))
@@ -2003,22 +2010,31 @@ Returns (VALUES INFERRED-TYPE NODE SUBSTITUTIONS)")
20032010
(known-variables
20042011
(tc:apply-substitution
20052012
subs
2006-
(append (remove-duplicates (tc:type-variables expr-type) :test #'eq) env-tvars)))
2013+
(append
2014+
(remove-duplicates (tc:type-variables expr-type) :test #'tc:ty=)
2015+
env-tvars)))
20072016

20082017
(preds (tc:apply-substitution subs preds))
20092018

2010-
(subs (tc:compose-substitution-lists
2011-
subs
2012-
(tc:fundep-entail (tc-env-env env) expr-preds preds known-variables)))
2019+
;; Whereas the lines above involving functional
2020+
;; dependencies relate to substitutions between the
2021+
;; predicates in a single list, the application here
2022+
;; of TC:FUNDEP-ENTAIL serves to create substitutions
2023+
;; for PREDS that reduces its generality with respect
2024+
;; to EXPR-PREDS where made possible by functional
2025+
;; dependencies.
2026+
(subs (tc:compose-substitution-lists subs
2027+
(tc:fundep-entail (tc-env-env env)
2028+
expr-preds
2029+
preds
2030+
known-variables)))
20132031

20142032
(expr-preds (tc:apply-substitution subs expr-preds))
20152033

20162034
(preds (remove-if
20172035
(lambda (p) (tc:entail (tc-env-env env) expr-preds p))
20182036
(tc:apply-substitution subs preds))))
20192037

2020-
(setf preds (tc:apply-substitution subs preds))
2021-
20222038
(setf local-tvars
20232039
(expand-local-tvars env-tvars
20242040
local-tvars
@@ -2254,6 +2270,9 @@ Returns (VALUES INFERRED-TYPE NODE SUBSTITUTIONS)")
22542270
(setf preds (tc:apply-substitution subs preds))
22552271

22562272
;; Generate additional substitutions from fundeps
2273+
;; This effects the inheritance of functional dependencies
2274+
;; from superclasses and reduces generality with respect to
2275+
;; instances defined in the environment.
22572276
(setf subs (nth-value 1 (tc:solve-fundeps (tc-env-env env) preds subs)))
22582277

22592278
(setf preds (tc:apply-substitution subs preds))
@@ -2628,32 +2647,9 @@ Returns (VALUES INFERRED-TYPE NODE SUBSTITUTIONS)")
26282647
;;; binding's predicates.
26292648

26302649
(defun expand-local-tvars (env-tvars local-tvars preds env)
2631-
(let ((old-local-tvars nil))
2632-
(loop :until (null (set-exclusive-or old-local-tvars local-tvars)) :do
2633-
(setf old-local-tvars local-tvars)
2634-
(loop :for pred :in preds
2635-
:for class := (tc:lookup-class env (tc:ty-predicate-class pred))
2636-
:when (tc:ty-class-fundeps class) :do
2637-
(let* ((idx (loop :for i :from 0
2638-
:for ty :in (tc:ty-predicate-types pred)
2639-
:when (subsetp (tc:type-variables ty) local-tvars :test #'eq)
2640-
:collect i))
2641-
2642-
(fundep-vars (util:project-indices idx (tc:ty-class-class-variables class)))
2643-
(closure-vars (tc:closure fundep-vars (tc:ty-class-fundeps class)))
2644-
2645-
(new-vars (set-difference closure-vars fundep-vars :test #'eq))
2646-
2647-
(new-tys (util:project-elements
2648-
new-vars
2649-
(tc:ty-class-class-variables class)
2650-
(tc:ty-predicate-types pred))))
2651-
2652-
(loop :for var :in (set-difference
2653-
(remove-duplicates
2654-
(tc:type-variables new-tys)
2655-
:test #'eq)
2656-
env-tvars)
2657-
:do (push var local-tvars)))))
2658-
2659-
(remove-duplicates local-tvars :test #'eq)))
2650+
"Expand LOCAL-TVARS over the functional dependencies taken from PREDS
2651+
and return the set difference of the expansion and ENV-TVARS."
2652+
(let* ((fundeps (tc:collect-fundep-vars env preds))
2653+
(expansion (tc:generic-closure local-tvars fundeps :test #'tc:ty=))
2654+
(expansion (remove-duplicates expansion :test #'tc:ty=)))
2655+
(set-difference expansion env-tvars :test #'tc:ty=)))

0 commit comments

Comments
 (0)